Documentation

TauCeti.AlgebraicTopology.UniversalCover.Classification.MonodromyEquivalence

Covers are classified by fundamental-groupoid actions #

Let X be path connected, locally path connected and semilocally simply connected. This file proves that monodromy

TauCeti.ConnectedCoveringSpace.transitiveMonodromyFunctor X : ConnectedCoveringSpace X ⥤ TransitiveFundamentalGroupoidAction X

is an equivalence of categories. Full faithfulness is already available: it is the lifting criterion, packaged in TauCeti.Topology.Covering.Monodromy.Connected. What is proved here is essential surjectivity, which is the reconstruction of a cover from an action.

The reconstruction has two steps. A fibrewise transitive action F restricts at a basepoint x₀ to a transitive, nonempty action of π₁(X, x₀) on F.obj x₀; quotienting the universal cover by the stabiliser of a point of that set produces a connected cover whose fibre over x₀ is equivariantly equivalent to F.obj x₀, which is TauCeti.UniversalCover.transitiveActionFiberEquiv. That is an isomorphism of the two actions at one object only. The second step upgrades it to a natural isomorphism of functors on the whole fundamental groupoid, by TauCeti.Groupoid.natIsoOfEnd: a path from x₀ transports the equivalence to any other point, and the transported equivalence does not depend on the path precisely because the two choices differ by a loop, on which equivariance applies.

Both hypotheses beyond local path-connectedness are used, and neither is an artefact. Path connectedness makes the fundamental groupoid connected, which is what the transport needs, and it is also what makes the fibres of a connected cover nonempty; semilocal simple connectedness is what produces the universal cover the reconstruction quotients.

Dropping both restrictions — connectedness of the cover, transitivity of the action — gives the classification of all covering spaces of X by all functors from its fundamental groupoid to types. Full faithfulness is again the lifting criterion, already packaged in TauCeti.Topology.Covering.Monodromy.Basic and …Monodromy.Full, and essential surjectivity is again reconstruction at x₀ followed by transport, but the cover reconstructed from an arbitrary π₁(X, x₀)-set is the balanced product of TauCeti.AlgebraicTopology.UniversalCover.Classification.ActionCover rather than a quotient of the universal cover by a stabiliser: the latter is connected, so it can only realise a transitive action, while the former realises the disjoint union of one such quotient per orbit in one step.

Main declarations #

References #

This completes the alternative monodromy-functor lens on Stage 2, item 8 of TauCetiRoadmap/UniversalCovers/README.md, which asks for the classification of connected covers by transitive π₁(X)-sets and of covers in general by functors out of the fundamental groupoid; see Hatcher, Algebraic Topology, Section 1.3. It consumes the based-path universal cover adapted from Kim Morrison's mathlib4#38292, the stabiliser-cover reconstruction of TauCeti.AlgebraicTopology.UniversalCover.Classification.Reconstruction, and the balanced-product cover of TauCeti.AlgebraicTopology.UniversalCover.Classification.ActionCover.

source
@[instance_reducible]
def TauCeti.FundamentalGroupoidAction.basepointMulAction {X : Type u} [TopologicalSpace X] (F : CategoryTheory.Functor (FundamentalGroupoid X) (Type u)) (x₀ : X) :
MulAction (FundamentalGroup X x₀) (F.obj { as := x₀ })

The value of a fundamental-groupoid action at x₀ carries an action of π₁(X, x₀), the vertex group of the fundamental groupoid at x₀.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.FundamentalGroupoidAction.basepointMulAction_smul {X : Type u} [TopologicalSpace X] (F : CategoryTheory.Functor (FundamentalGroupoid X) (Type u)) (x₀ : X) (g : FundamentalGroup X x₀) (a : F.obj { as := x₀ }) :
    g • a = (CategoryTheory.ConcreteCategory.hom (F.map g)) a
    source
    theorem TauCeti.ConnectedCoveringSpace.exists_monodromyFunctor_iso {X : TopCat} [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] (F : CategoryTheory.Functor (FundamentalGroupoid ↑X) (Type u)) (hF : FundamentalGroupoidAction.isFiberwiseTransitive X F) :
    ∃ (p : ConnectedCoveringSpace X), Nonempty ((CoveringSpace.monodromyFunctor X).obj ((forget X).obj p) ≅ F)

    Every fibrewise transitive fundamental-groupoid action is the monodromy of a connected covering space. The cover is the quotient of the universal cover by the stabiliser of a point in the value of the action at a basepoint.

    source
    instance TauCeti.ConnectedCoveringSpace.transitiveMonodromyFunctor_essSurj {X : TopCat} [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] :
    (transitiveMonodromyFunctor X).EssSurj

    Transitive connected-cover monodromy is essentially surjective.

    source
    instance TauCeti.ConnectedCoveringSpace.transitiveMonodromyFunctor_isEquivalence {X : TopCat} [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] :
    (transitiveMonodromyFunctor X).IsEquivalence

    Transitive connected-cover monodromy is fully faithful and essentially surjective.

    source
    noncomputable def TauCeti.ConnectedCoveringSpace.monodromyEquivalence (X : TopCat) [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] :
    ConnectedCoveringSpace X ≌ TransitiveFundamentalGroupoidAction X

    The classification of connected covering spaces by transitive fundamental-groupoid actions. Over a path-connected, locally path-connected, semilocally simply connected base, monodromy is an equivalence from connected covering spaces to fibrewise transitive actions of the fundamental groupoid.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.ConnectedCoveringSpace.monodromyEquivalence_functor (X : TopCat) [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] :
      (monodromyEquivalence X).functor = transitiveMonodromyFunctor X
      source
      theorem TauCeti.CoveringSpace.exists_monodromyFunctor_iso {X : TopCat} [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] (F : CategoryTheory.Functor (FundamentalGroupoid ↑X) (Type u)) :
      ∃ (p : CoveringSpace X), Nonempty ((monodromyFunctor X).obj p ≅ F)

      Every fundamental-groupoid action is the monodromy of a covering space. The cover is the balanced product of the universal cover with the value of the action at a basepoint.

      source
      instance TauCeti.CoveringSpace.monodromyFunctor_essSurj {X : TopCat} [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] :
      (monodromyFunctor X).EssSurj

      Covering-space monodromy is essentially surjective.

      source
      instance TauCeti.CoveringSpace.monodromyFunctor_isEquivalence {X : TopCat} [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] :
      (monodromyFunctor X).IsEquivalence

      Covering-space monodromy is fully faithful and essentially surjective.

      source
      noncomputable def TauCeti.CoveringSpace.monodromyEquivalence (X : TopCat) [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] :
      CoveringSpace X ≌ CategoryTheory.Functor (FundamentalGroupoid ↑X) (Type u)

      The classification of covering spaces by fundamental-groupoid actions. Over a path-connected, locally path-connected, semilocally simply connected base, monodromy is an equivalence from covering spaces to functors from the fundamental groupoid to types.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.CoveringSpace.monodromyEquivalence_functor (X : TopCat) [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] :
        (monodromyEquivalence X).functor = monodromyFunctor X