The subgroup recovered from a universal-cover quotient

For H ≤ π₁(X, x₀), the orbit quotient UniversalCover x₀ / H has a distinguished point represented by the constant path. The quotient map from the universal cover is a quotient covering map with acting group H; since the universal cover is simply connected, this gives

π₁(UniversalCover x₀ / H) ≃* Hᵐᵒᵖ.

The endpoint projection descends from the universal cover to the orbit quotient. This file computes its induced fundamental-group homomorphism and proves that its range is exactly H. The computation contains an inverse because the project uses a left action in which a loop class acts on the universal cover by prepending its inverse.

This proves the subgroup-recovery part of TauCetiRoadmap/UniversalCovers/README.md, Stage 2, item 7: for the pointed quotient associated to H, prove p_*(π₁(–)) = H. It reuses the fundamental-group action adapted from Kim Morrison's work in mathlib4#38292 and Mathlib's quotient-cover monodromy comparison due to Junyan Xu. No Mathlib code is vendored.

Main declarations

• TauCeti.UniversalCover.SubgroupQuotient.basepointLift: the constant-path lift of the distinguished quotient point.
• TauCeti.UniversalCover.SubgroupQuotient.fundamentalGroupEquiv and TauCeti.UniversalCover.SubgroupQuotient.fundamentalGroupEquiv_unop_smul: the fundamental group of the quotient is the opposite of H, compatibly with monodromy.
• TauCeti.UniversalCover.mapOfEq_subgroupQuotientProj_apply: the descended endpoint map sends a quotient loop to the inverse of its corresponding element of H.
• TauCeti.UniversalCover.range_mapOfEq_subgroupQuotientProj: the descended endpoint map recovers exactly H.

def TauCeti.UniversalCover.SubgroupQuotient.basepointLift {X : Type u_1} [TopologicalSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) : ↑(subgroupQuotientMap x₀ H ⁻¹' {basepoint x₀ H})

The constant-path lift of the distinguished point of the subgroup quotient.

Equations

• TauCeti.UniversalCover.SubgroupQuotient.basepointLift x₀ H = ⟨↑(TauCeti.UniversalCover.basepointLift x₀), ⋯⟩

@[simp]

theorem TauCeti.UniversalCover.SubgroupQuotient.basepointLift_coe {X : Type u_1} [TopologicalSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) : ↑(basepointLift x₀ H) = ↑(UniversalCover.basepointLift x₀)

The underlying universal-cover point of the distinguished lift is the constant-path point.

noncomputable def TauCeti.UniversalCover.SubgroupQuotient.fundamentalGroupEquiv {X : Type u_1} [TopologicalSpace X] (x₀ : X) [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (H : Subgroup (FundamentalGroup X x₀)) : FundamentalGroup (SubgroupQuotient x₀ H) (basepoint x₀ H) ≃* (↥H)ᵐᵒᵖ

The fundamental group of the subgroup quotient at its distinguished point is the opposite of the acting subgroup. The opposite records the left-action convention used by quotient-cover monodromy.

Equations

• TauCeti.UniversalCover.SubgroupQuotient.fundamentalGroupEquiv x₀ H = ⋯.fundamentalGroupEquiv (TauCeti.UniversalCover.SubgroupQuotient.basepointLift x₀ H)

@[simp]

theorem TauCeti.UniversalCover.SubgroupQuotient.fundamentalGroupEquiv_unop_smul {X : Type u_1} [TopologicalSpace X] (x₀ : X) [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (H : Subgroup (FundamentalGroup X x₀)) (g : FundamentalGroup (SubgroupQuotient x₀ H) (basepoint x₀ H)) : MulOpposite.unop ((fundamentalGroupEquiv x₀ H) g) • { proj := x₀, path := Path.Homotopic.Quotient.refl x₀ } = ↑(⋯.monodromy g (basepointLift x₀ H))

The subgroup element assigned to a quotient loop moves the distinguished lift to the endpoint of that loop's monodromy lift.

@[simp]

theorem TauCeti.UniversalCover.mapOfEq_subgroupQuotientProj_apply {X : Type u_1} [TopologicalSpace X] (x₀ : X) [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (H : Subgroup (FundamentalGroup X x₀)) (g : FundamentalGroup (SubgroupQuotient x₀ H) (SubgroupQuotient.basepoint x₀ H)) : (FundamentalGroup.mapOfEq { toFun := subgroupQuotientProj x₀ H, continuous_toFun := ⋯ } ⋯) g = (↑(MulOpposite.unop ((SubgroupQuotient.fundamentalGroupEquiv x₀ H) g)))⁻¹

The descended endpoint map sends a quotient loop to the inverse of the corresponding element of the acting subgroup. The inverse is forced by the left-action convention.

theorem TauCeti.UniversalCover.range_mapOfEq_subgroupQuotientProj {X : Type u_1} [TopologicalSpace X] (x₀ : X) [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (H : Subgroup (FundamentalGroup X x₀)) : (FundamentalGroup.mapOfEq { toFun := subgroupQuotientProj x₀ H, continuous_toFun := ⋯ } ⋯).range = H

The subgroup induced by the descended endpoint map is exactly the subgroup used to form the orbit quotient.