Documentation

Mathlib.Topology.Covering

Covering Maps #

This file defines covering maps.

Main definitions #

def IsEvenlyCovered {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] (f : EX) (x : X) (I : Type u_3) [TopologicalSpace I] :

A point x : X is evenly covered by f : E → X if x has an evenly covered neighborhood.

Remark: DiscreteTopology I ∧ ∃ Trivialization I f, x ∈ t.baseSet would be a simpler definition, but unfortunately it does not work if E is nonempty but nonetheless f has empty fibers over s. If PartialHomeomorph could be refactored to work with an empty space and a nonempty space while preserving the APIs, we could switch back to the definition.

Equations
Instances For
    noncomputable def IsEvenlyCovered.fiberHomeomorph {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : EX} {I : Type u_3} [TopologicalSpace I] {x : X} (h : IsEvenlyCovered f x I) :
    I ≃ₜ ↑(f ⁻¹' {x})

    If x : X is evenly covered by f with fiber I, then I is homeomorphic to f ⁻¹' {x}.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem IsEvenlyCovered.discreteTopology_fiber {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : EX} {I : Type u_3} [TopologicalSpace I] {x : X} (h : IsEvenlyCovered f x I) :
      noncomputable def IsEvenlyCovered.toTrivialization' {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : EX} {I : Type u_3} [TopologicalSpace I] {x : X} [Nonempty I] (h : IsEvenlyCovered f x I) :

      If x is evenly covered by f with nonempty fiber I, then we can construct a trivialization of f at x with fiber I.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        noncomputable def IsEvenlyCovered.toTrivialization {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : EX} {I : Type u_3} [TopologicalSpace I] {x : X} [Nonempty I] (h : IsEvenlyCovered f x I) :

        If x is evenly covered by f, then we can construct a trivialization of f at x.

        Equations
        Instances For
          theorem IsEvenlyCovered.toTrivialization_apply {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : EX} {I : Type u_3} [TopologicalSpace I] {x : E} [Nonempty I] (h : IsEvenlyCovered f (f x) I) :
          (h.toTrivialization x).2 = x,
          theorem IsEvenlyCovered.continuousAt {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : EX} {I : Type u_3} [TopologicalSpace I] {x : E} (h : IsEvenlyCovered f (f x) I) :
          theorem IsEvenlyCovered.of_fiber_homeomorph {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : EX} {I : Type u_3} [TopologicalSpace I] {J : Type u_4} [TopologicalSpace J] (g : I ≃ₜ J) {x : X} (h : IsEvenlyCovered f x I) :
          theorem IsEvenlyCovered.to_isEvenlyCovered_preimage {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : EX} {I : Type u_3} [TopologicalSpace I] {x : X} (h : IsEvenlyCovered f x I) :
          theorem IsEvenlyCovered.of_trivialization {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : EX} {I : Type u_3} [TopologicalSpace I] [DiscreteTopology I] {x : X} {t : Trivialization I f} (hx : x t.baseSet) :
          theorem IsEvenlyCovered.of_preimage_eq_empty {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : EX} (I : Type u_3) [TopologicalSpace I] [IsEmpty I] {x : X} {U : Set X} (hUx : U nhds x) (hfU : f ⁻¹' U = ) :
          def IsCoveringMapOn {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] (f : EX) (s : Set X) :

          A covering map is a continuous function f : E → X with discrete fibers such that each point of X has an evenly covered neighborhood.

          Equations
          Instances For
            theorem IsCoveringMapOn.of_isEmpty {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] (f : EX) (s : Set X) [IsEmpty E] :
            theorem IsCoveringMapOn.mk' {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] (f : EX) (s : Set X) (F : sType u_3) [(x : s) → TopologicalSpace (F x)] [hF : ∀ (x : s), DiscreteTopology (F x)] (t : (x : s) → x Set.range f{ t : Trivialization (F x) f // x t.baseSet }) (h : ∀ (x : s), xSet.range fUnhds x, f ⁻¹' U = ) :

            A constructor for IsCoveringMapOn when there are both empty and nonempty fibers.

            theorem IsCoveringMapOn.mk {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] (f : EX) (s : Set X) (F : sType u_3) [(x : s) → TopologicalSpace (F x)] [hF : ∀ (x : s), DiscreteTopology (F x)] (e : (x : s) → Trivialization (F x) f) (h : ∀ (x : s), x (e x).baseSet) :
            theorem IsCoveringMapOn.continuousAt {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : EX} {s : Set X} (hf : IsCoveringMapOn f s) {x : E} (hx : f x s) :
            theorem IsCoveringMapOn.continuousOn {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : EX} {s : Set X} (hf : IsCoveringMapOn f s) :
            theorem IsCoveringMapOn.isLocalHomeomorphOn {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : EX} {s : Set X} (hf : IsCoveringMapOn f s) :
            def IsCoveringMap {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] (f : EX) :

            A covering map is a continuous function f : E → X with discrete fibers such that each point of X has an evenly covered neighborhood.

            Equations
            Instances For
              theorem IsCoveringMap.of_isEmpty {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] (f : EX) [IsEmpty E] :
              theorem IsCoveringMap.mk' {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] (f : EX) (F : XType u_3) [(x : X) → TopologicalSpace (F x)] [∀ (x : X), DiscreteTopology (F x)] (t : (x : X) → x Set.range f{ t : Trivialization (F x) f // x t.baseSet }) (h : IsClosed (Set.range f)) :

              A constructor for IsCoveringMap when there are both empty and nonempty fibers.

              theorem IsCoveringMap.mk {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] (f : EX) (F : XType u_3) [(x : X) → TopologicalSpace (F x)] [∀ (x : X), DiscreteTopology (F x)] (e : (x : X) → Trivialization (F x) f) (h : ∀ (x : X), x (e x).baseSet) :
              theorem IsCoveringMap.continuous {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : EX} (hf : IsCoveringMap f) :
              theorem IsCoveringMap.isOpenMap {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : EX} (hf : IsCoveringMap f) :
              @[deprecated IsCoveringMap.isQuotientMap (since := "2024-10-22")]

              Alias of IsCoveringMap.isQuotientMap.

              theorem IsCoveringMap.isSeparatedMap {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : EX} (hf : IsCoveringMap f) :
              theorem IsCoveringMap.eq_of_comp_eq {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : EX} (hf : IsCoveringMap f) {A : Type u_3} [TopologicalSpace A] {g₁ g₂ : AE} [PreconnectedSpace A] (h₁ : Continuous g₁) (h₂ : Continuous g₂) (he : f g₁ = f g₂) (a : A) (ha : g₁ a = g₂ a) :
              g₁ = g₂
              theorem IsCoveringMap.const_of_comp {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : EX} (hf : IsCoveringMap f) {A : Type u_3} [TopologicalSpace A] {g : AE} [PreconnectedSpace A] (cont : Continuous g) (he : ∀ (a a' : A), f (g a) = f (g a')) (a a' : A) :
              g a = g a'
              theorem IsCoveringMap.eqOn_of_comp_eqOn {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : EX} (hf : IsCoveringMap f) {A : Type u_3} [TopologicalSpace A] {s : Set A} {g₁ g₂ : AE} (hs : IsPreconnected s) (h₁ : ContinuousOn g₁ s) (h₂ : ContinuousOn g₂ s) (he : Set.EqOn (f g₁) (f g₂) s) {a : A} (has : a s) (ha : g₁ a = g₂ a) :
              Set.EqOn g₁ g₂ s
              theorem IsCoveringMap.constOn_of_comp {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : EX} (hf : IsCoveringMap f) {A : Type u_3} [TopologicalSpace A] {s : Set A} {g : AE} (hs : IsPreconnected s) (cont : ContinuousOn g s) (he : as, a's, f (g a) = f (g a')) {a a' : A} (ha : a s) (ha' : a' s) :
              g a = g a'
              theorem IsFiberBundle.isCoveringMap {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : EX} {F : Type u_3} [TopologicalSpace F] [DiscreteTopology F] (hf : ∀ (x : X), ∃ (e : Trivialization F f), x e.baseSet) :