mathlib documentation

topology.covering

Covering Maps #

This file defines covering maps.

Main definitions #

def is_evenly_covered {E : Type u_1} {X : Type u_2} [topological_space E] [topological_space X] (f : E X) (x : X) (I : Type u_3) [topological_space I] :
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} [topological_space E] [topological_space X] {f : E X} {x : X} {I : Type u_3} [topological_space I] (h : is_evenly_covered f x I) :

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

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