# mathlib3documentation

topology.covering

# Covering Maps #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines covering maps.

## Main definitions #

• is_evenly_covered f x I: A point x is evenly coverd by f : E → X with fiber I if I is discrete and there is a trivialization of f at x with fiber I.
• is_covering_map 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 is_evenly_covered {E : Type u_1} {X : Type u_2} (f : E X) (x : X) (I : Type u_3)  :
Prop

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

Equations
noncomputable def is_evenly_covered.to_trivialization {E : Type u_1} {X : Type u_2} {f : E X} {x : X} {I : Type u_3} (h : I) :

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

Equations
theorem is_evenly_covered.mem_to_trivialization_base_set {E : Type u_1} {X : Type u_2} {f : E X} {x : X} {I : Type u_3} (h : I) :
theorem is_evenly_covered.to_trivialization_apply {E : Type u_1} {X : Type u_2} {f : E X} {x : E} {I : Type u_3} (h : (f x) I) :
((h.to_trivialization) x).snd = x, _⟩
@[protected]
theorem is_evenly_covered.continuous_at {E : Type u_1} {X : Type u_2} {f : E X} {x : E} {I : Type u_3} (h : (f x) I) :
theorem is_evenly_covered.to_is_evenly_covered_preimage {E : Type u_1} {X : Type u_2} {f : E X} {x : X} {I : Type u_3} (h : I) :
(f ⁻¹' {x})
def is_covering_map_on {E : Type u_1} {X : Type u_2} (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
theorem is_covering_map_on.mk {E : Type u_1} {X : Type u_2} (f : E X) (s : set X) (F : X Type u_3) [Π (x : X), topological_space (F x)] [hF : (x : X), discrete_topology (F x)] (e : Π (x : X), x s trivialization (F x) f) (h : (x : X) (hx : x s), x (e x hx).base_set) :
@[protected]
theorem is_covering_map_on.continuous_at {E : Type u_1} {X : Type u_2} {f : E X} {s : set X} (hf : s) {x : E} (hx : f x s) :
@[protected]
theorem is_covering_map_on.continuous_on {E : Type u_1} {X : Type u_2} {f : E X} {s : set X} (hf : s) :
(f ⁻¹' s)
@[protected]
theorem is_covering_map_on.is_locally_homeomorph_on {E : Type u_1} {X : Type u_2} {f : E X} {s : set X} (hf : s) :
(f ⁻¹' s)
def is_covering_map {E : Type u_1} {X : Type u_2} (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
theorem is_covering_map_iff_is_covering_map_on_univ {E : Type u_1} {X : Type u_2} {f : E X} :
@[protected]
theorem is_covering_map.is_covering_map_on {E : Type u_1} {X : Type u_2} {f : E X} (hf : is_covering_map f) :
theorem is_covering_map.mk {E : Type u_1} {X : Type u_2} (f : E X) (F : X Type u_3) [Π (x : X), topological_space (F x)] [hF : (x : X), discrete_topology (F x)] (e : Π (x : X), trivialization (F x) f) (h : (x : X), x (e x).base_set) :
@[protected]
theorem is_covering_map.continuous {E : Type u_1} {X : Type u_2} {f : E X} (hf : is_covering_map f) :
@[protected]
theorem is_covering_map.is_locally_homeomorph {E : Type u_1} {X : Type u_2} {f : E X} (hf : is_covering_map f) :
@[protected]
theorem is_covering_map.is_open_map {E : Type u_1} {X : Type u_2} {f : E X} (hf : is_covering_map f) :
@[protected]
theorem is_covering_map.quotient_map {E : Type u_1} {X : Type u_2} {f : E X} (hf : is_covering_map f) (hf' : function.surjective f) :
@[protected]
theorem is_fiber_bundle.is_covering_map {E : Type u_1} {X : Type u_2} {f : E X} {F : Type u_3} (hf : (x : X), (e : f), x e.base_set) :
@[protected]
theorem fiber_bundle.is_covering_map {X : Type u_2} {F : Type u_1} {E : X Type u_3} [Π (x : X), topological_space (E x)] [hf : E] :