Documentation

Mathlib.Topology.Germ

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 #

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
Instances For
    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_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' := β‹― }
    Instances For
      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' := β‹― }
      Instances For
        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' := β‹― }
        Instances For
          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' := β‹― }
          Instances For
            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' := β‹― }
            Instances For
              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
              Instances For
                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)) β‹―
                Instances For
                  @[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) β‹―
                  Instances For
                    @[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) :

                    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)