Integer matrices acting on tori, and straight loops

A torus is a product ∀ i, AddCircle (p i) of additive circles. An integer matrix A : Matrix κ ι ℤ acts by the continuous additive map Matrix.smulVecHom A (AddCircle p) from ι → AddCircle p to κ → AddCircle p, sending x to k ↦ ∑ i, A k i • x i. For p = 1 these are Mathlib's tori UnitAddTorus ι = ℝⁱ / ℤⁱ, and this is the map induced by the linear map A : ℝⁱ → ℝᵏ.

For n : ι → ℤ, the straight loop TauCeti.torusLoop p n is the image in the torus of the segment from 0 to (n i • p i)ᵢ: it winds n i times around the i-th circle. Integer matrices act on these loops through Matrix.mulVec (Matrix.smulVecHom_comp_torusLoop). They are the representatives used to compute the fundamental group and first homology of a torus naturally in the matrix.

def TauCeti.torusLoop {ι : Type u_1} (p : ι → ℝ) (n : ι → ℤ) : Path 0 0

The straight loop in the torus ∀ i, AddCircle (p i) winding n i times around the i-th circle: the image of the segment from 0 to (n i • p i)ᵢ in ι → ℝ.

@[simp]

theorem TauCeti.torusLoop_apply {ι : Type u_1} (p : ι → ℝ) (n : ι → ℤ) (t : ↑unitInterval) (i : ι) : (torusLoop p n) t i = ↑(↑t * n i • p i)

theorem Matrix.smulVecHom_comp_torusLoop {ι : Type u_1} {κ : Type u_2} [Fintype ι] (A : Matrix κ ι ℤ) (p : ℝ) (n : ι → ℤ) : (↑(A.smulVecHom (AddCircle p))).comp (TauCeti.torusLoop (fun (x : ι) => p) n).toContinuousMap = (TauCeti.torusLoop (fun (x : κ) => p) (A.mulVec n)).toContinuousMap

An integer matrix sends the straight loop of n to the straight loop of A *ᵥ n.