Covering Maps #
This file defines covering maps.
Main definitions #
IsEvenlyCovered f x I
: A pointx
is evenly covered byf : E → X
with fiberI
ifI
is discrete and there is a homeomorphismf ⁻¹' U ≃ₜ U × I
for some open setU
containingx
withf ⁻¹' U
open, such that the induced mapf ⁻¹' U → U
coincides withf
.IsCoveringMap f
: A functionf : E → X
is a covering map if every pointx
is evenly covered byf
with fiberf ⁻¹' {x}
. The fibersf ⁻¹' {x}
must be discrete, but ifX
is not connected, then the fibersf ⁻¹' {x}
are not necessarily isomorphic. Also,f
is not assumed to be surjective, so the fibers are even allowed to be empty.
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
Instances For
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.
Instances For
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.
Instances For
If x
is evenly covered by f
, then we can construct a trivialization of f
at x
.
Equations
Instances For
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})
Instances For
A constructor for IsCoveringMapOn
when there are both empty and nonempty fibers.
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})
Instances For
A constructor for IsCoveringMap
when there are both empty and nonempty fibers.
Alias of IsCoveringMap.isQuotientMap
.