Relations among the generators of PSL(2, ℤ)

In PSL(2, ℤ) the classes of S = (0 -1; 1 0) and U = T * S = (1 -1; 1 0), where T = (1 1; 0 1), satisfy S² = 1 and U³ = 1, and U * S = T. In SL(2, ℤ) the first two products are -1 and the last is -T, so each relation is proved by checking that the corresponding element of SL(2, ℤ) is ±1, that is, central. Likewise U² * S is the class of the lower-triangular matrix T′ = (1 0; 1 1). The classes of S and U generate PSL(2, ℤ), and hence also its opposite group.

U is written (T : PSL(2, ℤ)) * S, the simp-normal form of the class of T * S.

Main results

• TauCeti.ModularGroup.T_mul_S_pow_three: (T * S)³ = -1 in SL(2, ℤ).
• TauCeti.ModularGroup.coe_S_sq, TauCeti.ModularGroup.coe_S_inv: S² = 1 and S⁻¹ = S.
• TauCeti.ModularGroup.coe_T_mul_coe_S_pow_three, TauCeti.ModularGroup.coe_T_mul_coe_S_inv, TauCeti.ModularGroup.coe_T_mul_coe_S_sq_inv: U³ = 1, U⁻¹ = U² and (U²)⁻¹ = U.
• Matrix.ProjectiveSpecialLinearGroup.mul_coe_S_mul_coe_S: g * S * S = g, the product form of S² = 1; in particular U * S = T.
• TauCeti.ModularGroup.closure_coe_S_coe_T_mul_coe_S, TauCeti.ModularGroup.closure_op_coe_S_op_coe_T_mul_coe_S: S and U generate PSL(2, ℤ) and, as right multipliers, PSL(2, ℤ)ᵐᵒᵖ.
• TauCeti.ModularGroup.tPrime, TauCeti.ModularGroup.coe_tPrime, TauCeti.ModularGroup.coe_T_mul_coe_S_sq_mul_coe_S: the matrix T′ = (1 0; 1 1) and U² * S = T′.

theorem TauCeti.ModularGroup.T_mul_S_pow_three : (ModularGroup.T * ModularGroup.S) ^ 3 = -1

U³ = -1 in SL(2, ℤ), for U = T * S.

@[simp]

theorem TauCeti.ModularGroup.coe_S_sq : ↑ModularGroup.S ^ 2 = 1

The class of S has order dividing 2 in PSL(2, ℤ): in SL(2, ℤ), S² = -1.

@[simp]

theorem TauCeti.ModularGroup.coe_S_inv : (↑ModularGroup.S)⁻¹ = ↑ModularGroup.S

The class of S is its own inverse in PSL(2, ℤ).

@[simp]

theorem TauCeti.ModularGroup.coe_T_mul_coe_S_pow_three : (↑ModularGroup.T * ↑ModularGroup.S) ^ 3 = 1

The class of U = T * S has order dividing 3 in PSL(2, ℤ): in SL(2, ℤ), (T * S)³ = -1.

theorem TauCeti.ModularGroup.coe_T_mul_coe_S_inv : (↑ModularGroup.T * ↑ModularGroup.S)⁻¹ = (↑ModularGroup.T * ↑ModularGroup.S) ^ 2

The inverse of the class of U = T * S in PSL(2, ℤ) is U².

@[simp]

theorem TauCeti.ModularGroup.coe_T_mul_coe_S_sq_inv : ((↑ModularGroup.T * ↑ModularGroup.S) ^ 2)⁻¹ = ↑ModularGroup.T * ↑ModularGroup.S

The inverse of U², for U = T * S in PSL(2, ℤ), is U.

theorem TauCeti.ModularGroup.closure_coe_S_coe_T_mul_coe_S : Subgroup.closure {↑ModularGroup.S, ↑ModularGroup.T * ↑ModularGroup.S} = ⊤

The classes of S and U = T * S generate PSL(2, ℤ).

theorem TauCeti.ModularGroup.closure_op_coe_S_op_coe_T_mul_coe_S : Subgroup.closure {MulOpposite.op ↑ModularGroup.S, MulOpposite.op (↑ModularGroup.T * ↑ModularGroup.S)} = ⊤

The classes of S and U = T * S generate PSL(2, ℤ)ᵐᵒᵖ, the group acting on the right.

@[simp]

theorem Matrix.ProjectiveSpecialLinearGroup.mul_coe_S_mul_coe_S (g : ProjectiveSpecialLinearGroup (Fin 2) ℤ) : g * ↑ModularGroup.S * ↑ModularGroup.S = g

Right multiplication by S is an involution of PSL(2, ℤ).

def TauCeti.ModularGroup.tPrime : Matrix.SpecialLinearGroup (Fin 2) ℤ

Popa and Zagier's T′ = (1 0; 1 1), the lower-triangular counterpart of T.

@[simp]

theorem TauCeti.ModularGroup.coe_tPrime : ↑tPrime = !![1, 0; 1, 1]

The matrix of T′.

@[simp]

theorem TauCeti.ModularGroup.coe_T_mul_coe_S_sq_mul_coe_S : (↑ModularGroup.T * ↑ModularGroup.S) ^ 2 * ↑ModularGroup.S = ↑tPrime

In PSL(2, ℤ), U² * S = T′ for U = T * S; in SL(2, ℤ) the product is -T′.