Documentation

TauCeti.Topology.Covering.Monodromy.Basic

The monodromy functor on covering spaces #

For a fixed topological space X, a covering space over X determines its monodromy functor from the fundamental groupoid of X to types. A map of covering spaces restricts on every fibre and therefore induces a natural transformation of monodromy functors. This file assembles those object- and morphism-level constructions into a functor on TauCeti.CoveringSpace X.

The resulting functor is faithful: a map over X is determined by all of its restrictions to the fibres. Over a locally path-connected base, its fullness is proved in TauCeti.Topology.Covering.Monodromy.Full, and its restriction from connected covers to fibrewise pretransitive actions is packaged in TauCeti.Topology.Covering.Monodromy.Connected. Over a path-connected, locally path-connected, semilocally simply connected base a connected cover can moreover be reconstructed from its action, which makes the connected restriction an equivalence (TauCeti.ConnectedCoveringSpace.monodromyEquivalence); the essential image over a general base is the remaining topological content of the classification of covering spaces by fundamental-groupoid actions.

Main declarations #

References #

This is the functor-construction step in Stage 2, item 8 of TauCetiRoadmap/UniversalCovers/README.md. It reuses Mathlib's object-level IsCoveringMap.monodromyFunctor and Tau Ceti's functoriality of monodromy under maps of covering spaces.

source
noncomputable def TauCeti.CoveringSpace.monodromyFunctor (X : TopCat) :
CategoryTheory.Functor (CoveringSpace X) (CategoryTheory.Functor (FundamentalGroupoid ↑X) (Type u))

Monodromy as a functor from covering spaces over X to functors from the fundamental groupoid of X to types.

A covering space is sent to its own monodromy functor, and a map of covering spaces to the natural transformation restricting that map to every fibre. Its object and map values are characterized by monodromyFunctor_obj, monodromyFunctor_map, and monodromyFunctor_map_app; the definition is @[expose]d so that those equations also hold by rfl in downstream modules.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.CoveringSpace.monodromyFunctor_obj {X : TopCat} (p : CoveringSpace X) :
    (monodromyFunctor X).obj p = ⋯.monodromyFunctor
    source
    theorem TauCeti.CoveringSpace.monodromyFunctor_map {X : TopCat} {p q : CoveringSpace X} (f : p ⟶ q) :
    (monodromyFunctor X).map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (⋯.monodromyNatTrans ⋯ (TopCat.Hom.hom (CategoryTheory.Over.Hom.left f.hom)) ⋯) (CategoryTheory.eqToHom ⋯))

    After transporting along the object equations, the natural transformation assigned to a map of covering spaces is the one induced by its underlying map of total spaces.

    source
    @[simp]
    theorem TauCeti.CoveringSpace.monodromyFunctor_map_app {X : TopCat} {p q : CoveringSpace X} (f : p ⟶ q) (x : ↑X) :
    ((monodromyFunctor X).map f).app { as := x } = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (TypeCat.ofHom (Function.fiberMap ⇑(TopCat.Hom.hom (CategoryTheory.Over.Hom.left f.hom)) ⋯ x)) (CategoryTheory.eqToHom ⋯))

    After transporting along the object equations, the natural transformation assigned by monodromy at a base point is the restriction of the underlying map of total spaces to the corresponding fibre.

    source
    instance TauCeti.CoveringSpace.monodromyFunctor_faithful (X : TopCat) :
    (monodromyFunctor X).Faithful

    The monodromy functor is faithful: a map of covering spaces is determined by its restrictions to all fibres.