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.

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

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

    Equations
    Instances For
      theorem IsEvenlyCovered.mem_toTrivialization_baseSet {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : EX} {x : X} {I : Type u_3} [TopologicalSpace I] (h : IsEvenlyCovered f x I) :
      x h.toTrivialization.baseSet
      theorem IsEvenlyCovered.toTrivialization_apply {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : EX} {x : E} {I : Type u_3} [TopologicalSpace 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} {x : E} {I : Type u_3} [TopologicalSpace I] (h : IsEvenlyCovered f (f x) I) :
      theorem IsEvenlyCovered.to_isEvenlyCovered_preimage {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : EX} {x : X} {I : Type u_3} [TopologicalSpace I] (h : IsEvenlyCovered f x I) :
      IsEvenlyCovered f x (f ⁻¹' {x})
      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.mk {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] (f : EX) (s : Set X) (F : XType u_3) [(x : X) → TopologicalSpace (F x)] [hF : ∀ (x : X), DiscreteTopology (F x)] (e : (x : X) → x sTrivialization (F x) f) (h : ∀ (x : X) (hx : x s), x (e x hx).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.isCoveringMapOn {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : EX} (hf : IsCoveringMap f) :
          IsCoveringMapOn f Set.univ
          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) :
          theorem IsCoveringMap.quotientMap {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : EX} (hf : IsCoveringMap f) (hf' : Function.Surjective f) :
          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₁ : AE} {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.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} (hs : IsPreconnected s) {g₁ : AE} {g₂ : AE} (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.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' : A) :
          g a = g a'
          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} (hs : IsPreconnected s) {g : AE} (cont : ContinuousOn g s) (he : as, a's, f (g a) = f (g a')) {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) :
          theorem FiberBundle.isCoveringMap {X : Type u_2} [TopologicalSpace X] {F : Type u_3} {E : XType u_4} [TopologicalSpace F] [DiscreteTopology F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : X) → TopologicalSpace (E x)] [FiberBundle F E] :
          IsCoveringMap Bundle.TotalSpace.proj