The first homology of a torus, naturally in integer matrices

For a family of nonzero periods p : ι → ℝ, the first singular homology group with integer coefficients of the torus Tⁱ = ∀ i, AddCircle (p i) is ι → ℤ (TauCeti.torusFirstHomologyEquiv). The isomorphism is the composite of the Hurewicz isomorphism H₁(Tⁱ; ℤ) ≅ π₁(Tⁱ, 0)ᵃᵇ (TauCeti.HurewiczOne.hurewiczHomologyAddEquiv) with the computation π₁(Tⁱ, 0) ≅ ℤⁱ (AddCircle.piFundamentalGroupMulEquivZero), the fundamental group being already commutative. It sends the class of the straight loop TauCeti.torusLoop p n, which winds n i times around the i-th circle, to n (TauCeti.torusFirstHomologyEquiv_loopClass).

For a common period p, an integer matrix A : Matrix κ ι ℤ induces the map of tori Matrix.smulVecHom A (AddCircle p) : Tⁱ → Tᵏ, and under these identifications the map it induces on first homology is n ↦ A *ᵥ n (TauCeti.torusFirstHomologyEquiv_homologyMap_smulVecHom). This is the action of integer matrices on the first homology of a torus; the higher homology of a torus is the exterior algebra on it, which is not proved here. The torus is modelled here as a product of additive circles, on which integer matrices act. The ranks of all homology groups of the homeomorphic product of unit spheres are computed in ModuleCat.finrank_singularHomology_torus.

A space Y parametrized by the torus S¹ × S¹ of unit complex numbers, through a homeomorphism e : S¹ × S¹ ≃ₜ Y, has first homology ℤ² (TauCeti.circleProdFirstHomologyEquiv): the class of the (p, q) curve t ↦ e (exp (2πipt), exp (2πiqt)) corresponds to (p, q) (TauCeti.circleProdFirstHomologyEquiv_torusCurve). This is the form in which tori appear as boundaries of solid tori D² × S¹.

Main definitions and results

• TauCeti.torusFirstHomologyEquiv: the isomorphism H₁(Tⁱ; ℤ) ≃ₗ[ℤ] (ι → ℤ).

• TauCeti.torusFirstHomologyEquiv_loopClass, TauCeti.torusFirstHomologyEquiv_symm_apply: the class of the straight loop of n corresponds to n.

• TauCeti.torusFirstHomologyEquiv_homologyMap_smulVecHom: naturality in integer matrices.

• TauCeti.circleProdFirstHomologyEquiv, TauCeti.circleProdFirstHomologyEquiv_torusCurve: the isomorphism H₁(Y; ℤ) ≃ₗ[ℤ] ℤ² of a space parametrized by S¹ × S¹, sending the class of the (p, q) curve TauCeti.torusCurve p q to (p, q).

• TauCeti.torusClass: the class of an integer-winding curve on S¹ × S¹, with its coordinates, decomposition into the coordinate curves, and induced-map formula.

• ContinuousMap.exists_singularHomologyMap_prodMap_torusClass_zero_one: reparametrizing the second circle keeps the (0, 1) curve a (0, q) curve.

References

• A. Hatcher, Algebraic Topology, Theorem 2A.1 for the Hurewicz isomorphism in degree one, and Proposition 1.12 for the fundamental group of a product.

noncomputable def TauCeti.torusFirstHomologyEquiv {ι : Type} (p : ι → ℝ) (hp : ∀ (i : ι), p i ≠ 0) : ↑(HomologicalComplex.homology ((singularChains ℤ).obj ↧((i : ι) → AddCircle (p i))) 1) ≃ₗ[ℤ] ι → ℤ

The first singular homology group with integer coefficients of the torus ∀ i, AddCircle (p i) is ι → ℤ.

@[simp]

theorem TauCeti.torusFirstHomologyEquiv_loopClass {ι : Type} (p : ι → ℝ) (hp : ∀ (i : ι), p i ≠ 0) (n : ι → ℤ) : (torusFirstHomologyEquiv p hp) ((HurewiczOne.H₁AddEquivHomology ↧((i : ι) → AddCircle (p i))) (HurewiczOne.loopClass (torusLoop p n))) = n

The class of the straight loop TauCeti.torusLoop p n corresponds to n.

theorem TauCeti.torusFirstHomologyEquiv_symm_apply {ι : Type} (p : ι → ℝ) (hp : ∀ (i : ι), p i ≠ 0) (n : ι → ℤ) : (torusFirstHomologyEquiv p hp).symm n = (HurewiczOne.H₁AddEquivHomology ↧((i : ι) → AddCircle (p i))) (HurewiczOne.loopClass (torusLoop p n))

The inverse of TauCeti.torusFirstHomologyEquiv sends n to the class of the straight loop TauCeti.torusLoop p n, which winds n i times around the i-th circle.

theorem TauCeti.torusFirstHomologyEquiv_homologyMap_smulVecHom {ι : Type} [Fintype ι] {κ : Type} (A : Matrix κ ι ℤ) {p : ℝ} (hp : p ≠ 0) (x : ↑(HomologicalComplex.homology ((singularChains ℤ).obj ↧(ι → AddCircle p)) 1)) : (torusFirstHomologyEquiv (fun (x : κ) => p) ⋯) ((ModuleCat.Hom.hom (HomologicalComplex.homologyMap ((singularChains ℤ).map (TopCat.ofHom ↑(A.smulVecHom (AddCircle p)))) 1)) x) = A.mulVec ((torusFirstHomologyEquiv (fun (x : ι) => p) ⋯) x)

The first homology of a torus is natural in integer matrices. Under the identifications H₁(Tⁱ; ℤ) ≅ ℤⁱ of TauCeti.torusFirstHomologyEquiv, the map induced on first homology by the map of tori Matrix.smulVecHom A (AddCircle p) is multiplication by the matrix A.

Tori parametrized by S¹ × S¹

noncomputable def TauCeti.circleProdFirstHomologyEquiv {Y : Type} [TopologicalSpace Y] (e : Circle × Circle ≃ₜ Y) : ↑(HomologicalComplex.homology ((singularChains ℤ).obj ↧Y) 1) ≃ₗ[ℤ] Fin 2 → ℤ

The first homology of a torus parametrized by S¹ × S¹. A homeomorphism e : S¹ × S¹ ≃ₜ Y identifies H₁(Y; ℤ) with ℤ², the class of the (p, q) curve t ↦ e (exp (2πipt), exp (2πiqt)) going to (p, q) (TauCeti.circleProdFirstHomologyEquiv_torusCurve). It transports the computation TauCeti.torusFirstHomologyEquiv for ℝ² / ℤ² along e and TauCeti.circleProdHomeomorphUnitAddTorus.

theorem TauCeti.circleProdFirstHomologyEquiv_apply {Y : Type} [TopologicalSpace Y] (e : Circle × Circle ≃ₜ Y) (x : ↑(HomologicalComplex.homology ((singularChains ℤ).obj ↧Y) 1)) : (circleProdFirstHomologyEquiv e) x = (torusFirstHomologyEquiv (fun (x : Fin 2) => 1) ⋯) ((ModuleCat.Hom.hom (HomologicalComplex.homologyMap ((singularChains ℤ).map (TopCat.isoOfHomeo (e.symm.trans circleProdHomeomorphUnitAddTorus)).hom) 1)) x)

The identification of the first homology of a parametrized torus with ℤ² pushes a class forward to ℝ² / ℤ² along e.symm and TauCeti.circleProdHomeomorphUnitAddTorus, then reads it off by TauCeti.torusFirstHomologyEquiv.

@[simp]

theorem TauCeti.circleProdFirstHomologyEquiv_torusCurve {Y : Type} [TopologicalSpace Y] (e : Circle × Circle ≃ₜ Y) (p q : ℤ) : (circleProdFirstHomologyEquiv e) ((HurewiczOne.H₁AddEquivHomology ↧Y) (HurewiczOne.loopClass ((torusCurve p q).map ⋯))) = ![p, q]

The identification of the first homology of a parametrized torus with ℤ² sends the class of the (p, q) curve t ↦ e (exp (2πipt), exp (2πiqt)) to (p, q).

Classes of curves on the standard torus

noncomputable def TauCeti.torusClass (p q : ℤ) : ↑(HomologicalComplex.homology ((singularChains ℤ).obj ↧(Circle × Circle)) 1)

The class of the (p, q) curve of S¹ × S¹.

theorem TauCeti.torusClass_def (p q : ℤ) : torusClass p q = (HurewiczOne.H₁AddEquivHomology ↧(Circle × Circle)) (HurewiczOne.loopClass (torusCurve p q))

The class of the (p, q) curve is its Hurewicz class in H₁(S¹ × S¹; ℤ).

theorem ContinuousMap.singularHomologyMap_torusClass {Y : Type} [TopologicalSpace Y] (g : C(Circle × Circle, Y)) (p q : ℤ) : (singularHomologyMap ℤ 1 g) (TauCeti.torusClass p q) = (TauCeti.HurewiczOne.H₁AddEquivHomology ↧Y) (TauCeti.HurewiczOne.loopClass ((TauCeti.torusCurve p q).map ⋯))

The induced map sends the class of a torus curve to the class of its image.

@[simp]

theorem TauCeti.circleProdFirstHomologyEquiv_torusClass (p q : ℤ) : (circleProdFirstHomologyEquiv (Homeomorph.refl (Circle × Circle))) (torusClass p q) = ![p, q]

The class of the (p, q) curve has coordinates (p, q) in first homology.

theorem TauCeti.torusClass_eq (p q : ℤ) : torusClass p q = p • torusClass 1 0 + q • torusClass 0 1

Every torus curve class is the corresponding integral combination of the coordinate curves.

theorem TauCeti.exists_eq_torusClass (x : ↑(HomologicalComplex.homology ((singularChains ℤ).obj ↧(Circle × Circle)) 1)) : ∃ (p : ℤ) (q : ℤ), x = torusClass p q

Every first integral homology class of the torus is represented by a torus curve.

@[simp]

theorem TauCeti.torusClass_eq_zero_iff (p q : ℤ) : torusClass p q = 0 ↔ p = 0 ∧ q = 0

A torus curve has zero first integral homology class exactly when both winding numbers vanish.

theorem TauCeti.singularHomologyMap_prodMk_const_torusClass (p q : ℤ) : (ContinuousMap.singularHomologyMap ℤ 1 (ContinuousMap.fst.prodMk (ContinuousMap.const (Circle × Circle) 1))) (torusClass p q) = torusClass p 0

Collapsing the second circle of the torus sends the class of the (p, q) curve to the class of the (p, 0) curve.

theorem ContinuousMap.exists_singularHomologyMap_prodMap_torusClass_zero_one (g : C(Circle, Circle)) : ∃ (q : ℤ), (singularHomologyMap ℤ 1 ((ContinuousMap.id Circle).prodMap g)) (TauCeti.torusClass 0 1) = TauCeti.torusClass 0 q

Reparametrizing the second circle of the torus by a self-map g of the circle sends the class of the (0, 1) curve to the class of a (0, q) curve: the first winding number stays 0.