Covering Maps

This file defines covering maps.

Main definitions

• IsEvenlyCovered f x I: A point x is evenly covered by f : E → X with fiber I if I is discrete and there is a homeomorphism f ⁻¹' U ≃ₜ U × I for some open set U containing x with f ⁻¹' U open, such that the induced map f ⁻¹' U → U coincides with f.
• IsCoveringMap f: A function f : E → X is a covering map if every point x is evenly covered by f with fiber f ⁻¹' {x}. The fibers f ⁻¹' {x} must be discrete, but if X is not connected, then the fibers f ⁻¹' {x} are not necessarily isomorphic. Also, f is not assumed to be surjective, so the fibers are even allowed to be empty.

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

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

• IsEvenlyCovered f x I = (DiscreteTopology I ∧ ∃ (U : Set X), x ∈ U ∧ IsOpen U ∧ IsOpen (f ⁻¹' U) ∧ ∃ (H : ↑(f ⁻¹' U) ≃ₜ ↑U × I), ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x)

noncomputable def IsEvenlyCovered.fiberHomeomorph {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {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.

theorem IsEvenlyCovered.discreteTopology_fiber {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {I : Type u_3} [TopologicalSpace I] {x : X} (h : IsEvenlyCovered f x I) : DiscreteTopology ↑(f ⁻¹' {x})

noncomputable def IsEvenlyCovered.toTrivialization' {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {I : Type u_3} [TopologicalSpace I] {x : X} [Nonempty I] (h : IsEvenlyCovered f x I) : Trivialization I f

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.

noncomputable def IsEvenlyCovered.toTrivialization {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {I : Type u_3} [TopologicalSpace I] {x : X} [Nonempty 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

• h.toTrivialization = h.toTrivialization'.transFiberHomeomorph h.fiberHomeomorph

theorem IsEvenlyCovered.mem_toTrivialization_baseSet {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {I : Type u_3} [TopologicalSpace I] {x : X} [Nonempty 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 : E → X} {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 : E → X} {I : Type u_3} [TopologicalSpace I] {x : E} (h : IsEvenlyCovered f (f x) I) : ContinuousAt f x

theorem IsEvenlyCovered.of_fiber_homeomorph {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {I : Type u_3} [TopologicalSpace I] {J : Type u_4} [TopologicalSpace J] (g : I ≃ₜ J) {x : X} (h : IsEvenlyCovered f x I) : IsEvenlyCovered f x J

theorem IsEvenlyCovered.to_isEvenlyCovered_preimage {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {I : Type u_3} [TopologicalSpace I] {x : X} (h : IsEvenlyCovered f x I) : IsEvenlyCovered f x ↑(f ⁻¹' {x})

theorem IsEvenlyCovered.of_trivialization {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {I : Type u_3} [TopologicalSpace I] [DiscreteTopology I] {x : X} {t : Trivialization I f} (hx : x ∈ t.baseSet) : IsEvenlyCovered f x I

theorem IsEvenlyCovered.of_preimage_eq_empty {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} (I : Type u_3) [TopologicalSpace I] [IsEmpty I] {x : X} {U : Set X} (hUx : U ∈ nhds x) (hfU : f ⁻¹' U = ∅) : IsEvenlyCovered f x I

def IsCoveringMapOn {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] (f : E → X) (s : Set X) : Prop

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

• IsCoveringMapOn f s = ∀ x ∈ s, IsEvenlyCovered f x ↑(f ⁻¹' {x})

theorem IsCoveringMapOn.of_isEmpty {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] (f : E → X) (s : Set X) [IsEmpty E] : IsCoveringMapOn f s

theorem IsCoveringMapOn.mk' {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] (f : E → X) (s : Set X) (F : ↑s → Type 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), ↑x ∉ Set.range f → ∃ U ∈ nhds ↑x, f ⁻¹' U = ∅) : IsCoveringMapOn f s

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 : E → X) (s : Set X) (F : ↑s → Type 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) : IsCoveringMapOn f s

theorem IsCoveringMapOn.continuousAt {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {s : Set X} (hf : IsCoveringMapOn f s) {x : E} (hx : f x ∈ s) : ContinuousAt f x

theorem IsCoveringMapOn.continuousOn {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {s : Set X} (hf : IsCoveringMapOn f s) : ContinuousOn f (f ⁻¹' s)

theorem IsCoveringMapOn.isLocalHomeomorphOn {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {s : Set X} (hf : IsCoveringMapOn f s) : IsLocalHomeomorphOn f (f ⁻¹' s)

def IsCoveringMap {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] (f : E → X) : Prop

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

• IsCoveringMap f = ∀ (x : X), IsEvenlyCovered f x ↑(f ⁻¹' {x})

theorem isCoveringMap_iff_isCoveringMapOn_univ {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} : IsCoveringMap f ↔ IsCoveringMapOn f Set.univ

theorem IsCoveringMap.isCoveringMapOn {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} (hf : IsCoveringMap f) : IsCoveringMapOn f Set.univ

theorem IsCoveringMap.of_isEmpty {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] (f : E → X) [IsEmpty E] : IsCoveringMap f

theorem IsCoveringMap.of_discreteTopology {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] (f : E → X) [DiscreteTopology E] [DiscreteTopology X] : IsCoveringMap f

theorem IsCoveringMap.mk' {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] (f : E → X) (F : X → Type 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)) : IsCoveringMap 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 : E → X) (F : X → Type 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) : IsCoveringMap f

theorem IsCoveringMap.continuous {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} (hf : IsCoveringMap f) : Continuous f

theorem IsCoveringMap.isLocalHomeomorph {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} (hf : IsCoveringMap f) : IsLocalHomeomorph f

theorem IsCoveringMap.isOpenMap {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} (hf : IsCoveringMap f) : IsOpenMap f

theorem IsCoveringMap.isQuotientMap {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} (hf : IsCoveringMap f) (hf' : Function.Surjective f) : Topology.IsQuotientMap f

theorem IsCoveringMap.isSeparatedMap {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} (hf : IsCoveringMap f) : IsSeparatedMap f

theorem IsCoveringMap.eq_of_comp_eq {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} (hf : IsCoveringMap f) {A : Type u_3} [TopologicalSpace A] {g₁ g₂ : A → E} [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 : E → X} (hf : IsCoveringMap f) {A : Type u_3} [TopologicalSpace A] {g : A → E} [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 : E → X} (hf : IsCoveringMap f) {A : Type u_3} [TopologicalSpace A] {s : Set A} {g₁ g₂ : A → E} (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 : E → X} (hf : IsCoveringMap f) {A : Type u_3} [TopologicalSpace A] {s : Set A} {g : A → E} (hs : IsPreconnected s) (cont : ContinuousOn g s) (he : ∀ a ∈ s, ∀ 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 : E → X} {F : Type u_3} [TopologicalSpace F] [DiscreteTopology F] (hf : ∀ (x : X), ∃ (e : Trivialization F f), x ∈ e.baseSet) : IsCoveringMap f

theorem FiberBundle.isCoveringMap {X : Type u_2} [TopologicalSpace X] {F : Type u_3} {E : X → Type u_4} [TopologicalSpace F] [DiscreteTopology F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : X) → TopologicalSpace (E x)] [FiberBundle F E] : IsCoveringMap Bundle.TotalSpace.proj