Deck transformations of the universal cover

For a path-connected, locally path-connected, semilocally simply connected space X, the endpoint projection from the based-path universal cover is regular. Indeed, the explicit fundamental-group action from UniversalCover.Action acts through deck transformations and is transitive on each fibre.

Combining this regularity with the simple connectedness of the universal cover and the generic regular-cover comparison gives the convention-correct form of the classical calculation

deck (UniversalCover.proj : UniversalCover x₀ → X) ≃* (FundamentalGroup X x₀)ᵐᵒᵖ.

The opposite is genuine: the fundamental group acts on the universal cover by prepending the inverse loop, while deck transformations are composed as homeomorphisms. This is the convention pinned by TauCeti.Deck.IsRegular.deckFundamentalGroupEquiv.

Main declarations

• TauCeti.UniversalCover.loopDeck: the deck transformation induced by a loop class.
• TauCeti.UniversalCover.isRegular_proj: regularity of the universal-cover projection.
• TauCeti.UniversalCover.deckFundamentalGroupEquiv: the deck group of the universal cover is the opposite fundamental group.

References

The construction uses the universal-cover action adapted from Kim Morrison's mathlib4 PR mathlib4#38292, and the generic comparison ultimately uses Junyan Xu's IsQuotientCoveringMap.fundamentalGroupEquiv from Mathlib.Topology.Homotopy.Lifting.

noncomputable def TauCeti.UniversalCover.loopDeck {X : Type u_1} [TopologicalSpace X] (x₀ : X) (g : FundamentalGroup X x₀) : ↥(deck proj)

A loop class acts on the universal cover by a deck transformation of the endpoint projection.

Equations

• TauCeti.UniversalCover.loopDeck x₀ g = ⟨Homeomorph.smul g, ⋯⟩

@[simp]

theorem TauCeti.UniversalCover.loopDeck_apply {X : Type u_1} [TopologicalSpace X] (x₀ : X) (g : FundamentalGroup X x₀) (p : UniversalCover x₀) : ↑(loopDeck x₀ g) p = g • p

The deck transformation induced by a loop class acts by the fundamental-group action.

@[simp]

theorem TauCeti.UniversalCover.loopDeck_one {X : Type u_1} [TopologicalSpace X] (x₀ : X) : loopDeck x₀ (CategoryTheory.CategoryStruct.id { as := x₀ }) = 1

The identity loop class induces the identity deck transformation.

@[simp]

theorem TauCeti.UniversalCover.loopDeck_mul {X : Type u_1} [TopologicalSpace X] (x₀ : X) (g h : FundamentalGroup X x₀) : loopDeck x₀ (CategoryTheory.CategoryStruct.comp h g) = loopDeck x₀ g * loopDeck x₀ h

Multiplication of loop classes corresponds to composition of their deck transformations.

noncomputable def TauCeti.UniversalCover.loopDeckHom {X : Type u_1} [TopologicalSpace X] (x₀ : X) : FundamentalGroup X x₀ →* ↥(deck proj)

The fundamental-group action, bundled as a homomorphism into the deck group of the universal-cover projection.

Equations

• TauCeti.UniversalCover.loopDeckHom x₀ = { toFun := TauCeti.UniversalCover.loopDeck x₀, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.UniversalCover.loopDeckHom_apply {X : Type u_1} [TopologicalSpace X] (x₀ : X) (g : FundamentalGroup X x₀) : (loopDeckHom x₀) g = loopDeck x₀ g

theorem TauCeti.UniversalCover.isRegular_proj {X : Type u_1} [TopologicalSpace X] (x₀ : X) [PathConnectedSpace X] : Deck.IsRegular proj

The endpoint projection of the universal cover has regular deck action.

noncomputable def TauCeti.UniversalCover.deckFundamentalGroupEquiv {X : Type u_1} [TopologicalSpace X] (x₀ : X) [LocallyPathConnectedSpace X] [PathConnectedSpace X] [SemilocallySimplyConnectedSpace X] : ↥(deck proj) ≃* (FundamentalGroup X x₀)ᵐᵒᵖ

The deck transformation group of the based-path universal cover is the opposite of the fundamental group of the base.

Equations

• TauCeti.UniversalCover.deckFundamentalGroupEquiv x₀ = ⋯.deckFundamentalGroupEquiv ⋯ (TauCeti.UniversalCover.basepointLift x₀)

@[simp]

theorem TauCeti.UniversalCover.deckFundamentalGroupEquiv_symm_op {X : Type u_1} [TopologicalSpace X] (x₀ : X) [LocallyPathConnectedSpace X] [PathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (g : FundamentalGroup X x₀) : (deckFundamentalGroupEquiv x₀).symm (MulOpposite.op g) = loopDeck x₀ g⁻¹

The inverse deck-to-fundamental-group equivalence recovers the explicit loop deck transformation, with the inverse forced by the left-action convention.