Germs of functions between topological spaces

In this file, we prove basic properties of germs of functions between topological spaces, with respect to the neighbourhood filter 𝓝 x.

Main definitions and results

• Filter.Germ.value φ f: value associated to the germ φ at a point x, w.r.t. the neighbourhood filter at x. This is the common value of all representatives of φ at x.

• Filter.Germ.valueOrderRingHom and friends: the map Germ (𝓝 x) E → E is a monoid homomorphism, 𝕜-module homomorphism, ring homomorphism, monotone ring homomorphism

• RestrictGermPredicate: given a predicate on germs P : Π x : X, germ (𝓝 x) Y → Prop and A : set X, build a new predicate on germs restrictGermPredicate P A such that (∀ x, RestrictGermPredicate P A x f) ↔ ∀ᶠ x near A, P x f; forall_restrictRermPredicate_iff is this equivalence.

• Filter.Germ.sliceLeft, sliceRight: map the germ of functions X × Y → Z at p = (x,y) ∈ X × Y to the corresponding germ of functions X → Z at x ∈ X resp. Y → Z at y ∈ Y.

• eq_of_germ_isConstant: if each germ of f : X → Y is constant and X is pre-connected, f is constant.

def Filter.Germ.value {X : Type u_6} {α : Type u_7} [TopologicalSpace X] {x : X} (φ : (nhds x).Germ α) : α

The value associated to a germ at a point. This is the common value shared by all representatives at the given point.

Equations

• φ.value = Quotient.liftOn' φ (fun (f : X → α) => f x) ⋯

theorem Filter.Germ.value_smul {X : Type u_3} [TopologicalSpace X] {x : X} {α : Type u_6} {β : Type u_7} [SMul α β] (φ : (nhds x).Germ α) (ψ : (nhds x).Germ β) : (φ • ψ).value = φ.value • ψ.value

theorem Filter.Germ.valueAddHom.proof_1 {X : Type u_2} {E : Type u_1} [AddMonoid E] [TopologicalSpace X] {x : X} : Filter.Germ.value 0 = Filter.Germ.value 0

theorem Filter.Germ.valueAddHom.proof_2 {X : Type u_1} {E : Type u_2} [AddMonoid E] [TopologicalSpace X] {x : X} (φ : (nhds x).Germ E) (ψ : (nhds x).Germ E) : { toFun := Filter.Germ.value, map_zero' := ⋯ }.toFun (φ + ψ) = { toFun := Filter.Germ.value, map_zero' := ⋯ }.toFun φ + { toFun := Filter.Germ.value, map_zero' := ⋯ }.toFun ψ

def Filter.Germ.valueAddHom {X : Type u_6} {E : Type u_7} [AddMonoid E] [TopologicalSpace X] {x : X} : (nhds x).Germ E →+ E

The map Germ (𝓝 x) E → E as an additive monoid homomorphism

Equations

• Filter.Germ.valueAddHom = { toFun := Filter.Germ.value, map_zero' := ⋯, map_add' := ⋯ }

def Filter.Germ.valueMulHom {X : Type u_6} {E : Type u_7} [Monoid E] [TopologicalSpace X] {x : X} : (nhds x).Germ E →* E

The map Germ (𝓝 x) E → E into a monoid E as a monoid homomorphism

Equations

• Filter.Germ.valueMulHom = { toFun := Filter.Germ.value, map_one' := ⋯, map_mul' := ⋯ }

def Filter.Germ.valueₗ {X : Type u_6} {𝕜 : Type u_7} {E : Type u_8} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace X] {x : X} : (nhds x).Germ E →ₗ[𝕜] E

The map Germ (𝓝 x) E → E into a 𝕜-module E as a 𝕜-linear map

Equations

• Filter.Germ.valueₗ = let __spread.0 := Filter.Germ.valueAddHom; { toFun := (↑__spread.0).toFun, map_add' := ⋯, map_smul' := ⋯ }

def Filter.Germ.valueRingHom {X : Type u_6} {E : Type u_7} [Semiring E] [TopologicalSpace X] {x : X} : (nhds x).Germ E →+* E

The map Germ (𝓝 x) E → E as a ring homomorphism

Equations

• Filter.Germ.valueRingHom = let __src := Filter.Germ.valueMulHom; let __src_1 := Filter.Germ.valueAddHom; { toMonoidHom := __src, map_zero' := ⋯, map_add' := ⋯ }

def Filter.Germ.valueOrderRingHom {X : Type u_6} {E : Type u_7} [OrderedSemiring E] [TopologicalSpace X] {x : X} : (nhds x).Germ E →+*o E

The map Germ (𝓝 x) E → E as a monotone ring homomorphism

Equations

• Filter.Germ.valueOrderRingHom = let __spread.0 := Filter.Germ.valueRingHom; { toRingHom := __spread.0, monotone' := ⋯ }

def RestrictGermPredicate {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] (P : (x : X) → (nhds x).Germ Y → Prop) (A : Set X) (x : X) : (nhds x).Germ Y → Prop

Given a predicate on germs P : Π x : X, germ (𝓝 x) Y → Prop and A : set X, build a new predicate on germs RestrictGermPredicate P A such that (∀ x, RestrictGermPredicate P A x f) ↔ ∀ᶠ x near A, P x f, see forall_restrictGermPredicate_iff for this equivalence.

Equations

• RestrictGermPredicate P A x φ = φ.liftOn (fun (f : X → Y) => x ∈ A → ∀ᶠ (y : X) in nhds x, P y ↑f) ⋯

theorem Filter.Eventually.germ_congr_set {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] {f : X → Y} {g : X → Y} {A : Set X} {P : (x : X) → (nhds x).Germ Y → Prop} (hf : ∀ᶠ (x : X) in nhdsSet A, P x ↑f) (h : ∀ᶠ (z : X) in nhdsSet A, g z = f z) : ∀ᶠ (x : X) in nhdsSet A, P x ↑g

theorem restrictGermPredicate_congr {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] {f : X → Y} {g : X → Y} {A : Set X} {x : X} {P : (x : X) → (nhds x).Germ Y → Prop} (hf : RestrictGermPredicate P A x ↑f) (h : ∀ᶠ (z : X) in nhdsSet A, g z = f z) : RestrictGermPredicate P A x ↑g

theorem forall_restrictGermPredicate_iff {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] {f : X → Y} {A : Set X} {P : (x : X) → (nhds x).Germ Y → Prop} : (∀ (x : X), RestrictGermPredicate P A x ↑f) ↔ ∀ᶠ (x : X) in nhdsSet A, P x ↑f

theorem forall_restrictGermPredicate_of_forall {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] {f : X → Y} {A : Set X} {P : (x : X) → (nhds x).Germ Y → Prop} (h : ∀ (x : X), P x ↑f) (x : X) : RestrictGermPredicate P A x ↑f

def Filter.Germ.sliceLeft {X : Type u_3} {Y : Type u_4} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] {p : X × Y} (P : (nhds p).Germ Z) : (nhds p.1).Germ Z

Map the germ of functions X × Y → Z at p = (x,y) ∈ X × Y to the corresponding germ of functions X → Z at x ∈ X

Equations

• P.sliceLeft = P.compTendsto (fun (x : X) => (x, p.2)) ⋯

@[simp]

theorem Filter.Germ.sliceLeft_coe {X : Type u_3} {Y : Type u_4} {Z : Type u_5} [TopologicalSpace X] {x : X} [TopologicalSpace Y] {y : Y} (f : X × Y → Z) : (↑f).sliceLeft = ↑fun (x' : X) => f (x', y)

def Filter.Germ.sliceRight {X : Type u_3} {Y : Type u_4} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] {p : X × Y} (P : (nhds p).Germ Z) : (nhds p.2).Germ Z

Map the germ of functions X × Y → Z at p = (x,y) ∈ X × Y to the corresponding germ of functions Y → Z at y ∈ Y

Equations

• P.sliceRight = P.compTendsto (Prod.mk p.1) ⋯

@[simp]

theorem Filter.Germ.sliceRight_coe {X : Type u_3} {Y : Type u_4} {Z : Type u_5} [TopologicalSpace X] {x : X} [TopologicalSpace Y] {y : Y} (f : X × Y → Z) : (↑f).sliceRight = ↑fun (y' : Y) => f (x, y')

theorem Filter.Germ.isConstant_comp_subtype {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] {s : Set X} {f : X → Y} {x : ↑s} (hf : (↑f).IsConstant) : (↑(f ∘ Subtype.val)).IsConstant

theorem IsLocallyConstant.of_germ_isConstant {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] {f : X → Y} (h : ∀ (x : X), (↑f).IsConstant) : IsLocallyConstant f

If the germ of f w.r.t. each 𝓝 x is constant, f is locally constant.

theorem eq_of_germ_isConstant {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] {f : X → Y} [i : PreconnectedSpace X] (h : ∀ (x : X), (↑f).IsConstant) (x : X) (x' : X) : f x = f x'

theorem eq_of_germ_isConstant_on {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] {f : X → Y} {x : X} {s : Set X} (h : ∀ x ∈ s, (↑f).IsConstant) (hs : IsPreconnected s) {x' : X} (x_in : x ∈ s) (x'_in : x' ∈ s) : f x = f x'

@[simp]

theorem Germ.coe_sum {α : Type u_6} (l : Filter α) (R : Type u_7) [AddCommMonoid R] {ι : Type u_8} (f : ι → α → R) (s : Finset ι) : ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)

@[simp]

theorem Germ.coe_prod {α : Type u_6} (l : Filter α) (R : Type u_7) [CommMonoid R] {ι : Type u_8} (f : ι → α → R) (s : Finset ι) : ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)