Monodromy of connected covering spaces

For a locally path-connected base X, the monodromy functor of a connected covering space is pretransitive on every fibre: any two points over the same basepoint differ by transport along a loop. This file packages that condition as a full subcategory of fundamental-groupoid actions and lifts covering-space monodromy to it.

The word pretransitive follows Mathlib's convention: the condition allows an empty fibre. This matters over a disconnected base, since a connected cover can have image in only one component. On every nonempty fibre the condition is ordinary transitivity. Keeping the fibrewise formulation, rather than evaluating at one chosen basepoint, also retains the full information of a cover when the base is disconnected.

Main declarations

• TauCeti.FundamentalGroupoidAction.isFiberwisePretransitive: the property that the loop morphisms at each object act pretransitively on that object's value.
• TauCeti.PretransitiveFundamentalGroupoidAction: the full subcategory of functors satisfying that property.
• TauCeti.ConnectedCoveringSpace.isPretransitive_fiberAction: pretransitivity of Mathlib's IsCoveringMap.fundamentalGroupMulAction on the fibre over a basepoint.
• TauCeti.ConnectedCoveringSpace.monodromyFunctor: monodromy of connected covers, valued in fibrewise pretransitive fundamental-groupoid actions.
• TauCeti.ConnectedCoveringSpace.monodromyFunctor_faithful and monodromyFunctor_full: the lifted functor remains fully faithful.

References

This is the connected/transitive restriction in Stage 2, item 8 of TauCetiRoadmap/UniversalCovers/README.md. It uses Mathlib's local-homeomorphism charts and Tau Ceti's existing monodromy transitivity and full-faithfulness results. No Mathlib proof is vendored.

def TauCeti.FundamentalGroupoidAction.isFiberwisePretransitive (X : TopCat) : CategoryTheory.ObjectProperty (CategoryTheory.Functor (FundamentalGroupoid ↑X) (Type u))

A fundamental-groupoid action is fibrewise pretransitive if, at every basepoint, its loop morphisms carry any element of the fibre to any other element of that fibre.

Equations

• TauCeti.FundamentalGroupoidAction.isFiberwisePretransitive X F = ∀ (x : FundamentalGroupoid ↑X) (a b : F.obj x), ∃ (γ : x ⟶ x), (CategoryTheory.ConcreteCategory.hom (F.map γ)) a = b

@[simp]

theorem TauCeti.FundamentalGroupoidAction.isFiberwisePretransitive_iff (X : TopCat) (F : CategoryTheory.Functor (FundamentalGroupoid ↑X) (Type u)) : isFiberwisePretransitive X F ↔ ∀ (x : FundamentalGroupoid ↑X) (a b : F.obj x), ∃ (γ : x ⟶ x), (CategoryTheory.ConcreteCategory.hom (F.map γ)) a = b

Membership in the fibrewise pretransitive fundamental-groupoid action property.

instance TauCeti.FundamentalGroupoidAction.instIsClosedUnderIsomorphismsFunctorFundamentalGroupoidCarrierTypeIsFiberwisePretransitive (X : TopCat) : (isFiberwisePretransitive X).IsClosedUnderIsomorphisms

Fibrewise pretransitivity is preserved by natural isomorphisms of actions.

@[reducible, inline]

abbrev TauCeti.PretransitiveFundamentalGroupoidAction (X : TopCat) : Type (u + 1)

Fundamental-groupoid actions that are pretransitive on every fibre. Morphisms are arbitrary natural transformations between the underlying functors.

Equations

• TauCeti.PretransitiveFundamentalGroupoidAction X = (TauCeti.FundamentalGroupoidAction.isFiberwisePretransitive X).FullSubcategory

@[reducible, inline]

noncomputable abbrev TauCeti.PretransitiveFundamentalGroupoidAction.forget (X : TopCat) : CategoryTheory.Functor (PretransitiveFundamentalGroupoidAction X) (CategoryTheory.Functor (FundamentalGroupoid ↑X) (Type u))

The fully faithful inclusion into all fundamental-groupoid actions.

Equations

• TauCeti.PretransitiveFundamentalGroupoidAction.forget X = (TauCeti.FundamentalGroupoidAction.isFiberwisePretransitive X).ι

noncomputable def TauCeti.PretransitiveFundamentalGroupoidAction.mk {X : TopCat} (F : CategoryTheory.Functor (FundamentalGroupoid ↑X) (Type u)) (hF : FundamentalGroupoidAction.isFiberwisePretransitive X F) : PretransitiveFundamentalGroupoidAction X

Construct a fibrewise pretransitive fundamental-groupoid action from an action and a proof of fibrewise pretransitivity.

Equations

• TauCeti.PretransitiveFundamentalGroupoidAction.mk F hF = { obj := F, property := hF }

theorem TauCeti.PretransitiveFundamentalGroupoidAction.isFiberwisePretransitive {X : TopCat} (F : PretransitiveFundamentalGroupoidAction X) : FundamentalGroupoidAction.isFiberwisePretransitive X F.obj

The underlying action of a fibrewise pretransitive fundamental-groupoid action satisfies fibrewise pretransitivity.

noncomputable def TauCeti.PretransitiveFundamentalGroupoidAction.fullyFaithfulForget (X : TopCat) : (forget X).FullyFaithful

The inclusion into all fundamental-groupoid actions is fully faithful.

Equations

• TauCeti.PretransitiveFundamentalGroupoidAction.fullyFaithfulForget X = (TauCeti.FundamentalGroupoidAction.isFiberwisePretransitive X).fullyFaithfulι

theorem TauCeti.ConnectedCoveringSpace.monodromy_isFiberwisePretransitive {X : TopCat} [LocallyPathConnectedSpace ↑X] (p : ConnectedCoveringSpace X) : FundamentalGroupoidAction.isFiberwisePretransitive X ((CoveringSpace.monodromyFunctor X).obj ((forget X).obj p))

The ordinary monodromy functor of a connected cover is pretransitive on every fibre.

theorem TauCeti.ConnectedCoveringSpace.isPretransitive_fiberAction {X : TopCat} [LocallyPathConnectedSpace ↑X] (p : ConnectedCoveringSpace X) (x₀ : ↑X) : MulAction.IsPretransitive (FundamentalGroup (↑X) x₀) ↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj p)) ⁻¹' {x₀})

The fundamental group at x₀ acts pretransitively on the fibre of a connected covering space over x₀; the fibre may be empty, when the base is disconnected.

This is IsCoveringMap.monodromy_isPretransitive applied to the total space, which is path connected because a connected cover of a locally path-connected base is connected and locally path connected.

noncomputable def TauCeti.ConnectedCoveringSpace.monodromyFunctor (X : TopCat) [LocallyPathConnectedSpace ↑X] : CategoryTheory.Functor (ConnectedCoveringSpace X) (PretransitiveFundamentalGroupoidAction X)

Monodromy as a functor from connected covering spaces over X to fibrewise pretransitive fundamental-groupoid actions.

The underlying action is the ordinary covering-space monodromy functor, and the underlying map of every morphism is its fibrewise natural transformation.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.ConnectedCoveringSpace.monodromyFunctorCompForgetIso {X : TopCat} [LocallyPathConnectedSpace ↑X] : (monodromyFunctor X).comp (PretransitiveFundamentalGroupoidAction.forget X) ≅ (forget X).comp (CoveringSpace.monodromyFunctor X)

Forgetting fibrewise pretransitivity recovers the ordinary monodromy functor after including connected covers into all covers.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ConnectedCoveringSpace.monodromyFunctor_obj_obj {X : TopCat} [LocallyPathConnectedSpace ↑X] (p : ConnectedCoveringSpace X) : ((monodromyFunctor X).obj p).obj = (CoveringSpace.monodromyFunctor X).obj ((forget X).obj p)

The underlying action of connected-cover monodromy is the ordinary monodromy action.

@[simp]

theorem TauCeti.ConnectedCoveringSpace.monodromyFunctor_map_hom {X : TopCat} [LocallyPathConnectedSpace ↑X] {p q : ConnectedCoveringSpace X} (f : p ⟶ q) : ((monodromyFunctor X).map f).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((CoveringSpace.monodromyFunctor X).map ((forget X).map f)) (CategoryTheory.eqToHom ⋯))

The underlying natural transformation assigned to a map of connected covers is the one assigned by ordinary covering-space monodromy.

instance TauCeti.ConnectedCoveringSpace.monodromyFunctor_faithful {X : TopCat} [LocallyPathConnectedSpace ↑X] : (monodromyFunctor X).Faithful

Connected-cover monodromy is faithful.

instance TauCeti.ConnectedCoveringSpace.monodromyFunctor_full {X : TopCat} [LocallyPathConnectedSpace ↑X] : (monodromyFunctor X).Full

Over a locally path-connected base, connected-cover monodromy is full.