Functoriality of covering-space monodromy

A continuous map between two covering spaces over the same base carries lifts of a path to lifts of that path. Consequently it intertwines transport between fibres and induces a natural transformation between the two monodromy functors. An isomorphism of covers induces a natural isomorphism. The underlying set-level operations on fibres — the restriction Function.fiberMap of a map over the base to a fibre and the relabelling Equiv.compFiberEquiv of fibres under a bijection of bases — come from TauCeti.Logic.Function.Fiber; this file adds their compatibility with monodromy.

These constructions are the morphism-level input for the alternative classification of covers as functors from the fundamental groupoid in TauCetiRoadmap/UniversalCovers/README.md, Stage 2, item 8. Mathlib supplies the object-level functor IsCoveringMap.monodromyFunctor; this file packages its functoriality in the covering map.

Main declarations

• IsCoveringMap.fiberMap_monodromy: a map of covers intertwines monodromy transport on their fibres.
• IsCoveringMap.permutationRepresentation_eq_of_fiberMap: a map of covers respecting numberings identifies the numbered monodromy representations.
• IsCoveringMap.monodromyNatTrans: a map of covers induces a natural transformation between their monodromy functors.
• IsCoveringMap.monodromyNatIso: an isomorphism of covers induces a natural isomorphism between their monodromy functors.
• IsCoveringMap.monodromyHomeomorphCompNatIso: changing the base by a homeomorphism transports the monodromy functor by the inverse homeomorphism.

References

The proof uses Junyan Xu's path-lifting and monodromy API in Mathlib/Topology/Homotopy/Lifting.lean. No Mathlib code is vendored.

@[simp]

theorem IsCoveringMap.fiberMap_monodromy {E F : Type u} {X : Type v} [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace X] {p : E → X} {q : F → X} (hp : IsCoveringMap p) (hq : IsCoveringMap q) (f : C(E, F)) (hf : q ∘ ⇑f = p) {x y : X} (a : Path.Homotopic.Quotient x y) (e : ↑(p ⁻¹' {x})) : Function.fiberMap (⇑f) hf y (hp.monodromy a e) = hq.monodromy a (Function.fiberMap (⇑f) hf x e)

A map between covering spaces over the same base intertwines monodromy along every path.

theorem IsCoveringMap.permutationRepresentation_eq_of_fiberMap {E F : Type u} {X : Type v} [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace X] {p : E → X} {q : F → X} {n : ℕ} (hp : IsCoveringMap p) (hq : IsCoveringMap q) (x : X) (ν : ↑(p ⁻¹' {x}) ≃ Fin n) (ν' : ↑(q ⁻¹' {x}) ≃ Fin n) (f : C(E, F)) (hf : q ∘ ⇑f = p) (hν : ∀ (e : ↑(p ⁻¹' {x})), ν' (Function.fiberMap (⇑f) hf x e) = ν e) : ν'.permCongrHom.toMonoidHom.comp (hq.monodromyPerm x) = ν.permCongrHom.toMonoidHom.comp (hp.monodromyPerm x)

A map of covers that preserves the numberings of two fibres identifies their numbered monodromy representations.

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

A continuous map of covering spaces over X induces a natural transformation between their monodromy functors. Its component over x is the restriction of f to the fibre over x.

Equations

• hp.monodromyNatTrans hq f hf = { app := fun (x : FundamentalGroupoid X) => TypeCat.ofHom (Function.fiberMap (⇑f) hf x.as), naturality := ⋯ }

@[simp]

theorem IsCoveringMap.monodromyNatTrans_app {E F : Type u} {X : Type v} [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace X] {p : E → X} {q : F → X} (hp : IsCoveringMap p) (hq : IsCoveringMap q) (f : C(E, F)) (hf : q ∘ ⇑f = p) (x : X) : (hp.monodromyNatTrans hq f hf).app { as := x } = TypeCat.ofHom (Function.fiberMap (⇑f) hf x)

On a fibre, the natural transformation induced by a map of covers applies that map to the underlying point.

theorem IsCoveringMap.monodromyNatTrans_congr {E F : Type u} {X : Type v} [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace X] {p : E → X} {q : F → X} (hp : IsCoveringMap p) (hq : IsCoveringMap q) {f g : C(E, F)} (hf : q ∘ ⇑f = p) (hg : q ∘ ⇑g = p) (h : f = g) : hp.monodromyNatTrans hq f hf = hp.monodromyNatTrans hq g hg

The natural transformation induced by a map over the base depends only on that map, not on the proof that it lies over the base.

@[simp]

theorem IsCoveringMap.monodromyNatTrans_id {E : Type u} {X : Type v} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} (hp : IsCoveringMap p) : hp.monodromyNatTrans hp (ContinuousMap.id E) ⋯ = CategoryTheory.CategoryStruct.id hp.monodromyFunctor

The identity map of a cover induces the identity natural transformation.

theorem IsCoveringMap.monodromyNatTrans_comp {E F G : Type u} {X : Type v} [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalSpace X] {p : E → X} {q : F → X} {r : G → X} (hp : IsCoveringMap p) (hq : IsCoveringMap q) (hr : IsCoveringMap r) (f : C(E, F)) (g : C(F, G)) (hf : q ∘ ⇑f = p) (hg : r ∘ ⇑g = q) : hp.monodromyNatTrans hr (g.comp f) ⋯ = CategoryTheory.CategoryStruct.comp (hp.monodromyNatTrans hq f hf) (hq.monodromyNatTrans hr g hg)

Composition of maps of covers induces vertical composition of their monodromy natural transformations.

noncomputable def IsCoveringMap.monodromyNatIso {E F : Type u} {X : Type v} [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace X] {p : E → X} {q : F → X} (hp : IsCoveringMap p) (hq : IsCoveringMap q) (h : E ≃ₜ F) (hh : q ∘ ⇑h = p) : hp.monodromyFunctor ≅ hq.monodromyFunctor

An isomorphism of covering spaces over X induces a natural isomorphism between their monodromy functors. Its forward and inverse transformations are the ones induced by the homeomorphism and its inverse, so its component over x is the restriction of the homeomorphism to the fibre over x.

Equations

• hp.monodromyNatIso hq h hh = { hom := hp.monodromyNatTrans hq (↑h) hh, inv := hq.monodromyNatTrans hp ↑h.symm ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem IsCoveringMap.monodromyNatIso_hom {E F : Type u} {X : Type v} [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace X] {p : E → X} {q : F → X} (hp : IsCoveringMap p) (hq : IsCoveringMap q) (h : E ≃ₜ F) (hh : q ∘ ⇑h = p) : (hp.monodromyNatIso hq h hh).hom = hp.monodromyNatTrans hq (↑h) hh

The forward natural transformation of the monodromy isomorphism is the canonical transformation induced by the homeomorphism.

@[simp]

theorem IsCoveringMap.monodromyNatIso_inv {E F : Type u} {X : Type v} [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace X] {p : E → X} {q : F → X} (hp : IsCoveringMap p) (hq : IsCoveringMap q) (h : E ≃ₜ F) (hh : q ∘ ⇑h = p) : (hp.monodromyNatIso hq h hh).inv = hq.monodromyNatTrans hp ↑h.symm ⋯

The inverse natural transformation of the monodromy isomorphism is induced by the inverse homeomorphism.

theorem IsCoveringMap.compFiberEquiv_monodromy {E : Type u} {X : Type v} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {Y : Type v} [TopologicalSpace Y] (hp : IsCoveringMap p) (h : X ≃ₜ Y) {x y : Y} (a : Path.Homotopic.Quotient x y) (e : ↑(⇑h ∘ p ⁻¹' {x})) : (h.compFiberEquiv y) (⋯.monodromy a e) = hp.monodromy (a.map ↑h.symm) ((h.compFiberEquiv x) e)

Fibre transport after changing the base by a homeomorphism agrees with transport along the inverse image of the path.

noncomputable def IsCoveringMap.monodromyHomeomorphCompNatIso {E : Type u} {X : Type v} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {Y : Type v} [TopologicalSpace Y] (hp : IsCoveringMap p) (h : X ≃ₜ Y) : ⋯.monodromyFunctor ≅ (FundamentalGroupoid.map ↑h.symm).comp hp.monodromyFunctor

Changing the base of a covering map by a homeomorphism transports monodromy along the inverse homeomorphism.

Equations

• hp.monodromyHomeomorphCompNatIso h = CategoryTheory.NatIso.ofComponents (fun (y : FundamentalGroupoid Y) => (h.compFiberEquiv y.as).toIso) ⋯

@[simp]

theorem IsCoveringMap.monodromyHomeomorphCompNatIso_hom_app {E : Type u} {X : Type v} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {Y : Type v} [TopologicalSpace Y] (hp : IsCoveringMap p) (h : X ≃ₜ Y) (y : Y) : (hp.monodromyHomeomorphCompNatIso h).hom.app { as := y } = (h.compFiberEquiv y).toIso.hom

The forward component of the monodromy isomorphism for a homeomorphic base is the canonical equivalence of fibres.