$S$ and $T$ generate $SL(2,\mathbb Z)$

Proved

TongString.SL2Z_closure_S_T

by Lucas · Sep 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

modular-groupstring-theory

Let $S=\begin{pmatrix}0&-1\\1&0\end{pmatrix}$ and $T=\begin{pmatrix}1&1\\0&1\end{pmatrix}$ . Then the subgroup of $SL(2,\mathbb Z)$ generated by $S$ and $T$ is all of $SL(2,\mathbb Z)$ :

\langle S,T\rangle=SL(2,\mathbb Z).

This is the statement that every modular transformation (6.19) "is constructed from combinations of $S$ and $T$ ", which reduces modular invariance to invariance under $S$ and $T$ .

Preamble

import Mathlib
import Definitions.Def_TongString_modular_action

Formal statement

namespace TongString

theorem SL2Z_closure_S_T : Subgroup.closure {modularS, modularT} = ⊤ := by sorry

end TongString

Source

D. Tong, *String Theory*, University of Cambridge Part III Mathematical Tripos lecture notes (January 2009), http://www.damtp.cam.ac.uk/user/tong/string.html, Section 6.4.1, p. 146 ('A general modular transformation is constructed from combinations of S and T ...', eq. (6.19))

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic), non-blind: same agent that drafted the statement

Non-blind read-back. This read-back was written by the same agent that drafted the Lean statement, with full knowledge of the source text and of the intended meaning. It is not independent testimony and must not be treated as a blind audit; a reviewer should compare the Lean code against the source directly.

The statement asserts that the smallest subgroup of the group $SL(2,\mathbb Z)$ ( $2\times2$ integer matrices of determinant $1$ under matrix multiplication) containing the two elements

S=\begin{pmatrix}0&-1\\1&0\end{pmatrix},\qquad T=\begin{pmatrix}1&1\\0&1\end{pmatrix}

is the whole group $SL(2,\mathbb Z)$ . There are no hypotheses. The statement is about matrices, not about the maps $\tau\mapsto(a\tau+b)/(c\tau+d)$ .

View graph

SSS and TTT generate SL(2,Z)SL(2,\mathbb Z)SL(2,Z)

$S$ and $T$ generate $SL(2,\mathbb Z)$