Fullness for monodromy natural transformations

When the base is locally path-connected, every natural transformation between the monodromy functors of two covering maps is induced by a continuous map between their total spaces over the base.

The map on total spaces is forced pointwise: at e, apply the component of the natural transformation over p e to e viewed as an element of that fibre. Its continuity is the topological content. Around e, choose a path-connected open set contained in the images of chosen sheets for both covers. Naturality along paths in that set shows that the forced map agrees there with the inverse of the target sheet composed with the source projection.

Main declaration

• IsCoveringMap.exists_map_of_monodromyNatTrans: a natural transformation between monodromy functors of covering maps is induced by a continuous map over the base.

References

This is the fullness step in the alternative monodromy-functor classification requested by Stage 2, item 8 of TauCetiRoadmap/UniversalCovers/README.md. The mathematical argument is the standard local-sheet proof of fullness for the monodromy functor; see A. Hatcher, Algebraic Topology, Section 1.3. It uses Junyan Xu's path-lifting and monodromy API in Mathlib/Topology/Homotopy/Lifting.lean.

theorem IsCoveringMap.exists_map_of_monodromyNatTrans {E F : Type u} {X : Type v} [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace X] {p : E → X} {q : F → X} [LocallyPathConnectedSpace X] (hp : IsCoveringMap p) (hq : IsCoveringMap q) (α : hp.monodromyFunctor ⟶ hq.monodromyFunctor) : ∃ (f : C(E, F)) (hf : q ∘ ⇑f = p), hp.monodromyNatTrans hq f hf = α

Over a locally path-connected base, every natural transformation between the monodromy functors of two covering maps is induced by a continuous map over the base.