Documentation

TauCeti.AlgebraicTopology.UniversalCover.Classification.SubgroupQuotient

Quotients of the universal cover by subgroups #

For a subgroup H of the fundamental group of X, this file defines the orbit quotient UniversalCover x₀ / H. It equips that quotient with its canonical map from the universal cover and proves that this map is a quotient covering map. The class of the constant path supplies its distinguished point.

This is the first construction step in the subgroup-to-cover direction of the classification of covering spaces. This file descends UniversalCover.proj to the quotient; Classification.RecoveredSubgroup identifies the subgroup recovered by that map, while a later file will prove that the descended map is a covering map.

Main declarations #

References #

This advances TauCetiRoadmap/UniversalCovers/README.md, Stage 2, item 7: construct the pointed connected cover associated to H ≤ π₁(X, x₀). It reuses the fundamental-group action adapted from Kim Morrison's work in mathlib4#38292 and Mathlib's quotient-covering-map interface due to Junyan Xu.

source
@[reducible, inline]
abbrev TauCeti.UniversalCover.SubgroupQuotient {X : Type u_1} [TopologicalSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) :
Type u_1

The orbit quotient of the universal cover by a subgroup of the fundamental group.

Equations
Instances For
    source
    noncomputable def TauCeti.UniversalCover.SubgroupQuotient.basepoint {X : Type u_1} [TopologicalSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) :
    SubgroupQuotient x₀ H

    The distinguished point in the subgroup quotient, represented by the constant path at the basepoint.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.UniversalCover.SubgroupQuotient.basepoint_eq_mk {X : Type u_1} [TopologicalSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) :
      basepoint x₀ H = Quotient.mk'' { proj := x₀, path := Path.Homotopic.Quotient.refl x₀ }

      The distinguished point is the quotient class of the constant path at the basepoint.

      source
      noncomputable def TauCeti.UniversalCover.subgroupQuotientMap {X : Type u_1} [TopologicalSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) :
      UniversalCover x₀ → SubgroupQuotient x₀ H

      The canonical map from the universal cover to its orbit quotient by H.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.UniversalCover.subgroupQuotientMap_apply {X : Type u_1} [TopologicalSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) (e : UniversalCover x₀) :
        subgroupQuotientMap x₀ H e = Quotient.mk'' e

        The subgroup quotient map sends a representative to its quotient class.

        source
        theorem TauCeti.UniversalCover.subgroupQuotientMap_eq_iff {X : Type u_1} [TopologicalSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) {e₁ e₂ : UniversalCover x₀} :
        subgroupQuotientMap x₀ H e₁ = subgroupQuotientMap x₀ H e₂ ↔ e₁ ∈ MulAction.orbit (↥H) e₂

        Two points have the same image in the subgroup quotient exactly when they lie in the same H-orbit.

        source
        theorem TauCeti.UniversalCover.isQuotientCoveringMap_subgroupQuotientMap {X : Type u_1} [TopologicalSpace X] (x₀ : X) [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (H : Subgroup (FundamentalGroup X x₀)) :
        IsQuotientCoveringMap (subgroupQuotientMap x₀ H) ↥H

        The quotient map by any subgroup of the fundamental group is a quotient covering map.

        source
        noncomputable def TauCeti.UniversalCover.subgroupQuotientProj {X : Type u_1} [TopologicalSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) :
        SubgroupQuotient x₀ H → X

        The endpoint projection descended to the subgroup quotient.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.UniversalCover.subgroupQuotientProj_mk {X : Type u_1} [TopologicalSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) (e : UniversalCover x₀) :
          subgroupQuotientProj x₀ H (Quotient.mk'' e) = e.proj

          The descended endpoint projection evaluates on an orbit representative as proj.

          source
          theorem TauCeti.UniversalCover.subgroupQuotientProj_comp_subgroupQuotientMap {X : Type u_1} [TopologicalSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) :
          subgroupQuotientProj x₀ H ∘ subgroupQuotientMap x₀ H = proj

          The endpoint projection factors through the quotient by every subgroup.

          source
          @[simp]
          theorem TauCeti.UniversalCover.range_subgroupQuotientProj {X : Type u_1} [TopologicalSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) :
          Set.range (subgroupQuotientProj x₀ H) = pathComponent x₀

          The descended endpoint projection has range the path component of x₀, like UniversalCover.proj: its fibres over the other path components are empty.

          source
          theorem TauCeti.UniversalCover.subgroupQuotientProj_basepoint {X : Type u_1} [TopologicalSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) :
          subgroupQuotientProj x₀ H (SubgroupQuotient.basepoint x₀ H) = x₀

          The distinguished point of the subgroup quotient lies over the basepoint.

          source
          noncomputable def TauCeti.UniversalCover.SubgroupQuotient.basepointFiber {X : Type u_1} [TopologicalSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) :
          ↑(subgroupQuotientProj x₀ H ⁻¹' {x₀})

          The distinguished point of the subgroup quotient, regarded as a point of the fibre over the basepoint.

          Equations
          Instances For
            source
            @[simp]
            theorem TauCeti.UniversalCover.SubgroupQuotient.basepointFiber_coe {X : Type u_1} [TopologicalSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) :
            ↑(basepointFiber x₀ H) = basepoint x₀ H

            The underlying quotient point of basepointFiber is the distinguished point.

            source
            theorem TauCeti.UniversalCover.continuous_subgroupQuotientProj {X : Type u_1} [TopologicalSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) :
            Continuous (subgroupQuotientProj x₀ H)

            The descended endpoint projection is continuous.

            source
            theorem TauCeti.UniversalCover.subgroupQuotientProj_surjective {X : Type u_1} [TopologicalSpace X] (x₀ : X) [PathConnectedSpace X] (H : Subgroup (FundamentalGroup X x₀)) :
            Function.Surjective (subgroupQuotientProj x₀ H)

            The descended endpoint projection is surjective when the base is path connected.

            source
            theorem TauCeti.UniversalCover.subgroupQuotientProj_top_injective {X : Type u_1} [TopologicalSpace X] (x₀ : X) :
            Function.Injective (subgroupQuotientProj x₀ ⊤)

            The descended endpoint projection is injective on the orbit quotient by the whole fundamental group, because the orbits of that action are exactly the fibres of the endpoint projection.

            source
            noncomputable def TauCeti.UniversalCover.subgroupQuotientBotHomeomorph {X : Type u_1} [TopologicalSpace X] (x₀ : X) [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] :
            UniversalCover x₀ ≃ₜ SubgroupQuotient x₀ ⊥

            The quotient of the universal cover by the trivial subgroup is the universal cover. The underlying map is the quotient map subgroupQuotientMap x₀ ⊥, so the identification is one over X.

            Equations
            Instances For
              source
              @[simp]
              theorem TauCeti.UniversalCover.coe_subgroupQuotientBotHomeomorph {X : Type u_1} [TopologicalSpace X] (x₀ : X) [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] :
              ⇑(subgroupQuotientBotHomeomorph x₀) = subgroupQuotientMap x₀ ⊥