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 pointxis evenly coverd byf : E → Xwith fiberIifIis discrete and there is atrivializationoffatxwith fiberI.is_covering_map f: A functionf : E → Xis a covering map if every pointxis evenly covered byfwith fiberf ⁻¹' {x}. The fibersf ⁻¹' {x}must be discrete, but ifXis not connected, then the fibersf ⁻¹' {x}are not necessarily isomorphic. Also,fis 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}
[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
- is_evenly_covered f x I = (discrete_topology I ∧ ∃ (t : trivialization I f), x ∈ t.base_set)
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) :
trivialization ↥(f ⁻¹' {x}) f
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}
[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) :
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) :
continuous_at f x
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) :
is_evenly_covered f x ↥(f ⁻¹' {x})
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
- is_covering_map_on f s = ∀ (x : X), x ∈ s → is_evenly_covered f x ↥(f ⁻¹' {x})
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) :
continuous_at f x
@[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) :
continuous_on f (f ⁻¹' s)
@[protected]
theorem
is_covering_map_on.is_locally_homeomorph_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) :
is_locally_homeomorph_on f (f ⁻¹' s)
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
- is_covering_map f = ∀ (x : X), is_evenly_covered f x ↥(f ⁻¹' {x})
theorem
is_covering_map_iff_is_covering_map_on_univ
{E : Type u_1}
{X : Type u_2}
[topological_space E]
[topological_space X]
{f : E → X} :
@[protected]
theorem
is_covering_map.is_covering_map_on
{E : Type u_1}
{X : Type u_2}
[topological_space E]
[topological_space X]
{f : E → X}
(hf : is_covering_map f) :
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]
theorem
is_covering_map.is_locally_homeomorph
{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.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) :
@[protected]
theorem
fiber_bundle.is_covering_map
{X : Type u_2}
[topological_space X]
{F : Type u_1}
{E : X → Type u_3}
[topological_space F]
[discrete_topology F]
[topological_space (bundle.total_space F E)]
[Π (x : X), topological_space (E x)]
[hf : fiber_bundle F E] :