Fullness of covering-space monodromy #
When the base is locally path-connected, the monodromy functor from covering spaces to
fundamental-groupoid actions is full. The unbundled construction of the map between total spaces
is proved in TauCeti.Topology.Homotopy.Monodromy.Full; this file packages it for bundled covering
spaces. Its fully faithful restriction from connected covers to fibrewise pretransitive actions is
packaged in TauCeti.Topology.Covering.Monodromy.Connected.
Main declaration #
TauCeti.CoveringSpace.monodromyFunctor_full: over a locally path-connected base, the monodromy functor on covering spaces is full.
References #
This packages the fullness step in the alternative monodromy-functor classification requested by
Stage 2, item 8 of TauCetiRoadmap/UniversalCovers/README.md.
instance
TauCeti.CoveringSpace.monodromyFunctor_full
{X : TopCat}
[LocallyPathConnectedSpace ↑X]
:
(monodromyFunctor X).Full
Over a locally path-connected base, every natural transformation of monodromy functors is induced by a map of covering spaces.