Documentation

TauCeti.AlgebraicTopology.UniversalCover.PathComponent

The universal cover of a non-path-connected base #

The endpoint projection UniversalCover.proj : UniversalCover x₀ → X is a covering map for any locally path connected, semilocally simply connected X (UniversalCover.isCoveringMap); when X is not path connected its range is exactly the path component of x₀ (UniversalCover.range_proj), and the fibres over the other path components are empty.

The deck-group computation UniversalCover.deckFundamentalGroupEquiv does use path connectedness, since it goes through regularity of the covering, which includes surjectivity. For a base that is not path connected this file therefore passes to the universal cover of the path component of x₀. That component is path connected, is open and therefore locally path connected, and absorbs ambient null-homotopies, so it inherits all three standing hypotheses (TauCeti/AlgebraicTopology/PathComponent.lean). The deck group is unchanged by composing with the inclusion into X, and FundamentalGroup.pathComponentMulEquiv identifies the fundamental group of the path component with that of X at the same point. Thus the deck group of the path-component cover is (π₁(X, x₀))ᵐᵒᵖ, with the same opposite-group convention pinned in TauCeti.UniversalCover.deckFundamentalGroupEquiv.

Main declarations #

References #

It consumes the based-path universal cover adapted from Kim Morrison's mathlib4#38292 and Mathlib's deck group deck, from Kim Morrison's mathlib4#40135.

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

The universal cover of the path component of x₀. The component is path connected; local path connectedness follows from its openness, and semilocal simple connectivity follows because ambient null-homotopies based in the component remain there.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev TauCeti.UniversalCover.pathComponentCoverProj {X : Type u_1} [TopologicalSpace X] (x₀ : X) :
    PathComponentCover x₀ → X

    The projection of the universal cover of the path component of x₀ down to X, the endpoint projection followed by the inclusion of the path component.

    Equations
    Instances For
      source
      theorem TauCeti.UniversalCover.isCoveringMap_pathComponentCoverProj {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) :
      IsCoveringMap (pathComponentCoverProj x₀)

      The universal cover of a path component is a covering map into the ambient space. The path component is clopen, so fibres over the other path components are empty and evenly covered by empty trivialisations.

      source
      theorem TauCeti.UniversalCover.range_pathComponentCoverProj {X : Type u_1} [TopologicalSpace X] (x₀ : X) :
      Set.range (pathComponentCoverProj x₀) = pathComponent x₀

      The image of the path-component cover is exactly the path component of x₀.

      source
      theorem TauCeti.UniversalCover.existsUnique_continuousMap_lifts_pathComponentCoverProj {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) {A : Type u_2} [TopologicalSpace A] [LocallyPathConnectedSpace A] [SimplyConnectedSpace A] (f : C(A, X)) (a₀ : A) (e₀ : PathComponentCover x₀) (he : pathComponentCoverProj x₀ e₀ = f a₀) :
      ∃! F : C(A, PathComponentCover x₀), F a₀ = e₀ ∧ pathComponentCoverProj x₀ ∘ ⇑F = ⇑f

      Universal property of the path-component cover. A continuous map into X from a locally path connected, simply connected space lifts uniquely once the image of one point is prescribed.

      source
      theorem TauCeti.UniversalCover.deck_pathComponentCoverProj {X : Type u_1} [TopologicalSpace X] (x₀ : X) :
      deck (pathComponentCoverProj x₀) = deck proj

      Postcomposing the endpoint projection with the path-component inclusion does not change its deck group.

      source
      noncomputable def TauCeti.UniversalCover.deckPathComponentFundamentalGroupEquiv {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) :
      ↥(deck (pathComponentCoverProj x₀)) ≃* (FundamentalGroup X x₀)ᵐᵒᵖ

      The deck group of the path-component cover is the opposite fundamental group of X. The inclusion leaves the deck group unchanged, the universal cover of the component has deck group the opposite of its fundamental group, and FundamentalGroup.pathComponentMulEquiv identifies that group with π₁(X, x₀).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem TauCeti.UniversalCover.deckPathComponentFundamentalGroupEquiv_symm_op {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (g : FundamentalGroup X x₀) :
        (deckPathComponentFundamentalGroupEquiv x₀).symm (MulOpposite.op g) = (MulEquiv.subgroupCongr ⋯).symm (loopDeck (pathComponentSelf x₀) ((FundamentalGroup.pathComponentMulEquiv x₀ (pathComponentSelf x₀)).symm g)⁻¹)

        The inverse deck-group equivalence sends op g to the loop deck transformation associated to the inverse of the corresponding loop in the path component.