The covering associated to a subgroup

For a subgroup H ≤ π₁(X, x₀), UniversalCover.SubgroupQuotient x₀ H is already defined as the orbit quotient of the universal cover by H, and UniversalCover.subgroupQuotientProj is its descended endpoint projection. This file proves that the descended projection is a covering map.

The proof restricts UniversalCover.proj to the path component of x₀, where it and UniversalCover.subgroupQuotientMap are quotient covering maps for π₁(X, x₀) and H respectively. IsQuotientCoveringMap.isCoveringMap_of_comp makes the descended map to that component a covering map. Since locally path-connected spaces have clopen path components, composing with the inclusion gives a covering map to X, with empty fibres over the other components.

The conclusion is not inherited formally from the two quotient maps being covering maps: the deck group of UniversalCover x₀ / H over X is the normalizer quotient N(H) / H, which is transitive on the fibres only for normal H, so the descended projection is generally not itself a quotient covering map for any group.

Main declarations

• TauCeti.UniversalCover.isCoveringMap_subgroupQuotientProj: the cover associated to H ≤ π₁(X, x₀) is a covering space of X.
• TauCeti.UniversalCover.subgroupCover: the same cover, bundled as a connected covering space.
• TauCeti.UniversalCover.subgroupCoverBasepointFiber: its distinguished fibre point.
• TauCeti.UniversalCover.subgroupQuotientTopHomeomorph: the cover associated to the whole fundamental group is X itself.

References

This completes the existence half in TauCetiRoadmap/UniversalCovers/README.md, Stage 2, item 7: construct the pointed connected cover UniversalCover x₀ / H. It uses the universal cover adapted from Kim Morrison's mathlib4#38292 and Mathlib's quotient-covering-map interface due to Junyan Xu.

theorem TauCeti.UniversalCover.isCoveringMap_subgroupQuotientProj {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) : IsCoveringMap (subgroupQuotientProj x₀ H)

The endpoint projection on the quotient of the universal cover by H is a covering map.

theorem TauCeti.UniversalCover.locallyPathConnectedSpace_subgroupQuotient {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) : LocallyPathConnectedSpace (SubgroupQuotient x₀ H)

The quotient of the universal cover by a subgroup is locally path-connected, being the total space of a covering space of the locally path-connected base X.

noncomputable def TauCeti.UniversalCover.subgroupCover {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) : ConnectedCoveringSpace ↧X

The connected covering space associated to a subgroup H ≤ π₁(X, x₀), obtained by quotienting the universal cover by H. Its fibres outside the path component of x₀ are empty, so the base need not be path-connected.

Equations

• TauCeti.UniversalCover.subgroupCover x₀ H = TauCeti.ConnectedCoveringSpace.mk (TopCat.ofHom { toFun := TauCeti.UniversalCover.subgroupQuotientProj x₀ H, continuous_toFun := ⋯ }) ⋯

@[simp]

theorem TauCeti.UniversalCover.subgroupCover_coe {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) : (subgroupCover x₀ H).obj.left = ↧(SubgroupQuotient x₀ H)

The total space of the cover associated to H is the quotient of the universal cover by H.

@[simp]

theorem TauCeti.UniversalCover.subgroupCover_proj {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) : CoveringSpace.FullSubcategory.proj (subgroupCover x₀ H) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (TopCat.ofHom { toFun := subgroupQuotientProj x₀ H, continuous_toFun := ⋯ })

The projection of the cover associated to H is the descended endpoint projection.

noncomputable def TauCeti.UniversalCover.subgroupCoverTotalSpaceHomeomorph {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) : ↑(subgroupCover x₀ H).obj.left ≃ₜ SubgroupQuotient x₀ H

The characteristic equality of total spaces for subgroupCover, viewed as a homeomorphism.

Equations

• TauCeti.UniversalCover.subgroupCoverTotalSpaceHomeomorph x₀ H = TopCat.homeoOfIso (CategoryTheory.eqToIso ⋯)

theorem TauCeti.UniversalCover.subgroupQuotientProj_subgroupCoverTotalSpaceHomeomorph {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) (e : ↑(subgroupCover x₀ H).obj.left) : subgroupQuotientProj x₀ H ((subgroupCoverTotalSpaceHomeomorph x₀ H) e) = (CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj (subgroupCover x₀ H))) e

The characteristic total-space homeomorphism commutes with the two projections.

noncomputable def TauCeti.UniversalCover.subgroupCoverFiberEquivSubgroupQuotient {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) : ↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj (subgroupCover x₀ H))) ⁻¹' {x₀}) ≃ ↑(subgroupQuotientProj x₀ H ⁻¹' {x₀})

Transport from the fibre of the bundled subgroup cover to the fibre of its quotient projection.

Equations

• TauCeti.UniversalCover.subgroupCoverFiberEquivSubgroupQuotient x₀ H = ((TauCeti.UniversalCover.subgroupCoverTotalSpaceHomeomorph x₀ H).subtype ⋯).toEquiv

@[simp]

theorem TauCeti.UniversalCover.subgroupCoverFiberEquivSubgroupQuotient_apply_monodromy {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) (g : FundamentalGroup X x₀) (e : ↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj (subgroupCover x₀ H))) ⁻¹' {x₀})) : (subgroupCoverFiberEquivSubgroupQuotient x₀ H) (⋯.monodromy g e) = ⋯.monodromy g ((subgroupCoverFiberEquivSubgroupQuotient x₀ H) e)

Fibre transport commutes with monodromy.

noncomputable def TauCeti.UniversalCover.subgroupCoverBasepointFiber {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) : ↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj (subgroupCover x₀ H))) ⁻¹' {x₀})

The distinguished point in the fibre over x₀ of the cover associated to H.

Equations

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

@[simp]

theorem TauCeti.UniversalCover.subgroupCoverFiberEquivSubgroupQuotient_apply_basepoint {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) : (subgroupCoverFiberEquivSubgroupQuotient x₀ H) (subgroupCoverBasepointFiber x₀ H) = SubgroupQuotient.basepointFiber x₀ H

Fibre transport identifies the bundled distinguished point with the quotient distinguished point.

noncomputable def TauCeti.UniversalCover.subgroupQuotientTopHomeomorph {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [PathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) : SubgroupQuotient x₀ ⊤ ≃ₜ X

The cover associated to the whole fundamental group is X itself. The comparison is the descended endpoint projection, so this cover is the trivial one-sheeted cover.

Equations

• TauCeti.UniversalCover.subgroupQuotientTopHomeomorph x₀ = (Equiv.ofBijective (TauCeti.UniversalCover.subgroupQuotientProj x₀ ⊤) ⋯).toHomeomorphOfContinuousOpen ⋯ ⋯

@[simp]

theorem TauCeti.UniversalCover.coe_subgroupQuotientTopHomeomorph {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [PathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) : ⇑(subgroupQuotientTopHomeomorph x₀) = subgroupQuotientProj x₀ ⊤