Monodromy of connected covers over a path-connected base

Over a path-connected base the fibres of a connected covering space are nonempty, so its monodromy action is transitive on each fibre and not merely pretransitive. This file records that strengthening and lifts the monodromy functor of connected covers to the full subcategory of fibrewise transitive fundamental-groupoid actions.

The distinction is not cosmetic. Over a base with several path components a connected cover has its image in one of them, so its fibres over the other components are empty, which is why TauCeti.FundamentalGroupoidAction.isFiberwisePretransitive is the right condition there and is what TauCeti.ConnectedCoveringSpace.monodromyFunctor is stated against. Once the base is path connected the empty action drops out of the essential image, and it has to: the empty action is fibrewise pretransitive, while TauCeti.ConnectedCoveringSpace carries ConnectedSpace and so has a nonempty total space. Transitivity is therefore exactly the extra condition that makes monodromy an equivalence onto the actions, which is proved in TauCeti.AlgebraicTopology.UniversalCover.Classification.MonodromyEquivalence.

Main declarations

• TauCeti.FundamentalGroupoidAction.isFiberwiseTransitive: fibrewise pretransitive with nonempty fibres.
• TauCeti.TransitiveFundamentalGroupoidAction: the corresponding full subcategory.
• TauCeti.ConnectedCoveringSpace.nonempty_fiber: over a preconnected base every fibre of a connected cover is nonempty.
• TauCeti.ConnectedCoveringSpace.transitiveMonodromyFunctor: monodromy of connected covers, valued in fibrewise transitive actions.

References

This is the connected/transitive restriction in Stage 2, item 8 of TauCetiRoadmap/UniversalCovers/README.md, which asks for the classification of connected covers by transitive fundamental-group sets. It builds on the fibrewise pretransitive packaging in TauCeti.Topology.Covering.Monodromy.Connected.

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

A fundamental-groupoid action is fibrewise nonempty if every fibre is nonempty.

Equations

• TauCeti.FundamentalGroupoidAction.isFiberwiseNonempty X F = ∀ (x : FundamentalGroupoid ↑X), Nonempty (F.obj x)

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

A fundamental-groupoid action is fibrewise transitive if it is fibrewise pretransitive with nonempty fibres.

Equations

• TauCeti.FundamentalGroupoidAction.isFiberwiseTransitive X = TauCeti.FundamentalGroupoidAction.isFiberwisePretransitive X ⊓ TauCeti.FundamentalGroupoidAction.isFiberwiseNonempty X

@[simp]

theorem TauCeti.FundamentalGroupoidAction.isFiberwiseTransitive_iff {X : TopCat} (F : CategoryTheory.Functor (FundamentalGroupoid ↑X) (Type u)) : isFiberwiseTransitive X F ↔ isFiberwisePretransitive X F ∧ ∀ (x : FundamentalGroupoid ↑X), Nonempty (F.obj x)

Membership in the fibrewise transitive fundamental-groupoid action property.

theorem TauCeti.FundamentalGroupoidAction.isFiberwisePretransitive_of_isFiberwiseTransitive {X : TopCat} {F : CategoryTheory.Functor (FundamentalGroupoid ↑X) (Type u)} (hF : isFiberwiseTransitive X F) : isFiberwisePretransitive X F

A fibrewise transitive action is fibrewise pretransitive.

theorem TauCeti.FundamentalGroupoidAction.nonempty_of_isFiberwiseTransitive {X : TopCat} {F : CategoryTheory.Functor (FundamentalGroupoid ↑X) (Type u)} (hF : isFiberwiseTransitive X F) (x : FundamentalGroupoid ↑X) : Nonempty (F.obj x)

Every fibre of a fibrewise transitive action is nonempty.

theorem TauCeti.FundamentalGroupoidAction.isFiberwiseTransitive_le (X : TopCat) : isFiberwiseTransitive X ≤ isFiberwisePretransitive X

Fibrewise transitivity is stronger than fibrewise pretransitivity.

instance TauCeti.FundamentalGroupoidAction.instIsClosedUnderIsomorphismsFunctorFundamentalGroupoidCarrierTypeIsFiberwiseNonempty (X : TopCat) : (isFiberwiseNonempty X).IsClosedUnderIsomorphisms

Fibrewise nonemptiness is preserved by natural isomorphisms of actions.

instance TauCeti.FundamentalGroupoidAction.instIsClosedUnderIsomorphismsFunctorFundamentalGroupoidCarrierTypeIsFiberwiseTransitive (X : TopCat) : (isFiberwiseTransitive X).IsClosedUnderIsomorphisms

Fibrewise transitivity is preserved by natural isomorphisms of actions.

@[reducible, inline]

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

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

Equations

• TauCeti.TransitiveFundamentalGroupoidAction X = (TauCeti.FundamentalGroupoidAction.isFiberwiseTransitive X).FullSubcategory

@[reducible, inline]

noncomputable abbrev TauCeti.TransitiveFundamentalGroupoidAction.forget (X : TopCat) : CategoryTheory.Functor (TransitiveFundamentalGroupoidAction X) (PretransitiveFundamentalGroupoidAction X)

The fully faithful inclusion into fibrewise pretransitive actions.

Equations

• TauCeti.TransitiveFundamentalGroupoidAction.forget X = CategoryTheory.ObjectProperty.ιOfLE ⋯

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

Construct a fibrewise transitive action from an action and a proof of fibrewise transitivity.

Equations

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

theorem TauCeti.TransitiveFundamentalGroupoidAction.isFiberwiseTransitive {X : TopCat} (F : TransitiveFundamentalGroupoidAction X) : FundamentalGroupoidAction.isFiberwiseTransitive X F.obj

The underlying action of a fibrewise transitive action is fibrewise transitive.

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

The inclusion into fibrewise pretransitive actions is fully faithful.

Equations

• TauCeti.TransitiveFundamentalGroupoidAction.fullyFaithfulForget X = CategoryTheory.ObjectProperty.fullyFaithfulιOfLE ⋯

theorem TauCeti.ConnectedCoveringSpace.nonempty_fiber {X : TopCat} [PreconnectedSpace ↑X] (p : ConnectedCoveringSpace X) (x : ↑X) : Nonempty ↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj p)) ⁻¹' {x})

Over a preconnected base, every fibre of a connected covering space is nonempty: its projection is surjective (IsCoveringMap.surjective).

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

The ordinary monodromy functor of a connected cover over a path-connected base is transitive on every fibre.

noncomputable def TauCeti.ConnectedCoveringSpace.transitiveMonodromyFunctor (X : TopCat) [LocallyPathConnectedSpace ↑X] [PathConnectedSpace ↑X] : CategoryTheory.Functor (ConnectedCoveringSpace X) (TransitiveFundamentalGroupoidAction X)

Monodromy as a functor from connected covering spaces over a path-connected base to fibrewise transitive fundamental-groupoid actions.

Equations

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

@[simp]

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

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

instance TauCeti.ConnectedCoveringSpace.transitiveMonodromyFunctor_faithful {X : TopCat} [LocallyPathConnectedSpace ↑X] [PathConnectedSpace ↑X] : (transitiveMonodromyFunctor X).Faithful

Transitive connected-cover monodromy is faithful.

instance TauCeti.ConnectedCoveringSpace.transitiveMonodromyFunctor_full {X : TopCat} [LocallyPathConnectedSpace ↑X] [PathConnectedSpace ↑X] : (transitiveMonodromyFunctor X).Full

Transitive connected-cover monodromy is full.