The deck group of the cover attached to a subgroup

For H ≤ π₁(X, x₀), the orbit quotient UniversalCover x₀ / H is a covering space of X through UniversalCover.subgroupQuotientProj. This file computes its deck transformation group:

deck (subgroupQuotientProj x₀ H) ≃* N(H) ⧸ H,

and, when H is normal, deck (subgroupQuotientProj x₀ H) ≃* π₁(X, x₀) ⧸ H. Both are the specialisation to the universal cover of TauCeti.Deck.IsQuotientCoveringMap.normalizerQuotientDeckMulEquiv.

The isomorphism is stated for the left action of π₁(X, x₀) on the universal cover, in which a loop class acts by prepending its inverse; this is the same convention as TauCeti.Deck.IsQuotientCoveringMap.deckMulEquiv, and it is why no ᵐᵒᵖ appears here, unlike in the monodromy identification UniversalCover.deckFundamentalGroupEquiv.

Taking H = ⊥ recovers the deck group of the universal cover itself; taking H normal and H = ⊥ gives π₁(X, x₀) again.

Main declarations

• TauCeti.UniversalCover.deckSubgroupQuotientProjEquiv: the deck group of the cover attached to H is N(H) ⧸ H.
• TauCeti.UniversalCover.deckSubgroupQuotientProjEquivOfNormal: for normal H this reads π₁(X, x₀) ⧸ H.

References

It consumes the based-path universal cover adapted from Kim Morrison's mathlib4#38292, Mathlib's quotient-covering-map interface due to Junyan Xu, and the covering-map property of subgroupQuotientProj proved in TauCeti.AlgebraicTopology.UniversalCover.Classification.Existence.

noncomputable def TauCeti.UniversalCover.deckSubgroupQuotientProjEquiv {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [PathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) : ↥(Subgroup.normalizer ↑H) ⧸ H.subgroupOf (Subgroup.normalizer ↑H) ≃* ↥(deck (subgroupQuotientProj x₀ H))

The deck group of the cover attached to H ≤ π₁(X, x₀) is the normalizer quotient N(H) ⧸ H. A normalizer class acts by descending its translation of the universal cover.

Equations

• TauCeti.UniversalCover.deckSubgroupQuotientProjEquiv x₀ H = TauCeti.Deck.IsQuotientCoveringMap.normalizerQuotientDeckMulEquiv ⋯ ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.UniversalCover.deckSubgroupQuotientProjEquiv_mk_apply {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [PathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) (g : ↥(Subgroup.normalizer ↑H)) (e : UniversalCover x₀) : ↑((deckSubgroupQuotientProjEquiv x₀ H) ↑g) (Quotient.mk'' e) = Quotient.mk'' (↑g • e)

The normalizer class of g acts on the cover attached to H by sending the class of e to the class of g • e.

@[simp]

theorem TauCeti.UniversalCover.deckSubgroupQuotientProjEquiv_mk_symm_apply {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [PathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) (g : ↥(Subgroup.normalizer ↑H)) (e : UniversalCover x₀) : (↑((deckSubgroupQuotientProjEquiv x₀ H) ↑g)).symm (Quotient.mk'' e) = Quotient.mk'' ((↑g)⁻¹ • e)

The inverse of the deck transformation attached to the normalizer class of g sends the class of e to the class of g⁻¹ • e.

noncomputable def TauCeti.UniversalCover.deckSubgroupQuotientProjEquivOfNormal {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [PathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) [H.Normal] : FundamentalGroup X x₀ ⧸ H ≃* ↥(deck (subgroupQuotientProj x₀ H))

For a normal subgroup H ◁ π₁(X, x₀), the deck group of the cover attached to H is π₁(X, x₀) ⧸ H, so that cover is regular.

Equations

• TauCeti.UniversalCover.deckSubgroupQuotientProjEquivOfNormal x₀ H = TauCeti.Deck.IsQuotientCoveringMap.quotientDeckMulEquivOfNormal ⋯ ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.UniversalCover.deckSubgroupQuotientProjEquivOfNormal_mk_apply {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [PathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) [H.Normal] (g : FundamentalGroup X x₀) (e : UniversalCover x₀) : ↑((deckSubgroupQuotientProjEquivOfNormal x₀ H) ↑g) (Quotient.mk'' e) = Quotient.mk'' (g • e)

For normal H, the class of g acts on the cover attached to H by sending the class of e to the class of g • e.

@[simp]

theorem TauCeti.UniversalCover.deckSubgroupQuotientProjEquivOfNormal_mk_symm_apply {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [PathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) [H.Normal] (g : FundamentalGroup X x₀) (e : UniversalCover x₀) : (↑((deckSubgroupQuotientProjEquivOfNormal x₀ H) ↑g)).symm (Quotient.mk'' e) = Quotient.mk'' (g⁻¹ • e)

For normal H, the inverse of the deck transformation attached to the class of g sends the class of e to the class of g⁻¹ • e.