Documentation

TauCeti.AlgebraicTopology.FundamentalGroup.Product

The fundamental group of a product space #

Mathlib knows that the fundamental groupoid preserves products (FundamentalGroupoidFunctor.prodIso, …piIso), but the corresponding group-level statement is missing: the fundamental group of a product is the product of the fundamental groups. This file supplies it, both for binary and for indexed products, together with its simplest consequence: a product of two simply connected spaces is simply connected.

The two equivalences are built directly from the path-class product operations Path.Homotopic.prod / Path.Homotopic.pi and their coordinate projections, which already descend homotopy and composition through the quotient. The forward map is the pair (resp. tuple) of the maps induced by the coordinate projections, packaged through Mathlib's FundamentalGroup.map; the inverse assembles a loop in the product from its coordinate loops. The projection-product round trips (Path.Homotopic.prod_projLeft_projRight, …projLeft_prod, …projRight_prod, …pi_proj, …proj_pi) make both composites the identity, and FundamentalGroup.map being a MonoidHom supplies multiplicativity.

This is the group-level input the universal-covers roadmap calls for when computing π₁(Tᵏ) (Stage 4, "applications": π_n(Tᵏ)); see TauCeti/AlgebraicTopology/UniversalCover/Torus/FundamentalGroup.lean for the torus application built on top.

Main declarations #

source
noncomputable def TauCeti.FundamentalGroup.prodMulEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (x : X) (y : Y) :
FundamentalGroup (X × Y) (x, y) ≃* FundamentalGroup X x × FundamentalGroup Y y

The fundamental group of a binary product is the product of the fundamental groups: π₁(X × Y, (x, y)) ≃* π₁(X, x) × π₁(Y, y). The forward map is the pair of the maps induced by the two coordinate projections; the inverse sends a pair of loop classes to their product Path.Homotopic.prod.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.FundamentalGroup.prodMulEquiv_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (x : X) (y : Y) (γ : FundamentalGroup (X × Y) (x, y)) :
    (prodMulEquiv x y) γ = ((FundamentalGroup.map ContinuousMap.fst (x, y)) γ, (FundamentalGroup.map ContinuousMap.snd (x, y)) γ)
    source
    @[simp]
    theorem TauCeti.FundamentalGroup.prodMulEquiv_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (x : X) (y : Y) (γ : FundamentalGroup X x × FundamentalGroup Y y) :
    (prodMulEquiv x y).symm γ = Path.Homotopic.prod γ.1 γ.2
    source
    instance TauCeti.instSimplyConnectedSpaceProd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SimplyConnectedSpace X] [SimplyConnectedSpace Y] :
    SimplyConnectedSpace (X × Y)

    A product of two simply connected spaces is simply connected. A path class in X × Y is the product of its two coordinate classes (Path.Homotopic.prod_projLeft_projRight), and those are unique.

    source
    noncomputable def TauCeti.FundamentalGroup.piMulEquiv {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] (x : (i : ι) → X i) :
    FundamentalGroup ((i : ι) → X i) x ≃* ((i : ι) → FundamentalGroup (X i) (x i))

    The fundamental group of an indexed product is the product of the fundamental groups: π₁(Π i, X i, x) ≃* Π i, π₁(X i, x i). The forward map records the loop's image under each coordinate projection; the inverse assembles a loop from its coordinate loops via Path.Homotopic.pi.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.FundamentalGroup.piMulEquiv_apply {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] (x : (i : ι) → X i) (γ : FundamentalGroup ((i : ι) → X i) x) (i : ι) :
      (piMulEquiv x) γ i = (FundamentalGroup.map (ContinuousMap.eval i) x) γ
      source
      @[simp]
      theorem TauCeti.FundamentalGroup.piMulEquiv_symm_apply {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] (x : (i : ι) → X i) (γ : (i : ι) → FundamentalGroup (X i) (x i)) :
      (piMulEquiv x).symm γ = Path.Homotopic.pi γ