Integral matrices acting on the torus

An invertible integral 2 × 2 matrix A acts on the torus S¹ × S¹ by the monomial homeomorphism (a, b) ↦ (a ^ A₀₀ * b ^ A₀₁, a ^ A₁₀ * b ^ A₁₁). These are the linear homeomorphisms of the torus ℝ² / ℤ² read in the coordinates S¹ = ℝ / ℤ: the map carries the (p, q) curve TauCeti.torusCurve p q to the A (p, q) curve, so it acts on the first homology of the torus by A. Every homeomorphism of the torus is isotopic to exactly one of them, which is why gluings of solid tori along their boundary tori, as in Dehn filling, are normally given by such a matrix. Up to homotopy rather than isotopy, this is Homeomorph.existsUnique_homotopic_torusHomeomorph.

Main definitions

• Matrix.torusMap M: the monomial self-map of S¹ × S¹ induced by any integral matrix M.
• Matrix.torusContinuousMap M: the same map, as a continuous map.
• Matrix.GeneralLinearGroup.torusHomeomorph A: the homeomorphism of S¹ × S¹ induced by A.

Main results

• Matrix.torusMap_torusMap, Matrix.torusMap_one: the integral matrices act on the torus through a monoid action.
• Matrix.torusContinuousMap_comp, Matrix.torusContinuousMap_one: the same for the continuous maps.
• Matrix.GeneralLinearGroup.torusHomeomorph_one, Matrix.GeneralLinearGroup.torusHomeomorph_mul, Matrix.GeneralLinearGroup.symm_torusHomeomorph: the matrices act through a group action.
• Matrix.GeneralLinearGroup.torusHomeomorph_torusCurve: the (p, q) curve goes to the A (p, q) curve.
• Matrix.GeneralLinearGroup.torusHomeomorph_swap: the matrix exchanging the coordinates acts by exchanging the circle factors.
• TauCeti.exists_torusHomeomorph_eq_torusGluing: the determinant-one gluing TauCeti.torusGluing p q s t is induced by the matrix [[p, -t], [q, s]].

noncomputable def Matrix.torusMap (M : Matrix (Fin 2) (Fin 2) ℤ) (q : Circle × Circle) : Circle × Circle

The monomial self-map of the torus S¹ × S¹ defined by an integral 2 × 2 matrix M, invertible or not: (a, b) ↦ (a ^ M₀₀ * b ^ M₀₁, a ^ M₁₀ * b ^ M₁₁). For invertible M it is the homeomorphism Matrix.GeneralLinearGroup.torusHomeomorph.

@[simp]

theorem Matrix.torusMap_apply (M : Matrix (Fin 2) (Fin 2) ℤ) (q : Circle × Circle) : M.torusMap q = (q.1 ^ M 0 0 * q.2 ^ M 0 1, q.1 ^ M 1 0 * q.2 ^ M 1 1)

The formula for the self-map of the torus induced by a matrix.

theorem Matrix.torusMap_torusMap (M N : Matrix (Fin 2) (Fin 2) ℤ) (q : Circle × Circle) : M.torusMap (N.torusMap q) = (M * N).torusMap q

The self-map of the torus induced by a product of matrices is the composite of their self-maps.

theorem Matrix.torusMap_one (q : Circle × Circle) : torusMap 1 q = q

The identity matrix induces the identity of the torus.

theorem Matrix.continuous_torusMap (M : Matrix (Fin 2) (Fin 2) ℤ) : Continuous M.torusMap

The self-map of the torus induced by a matrix is continuous.

noncomputable def Matrix.torusContinuousMap (M : Matrix (Fin 2) (Fin 2) ℤ) : C(Circle × Circle, Circle × Circle)

The monomial self-map Matrix.torusMap M of the torus, as a continuous map.

@[simp]

theorem Matrix.coe_torusContinuousMap (M : Matrix (Fin 2) (Fin 2) ℤ) : ⇑M.torusContinuousMap = M.torusMap

theorem Matrix.torusContinuousMap_comp (M N : Matrix (Fin 2) (Fin 2) ℤ) : M.torusContinuousMap.comp N.torusContinuousMap = (M * N).torusContinuousMap

The continuous self-map of the torus induced by a product of matrices is the composite of their continuous self-maps.

@[simp]

theorem Matrix.torusContinuousMap_one : torusContinuousMap 1 = ContinuousMap.id (Circle × Circle)

The identity matrix induces the identity map of the torus.

noncomputable def Matrix.GeneralLinearGroup.torusHomeomorph (A : GL (Fin 2) ℤ) : Circle × Circle ≃ₜ Circle × Circle

The homeomorphism of the torus S¹ × S¹ induced by an invertible integral 2 × 2 matrix A, (a, b) ↦ (a ^ A₀₀ * b ^ A₀₁, a ^ A₁₀ * b ^ A₁₁) (Matrix.GeneralLinearGroup.torusHomeomorph_apply). It carries the (p, q) curve to the A (p, q) curve (Matrix.GeneralLinearGroup.torusHomeomorph_torusCurve).

@[simp]

theorem Matrix.GeneralLinearGroup.torusHomeomorph_apply (A : GL (Fin 2) ℤ) (q : Circle × Circle) : A.torusHomeomorph q = (q.1 ^ ↑A 0 0 * q.2 ^ ↑A 0 1, q.1 ^ ↑A 1 0 * q.2 ^ ↑A 1 1)

The formula for the homeomorphism of the torus induced by a matrix.

theorem Matrix.GeneralLinearGroup.coe_torusHomeomorph (A : GL (Fin 2) ℤ) : ⇑A.torusHomeomorph = (↑A).torusMap

The homeomorphism of the torus induced by an invertible matrix is its monomial self-map.

@[simp]

theorem Matrix.GeneralLinearGroup.toContinuousMap_torusHomeomorph (A : GL (Fin 2) ℤ) : ↑A.torusHomeomorph = (↑A).torusContinuousMap

The homeomorphism of the torus induced by an invertible matrix, as a continuous map, is the continuous monomial self-map of the matrix.

@[simp]

theorem Matrix.GeneralLinearGroup.torusHomeomorph_one : torusHomeomorph 1 = Homeomorph.refl (Circle × Circle)

The identity matrix acts on the torus by the identity.

theorem Matrix.GeneralLinearGroup.torusHomeomorph_mul (A B : GL (Fin 2) ℤ) : (A * B).torusHomeomorph = B.torusHomeomorph.trans A.torusHomeomorph

The action of a product of matrices is the composite of their actions.

@[simp]

theorem Matrix.GeneralLinearGroup.symm_torusHomeomorph (A : GL (Fin 2) ℤ) : A.torusHomeomorph.symm = A⁻¹.torusHomeomorph

The inverse of the action of a matrix is the action of the inverse matrix.

theorem Matrix.GeneralLinearGroup.torusHomeomorph_torusCurve (A : GL (Fin 2) ℤ) (p q : ℤ) (t : ↑unitInterval) : A.torusHomeomorph ((TauCeti.torusCurve p q) t) = (TauCeti.torusCurve (↑A 0 0 * p + ↑A 0 1 * q) (↑A 1 0 * p + ↑A 1 1 * q)) t

The action on curves. The homeomorphism of the torus induced by A carries the (p, q) curve t ↦ (exp (2πipt), exp (2πiqt)) to the (A₀₀ p + A₀₁ q, A₁₀ p + A₁₁ q) curve.

@[simp]

theorem Matrix.GeneralLinearGroup.torusHomeomorph_swap : (swap ℤ 0 1).torusHomeomorph = Homeomorph.prodComm Circle Circle

The matrix exchanging the two coordinates acts on the torus by exchanging the two circle factors.

theorem TauCeti.exists_torusHomeomorph_eq_torusGluing (p q s t : ℤ) (h : s * p + t * q = 1) : ∃ (A : GL (Fin 2) ℤ), ↑A = !![p, -t; q, s] ∧ A.torusHomeomorph = torusGluing p q s t h

The determinant-one gluing (a, b) ↦ (a ^ p b ^ (-t), a ^ q b ^ s) is the homeomorphism of the torus induced by the invertible matrix [[p, -t], [q, s]].