Documentation

TauCeti.AlgebraicTopology.UniversalCover.Classification.Existence

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 two inputs are that UniversalCover.proj and UniversalCover.subgroupQuotientMap are quotient covering maps, for π₁(X, x₀) and for H respectively, and that the first factors through the second. TauCeti.IsQuotientCoveringMap.isCoveringMap_of_comp turns exactly that data into a covering map: the sheets of the descended projection over the image of a locally disjoint set U are the images of the translates of U. Nothing about good neighbourhoods of the base, their path-connectedness, or the transport of a sheet of proj along the fundamental-group action enters here, because the general statement uses only the disjointness built into IsQuotientCoveringMap.

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 #

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.

source
theorem TauCeti.UniversalCover.isCoveringMap_subgroupQuotientProj {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [PathConnectedSpace 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.

source
theorem TauCeti.UniversalCover.locallyPathConnectedSpace_subgroupQuotient {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [PathConnectedSpace 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.

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

The connected covering space associated to a subgroup H ≤ π₁(X, x₀), obtained by quotienting the universal cover by H.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.UniversalCover.subgroupCover_coe {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [PathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) :
    (subgroupCover x₀ H).obj.left = TopCat.of (SubgroupQuotient x₀ H)

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

    source
    @[simp]
    theorem TauCeti.UniversalCover.subgroupCover_proj {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [PathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) :
    (subgroupCover x₀ H).proj = 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.

    source
    noncomputable def TauCeti.UniversalCover.subgroupCoverTotalSpaceHomeomorph {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [PathConnectedSpace 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
    Instances For
      source
      theorem TauCeti.UniversalCover.subgroupQuotientProj_subgroupCoverTotalSpaceHomeomorph {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [PathConnectedSpace 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 (subgroupCover x₀ H).proj) e

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

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

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

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

        Fibre transport commutes with monodromy.

        source
        noncomputable def TauCeti.UniversalCover.subgroupCoverBasepointFiber {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [PathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (H : Subgroup (FundamentalGroup X x₀)) :
        ↑(⇑(CategoryTheory.ConcreteCategory.hom (subgroupCover x₀ H).proj) ⁻¹' {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.
        Instances For
          source
          @[simp]
          theorem TauCeti.UniversalCover.subgroupCoverFiberEquivSubgroupQuotient_apply_basepoint {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [PathConnectedSpace 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.

          source
          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
          Instances For
            source
            @[simp]
            theorem TauCeti.UniversalCover.coe_subgroupQuotientTopHomeomorph {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [PathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) :
            ⇑(subgroupQuotientTopHomeomorph x₀) = subgroupQuotientProj x₀ ⊤