The fundamental group of a torus

Combining the product formula for fundamental groups (TauCeti.FundamentalGroup.prodMulEquiv, …piMulEquiv) with the circle computation π₁(AddCircle p) ≃* Multiplicative ℤ (AddCircle.fundamentalGroupMulEquivZero) gives the fundamental group of a torus. For a finite product of circles this is the free abelian group (Multiplicative ℤ)ᵏ; in particular the standard two-torus AddCircle p × AddCircle q has fundamental group Multiplicative ℤ × Multiplicative ℤ.

This realises the universal-covers roadmap Stage 4 "applications" target π_n(Tᵏ) at n = 1: π₁(Tᵏ) ≅ ℤᵏ.

Main declarations

• AddCircle.prodFundamentalGroupMulEquiv: π₁(AddCircle p × AddCircle q, (x, y)) ≃* Multiplicative ℤ × Multiplicative ℤ.
• AddCircle.piFundamentalGroupMulEquiv: π₁(Π i, AddCircle (p i), x) ≃* Π i, Multiplicative ℤ, the fundamental group of a torus.
• AddCircle.prodFundamentalGroupMulEquivZero, AddCircle.piFundamentalGroupMulEquivZero: the basepoint-0 specialisations.

noncomputable def AddCircle.prodFundamentalGroupMulEquiv {p q : ℝ} (hp : p ≠ 0) (hq : q ≠ 0) {x : AddCircle p} {y : AddCircle q} (ex : ↑(QuotientAddGroup.mk ⁻¹' {x})) (ey : ↑(QuotientAddGroup.mk ⁻¹' {y})) : FundamentalGroup (AddCircle p × AddCircle q) (x, y) ≃* Multiplicative ℤ × Multiplicative ℤ

The fundamental group of the two-torus AddCircle p × AddCircle q, based at any point (x, y) with chosen lifts ex, ey, is Multiplicative ℤ × Multiplicative ℤ, for nonzero real periods p and q. The forward map records, in each coordinate, the integer the corresponding projected loop winds around that circle.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AddCircle.prodFundamentalGroupMulEquiv_apply {p q : ℝ} (hp : p ≠ 0) (hq : q ≠ 0) {x : AddCircle p} {y : AddCircle q} (ex : ↑(QuotientAddGroup.mk ⁻¹' {x})) (ey : ↑(QuotientAddGroup.mk ⁻¹' {y})) (γ : FundamentalGroup (AddCircle p × AddCircle q) (x, y)) : (prodFundamentalGroupMulEquiv hp hq ex ey) γ = ((fundamentalGroupMulEquiv p hp ex) ((FundamentalGroup.map ContinuousMap.fst (x, y)) γ), (fundamentalGroupMulEquiv q hq ey) ((FundamentalGroup.map ContinuousMap.snd (x, y)) γ))

@[simp]

theorem AddCircle.prodFundamentalGroupMulEquiv_symm_apply {p q : ℝ} (hp : p ≠ 0) (hq : q ≠ 0) {x : AddCircle p} {y : AddCircle q} (ex : ↑(QuotientAddGroup.mk ⁻¹' {x})) (ey : ↑(QuotientAddGroup.mk ⁻¹' {y})) (mn : Multiplicative ℤ × Multiplicative ℤ) : (prodFundamentalGroupMulEquiv hp hq ex ey).symm mn = Path.Homotopic.prod ((fundamentalGroupMulEquiv p hp ex).symm mn.1) ((fundamentalGroupMulEquiv q hq ey).symm mn.2)

noncomputable def AddCircle.piFundamentalGroupMulEquiv {ι : Type u_1} {p : ι → ℝ} (hp : ∀ (i : ι), p i ≠ 0) {x : (i : ι) → AddCircle (p i)} (e : (i : ι) → ↑(QuotientAddGroup.mk ⁻¹' {x i})) : FundamentalGroup ((i : ι) → AddCircle (p i)) x ≃* (ι → Multiplicative ℤ)

The fundamental group of a torus Π i, AddCircle (p i), based at any point x with chosen lifts e, is the product Π i, Multiplicative ℤ, for a family of nonzero real periods. For a finite index this is the free abelian group (Multiplicative ℤ)ᵏ, i.e. π₁(Tᵏ) ≅ ℤᵏ. The forward map records, in each coordinate, the winding integer of the corresponding projected loop.

Equations

• AddCircle.piFundamentalGroupMulEquiv hp e = (TauCeti.FundamentalGroup.piMulEquiv x).trans (MulEquiv.piCongrRight fun (i : ι) => AddCircle.fundamentalGroupMulEquiv (p i) ⋯ (e i))

@[simp]

theorem AddCircle.piFundamentalGroupMulEquiv_apply {ι : Type u_1} {p : ι → ℝ} (hp : ∀ (i : ι), p i ≠ 0) {x : (i : ι) → AddCircle (p i)} (e : (i : ι) → ↑(QuotientAddGroup.mk ⁻¹' {x i})) (γ : FundamentalGroup ((i : ι) → AddCircle (p i)) x) (i : ι) : (piFundamentalGroupMulEquiv hp e) γ i = (fundamentalGroupMulEquiv (p i) ⋯ (e i)) ((FundamentalGroup.map (ContinuousMap.eval i) x) γ)

@[simp]

theorem AddCircle.piFundamentalGroupMulEquiv_symm_apply {ι : Type u_1} {p : ι → ℝ} (hp : ∀ (i : ι), p i ≠ 0) {x : (i : ι) → AddCircle (p i)} (e : (i : ι) → ↑(QuotientAddGroup.mk ⁻¹' {x i})) (n : ι → Multiplicative ℤ) : (piFundamentalGroupMulEquiv hp e).symm n = Path.Homotopic.pi fun (i : ι) => (fundamentalGroupMulEquiv (p i) ⋯ (e i)).symm (n i)

noncomputable def AddCircle.prodFundamentalGroupMulEquivZero {p q : ℝ} (hp : p ≠ 0) (hq : q ≠ 0) : FundamentalGroup (AddCircle p × AddCircle q) (0, 0) ≃* Multiplicative ℤ × Multiplicative ℤ

The fundamental group of the two-torus AddCircle p × AddCircle q, based at (0, 0), is Multiplicative ℤ × Multiplicative ℤ, for nonzero real periods p and q.

Equations

• AddCircle.prodFundamentalGroupMulEquivZero hp hq = AddCircle.prodFundamentalGroupMulEquiv hp hq ⟨0, ⋯⟩ ⟨0, ⋯⟩

@[simp]

theorem AddCircle.prodFundamentalGroupMulEquivZero_apply {p q : ℝ} (hp : p ≠ 0) (hq : q ≠ 0) (γ : FundamentalGroup (AddCircle p × AddCircle q) (0, 0)) : (prodFundamentalGroupMulEquivZero hp hq) γ = ((fundamentalGroupMulEquivZero p hp) ((FundamentalGroup.map ContinuousMap.fst (0, 0)) γ), (fundamentalGroupMulEquivZero q hq) ((FundamentalGroup.map ContinuousMap.snd (0, 0)) γ))

@[simp]

theorem AddCircle.prodFundamentalGroupMulEquivZero_symm_apply {p q : ℝ} (hp : p ≠ 0) (hq : q ≠ 0) (mn : Multiplicative ℤ × Multiplicative ℤ) : (prodFundamentalGroupMulEquivZero hp hq).symm mn = Path.Homotopic.prod ((fundamentalGroupMulEquivZero p hp).symm mn.1) ((fundamentalGroupMulEquivZero q hq).symm mn.2)

noncomputable def AddCircle.piFundamentalGroupMulEquivZero {ι : Type u_1} {p : ι → ℝ} (hp : ∀ (i : ι), p i ≠ 0) : (FundamentalGroup ((i : ι) → AddCircle (p i)) fun (x : ι) => 0) ≃* (ι → Multiplicative ℤ)

The fundamental group of a torus Π i, AddCircle (p i), based at 0, is the product Π i, Multiplicative ℤ, for a family of nonzero real periods. For a finite index this is the free abelian group (Multiplicative ℤ)ᵏ, i.e. π₁(Tᵏ) ≅ ℤᵏ.

Equations

• AddCircle.piFundamentalGroupMulEquivZero hp = AddCircle.piFundamentalGroupMulEquiv hp fun (i : ι) => ⟨0, ⋯⟩

@[simp]

theorem AddCircle.piFundamentalGroupMulEquivZero_apply {ι : Type u_1} {p : ι → ℝ} (hp : ∀ (i : ι), p i ≠ 0) (γ : FundamentalGroup ((i : ι) → AddCircle (p i)) fun (x : ι) => 0) (i : ι) : (piFundamentalGroupMulEquivZero hp) γ i = (fundamentalGroupMulEquivZero (p i) ⋯) ((FundamentalGroup.map (ContinuousMap.eval i) fun (x : ι) => 0) γ)

@[simp]

theorem AddCircle.piFundamentalGroupMulEquivZero_symm_apply {ι : Type u_1} {p : ι → ℝ} (hp : ∀ (i : ι), p i ≠ 0) (n : ι → Multiplicative ℤ) : (piFundamentalGroupMulEquivZero hp).symm n = Path.Homotopic.pi fun (i : ι) => (fundamentalGroupMulEquivZero (p i) ⋯).symm (n i)