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 Trivialization of f at x with fiber I.
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.

Instances For

source

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

Instances For

source

theorem IsEvenlyCovered.mem_toTrivialization_baseSet {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {x : X} {I : Type u_3} [TopologicalSpace I] (h : IsEvenlyCovered f x I) :

x ∈ (IsEvenlyCovered.toTrivialization h).baseSet

source

theorem IsEvenlyCovered.toTrivialization_apply {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {x : E} {I : Type u_3} [TopologicalSpace I] (h : IsEvenlyCovered f (f x) I) :

(↑(IsEvenlyCovered.toTrivialization h) x).snd = { val := x, property := (_ : f x = f x) }

source

theorem IsEvenlyCovered.continuousAt {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {x : E} {I : Type u_3} [TopologicalSpace I] (h : IsEvenlyCovered f (f x) I) :

ContinuousAt f x

source

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

IsEvenlyCovered f x ↑(f ⁻¹' {x})

source

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.

Instances For

source

theorem IsCoveringMapOn.mk {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] (f : E → X) (s : Set X) (F : X → Type u_3) [(x : X) → TopologicalSpace (F x)] [hF : ∀ (x : X), DiscreteTopology (F x)] (e : (x : X) → x ∈ s → Trivialization (F x) f) (h : ∀ (x : X) (hx : x ∈ s), x ∈ (e x hx).baseSet) :

IsCoveringMapOn f s

source

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

source

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)

source

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

IsLocallyHomeomorphOn f (f ⁻¹' s)

source

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.

Instances For

source

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

source

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

source

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

source

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

Continuous f

source

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

IsLocallyHomeomorph f

source

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

IsOpenMap f

source

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

QuotientMap f

source

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, x ∈ e.baseSet) :

IsCoveringMap f

source

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