Homotopy classes of self-maps of the torus

Every continuous self-map of the torus S¹ × S¹ is homotopic to exactly one monomial map Matrix.torusMap M, (a, b) ↦ (a ^ M₀₀ * b ^ M₀₁, a ^ M₁₀ * b ^ M₁₁), for an integral 2 × 2 matrix M. So the homotopy classes of self-maps of the torus are the integral matrices, composition corresponding to the product of matrices, and the self-homeomorphisms of the torus are homotopic to the linear homeomorphisms Matrix.GeneralLinearGroup.torusHomeomorph A, A ∈ GL₂(ℤ). This is the case of the torus, a K(ℤ², 1), of the classification of maps into an Eilenberg–MacLane space by their action on the fundamental group.

The proof lifts along the universal covering ℝ × ℝ → S¹ × S¹, (x, y) ↦ (exp (i x), exp (i y)). A coordinate g of a self-map of the torus, read on ℝ × ℝ, lifts through exp : ℝ → S¹ to a continuous G : ℝ × ℝ → ℝ, since ℝ × ℝ is simply connected. Translating by a period 2π in either variable changes G by an integer multiple of 2π, which is constant because ℝ × ℝ is connected; call these integers m and n. Then G differs from the linear map (x, y) ↦ m x + n y by a function periodic in both variables, and the straight-line homotopy between them descends to the torus, from g to the monomial (a, b) ↦ a ^ m * b ^ n. The integers are determined by the homotopy class: restricted to the (p, q) curve on the torus, the monomial is a loop in the circle of degree m p + n q, and the degree is invariant under homotopy (Circle.degree_eq_of_homotopy).

The matrix of a self-map f is ContinuousMap.torusMatrix f. Two self-maps are homotopic exactly when their matrices agree (ContinuousMap.homotopic_iff_torusMatrix_eq), the matrix of a composite is the product of the matrices (ContinuousMap.torusMatrix_comp), and the matrix of a homeomorphism is invertible (Homeomorph.isUnit_torusMatrix). The homotopy class of a gluing of two solid tori along their boundary tori is therefore an element of GL₂(ℤ); that homotopic homeomorphisms of the torus are isotopic, which upgrades this to the isotopy classification used for Dehn filling, is not proved here.

Main definitions

• ContinuousMap.torusMatrix f: the integral matrix of the monomial map homotopic to a self-map f of the torus.

Main results

• ContinuousMap.homotopic_torusContinuousMap_torusMatrix: every self-map of the torus is homotopic to the monomial map of its matrix.
• Matrix.torusContinuousMap_homotopic_iff: two monomial maps are homotopic exactly when their matrices are equal.
• ContinuousMap.homotopic_iff_torusMatrix_eq: two self-maps of the torus are homotopic exactly when their matrices are equal.
• ContinuousMap.torusMatrix_comp, ContinuousMap.torusMatrix_id: the matrix is multiplicative.
• Homeomorph.isUnit_torusMatrix: the matrix of a self-homeomorphism of the torus is invertible.
• Homeomorph.existsUnique_homotopic_torusHomeomorph: every self-homeomorphism of the torus is homotopic to the linear homeomorphism of exactly one matrix in GL₂(ℤ).

References

• A. Hatcher, Algebraic Topology, Cambridge University Press (2002), Proposition 1.30 (homotopy lifting for covering spaces) and Proposition 1B.9 (maps into a K(G, 1) are classified up to homotopy by the homomorphisms they induce on fundamental groups).
• B. Farb, D. Margalit, A Primer on Mapping Class Groups, Princeton University Press (2012), Section 2.2 (the mapping class group of the torus, through the action of homeomorphisms on the fundamental group).

Lifting maps along the covering ℝ × ℝ → S¹ × S¹

Every coordinate is homotopic to a monomial

The matrix of a self-map of the torus

theorem Matrix.torusContinuousMap_homotopic_iff {M N : Matrix (Fin 2) (Fin 2) ℤ} : M.torusContinuousMap.Homotopic N.torusContinuousMap ↔ M = N

Two monomial self-maps of the torus are homotopic exactly when their matrices are equal.

noncomputable def ContinuousMap.torusMatrix (f : C(Circle × Circle, Circle × Circle)) : Matrix (Fin 2) (Fin 2) ℤ

The matrix of a self-map f of the torus: the integral matrix M whose monomial map (a, b) ↦ (a ^ M₀₀ * b ^ M₀₁, a ^ M₁₀ * b ^ M₁₁) is homotopic to f (ContinuousMap.homotopic_torusContinuousMap_torusMatrix). It is unique (ContinuousMap.torusMatrix_eq_iff).

theorem ContinuousMap.homotopic_torusContinuousMap_torusMatrix (f : C(Circle × Circle, Circle × Circle)) : f.Homotopic f.torusMatrix.torusContinuousMap

A self-map of the torus is homotopic to the monomial map of its matrix.

theorem ContinuousMap.torusMatrix_eq_iff {f : C(Circle × Circle, Circle × Circle)} {M : Matrix (Fin 2) (Fin 2) ℤ} : f.torusMatrix = M ↔ f.Homotopic M.torusContinuousMap

The matrix of a self-map of the torus is the matrix of any monomial map homotopic to it.

theorem ContinuousMap.homotopic_iff_torusMatrix_eq {f g : C(Circle × Circle, Circle × Circle)} : f.Homotopic g ↔ f.torusMatrix = g.torusMatrix

The homotopy classification of self-maps of the torus. Two self-maps of the torus are homotopic exactly when their matrices are equal.

@[simp]

theorem ContinuousMap.torusMatrix_torusContinuousMap (M : Matrix (Fin 2) (Fin 2) ℤ) : M.torusContinuousMap.torusMatrix = M

The matrix of the monomial map of a matrix is that matrix.

@[simp]

theorem ContinuousMap.torusMatrix_id : (ContinuousMap.id (Circle × Circle)).torusMatrix = 1

The matrix of the identity of the torus is the identity matrix.

@[simp]

theorem ContinuousMap.torusMatrix_comp (f g : C(Circle × Circle, Circle × Circle)) : (f.comp g).torusMatrix = f.torusMatrix * g.torusMatrix

The matrix of a composite of self-maps of the torus is the product of their matrices.

theorem Homeomorph.isUnit_torusMatrix (h : Circle × Circle ≃ₜ Circle × Circle) : IsUnit (↑h).torusMatrix

The matrix of a self-homeomorphism of the torus is invertible: its inverse is the matrix of the inverse homeomorphism.

theorem Homeomorph.existsUnique_homotopic_torusHomeomorph (h : Circle × Circle ≃ₜ Circle × Circle) : ∃! A : GL (Fin 2) ℤ, (↑h).Homotopic ↑A.torusHomeomorph

Every self-homeomorphism of the torus is homotopic to a linear one: it is homotopic to the homeomorphism Matrix.GeneralLinearGroup.torusHomeomorph A of exactly one matrix A ∈ GL₂(ℤ).