Documentation

TauCeti.AlgebraicTopology.UniversalCover.Quotient

The fundamental-group quotient of the universal cover #

The fundamental group of a path-connected, locally path-connected space acts on its based-path universal cover. Two points of the universal cover have the same endpoint exactly when they belong to the same orbit. The endpoint projection therefore descends to a homeomorphism

UniversalCover x₀ / FundamentalGroup X x₀ ≃ₜ X.

This is the topological quotient statement associated to the universal cover. It uses the actual fundamental-group action on based path classes, rather than first replacing that action by the isomorphic deck-transformation group.

Main declaration #

References #

Compare Hatcher, Algebraic Topology, Section 1.3, especially Propositions 1.39 and 1.40. The based-path construction and action are adapted from Kim Morrison's mathlib4#38292.

source
noncomputable def TauCeti.UniversalCover.orbitQuotientHomeomorph {X : Type u_1} [TopologicalSpace X] [PathConnectedSpace X] [LocallyPathConnectedSpace X] (x₀ : X) :
MulAction.orbitRel.Quotient (FundamentalGroup X x₀) (UniversalCover x₀) ≃ₜ X

The quotient of the universal cover by its fundamental-group action is homeomorphic to the base space. The homeomorphism sends the orbit of a based path to its endpoint.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.UniversalCover.orbitQuotientHomeomorph_mk {X : Type u_1} [TopologicalSpace X] [PathConnectedSpace X] [LocallyPathConnectedSpace X] (x₀ : X) (p : UniversalCover x₀) :
    (orbitQuotientHomeomorph x₀) (Quotient.mk'' p) = p.proj

    On an orbit representative, the quotient homeomorphism is the endpoint projection.

    source
    @[simp]
    theorem TauCeti.UniversalCover.orbitQuotientHomeomorph_symm_apply_proj {X : Type u_1} [TopologicalSpace X] [PathConnectedSpace X] [LocallyPathConnectedSpace X] (x₀ : X) (p : UniversalCover x₀) :
    (orbitQuotientHomeomorph x₀).symm p.proj = Quotient.mk'' p

    The inverse quotient homeomorphism sends an endpoint to the orbit of any lift with that endpoint.