Free groups of countable rank are linear over ℤ

The matrices A = [[1, 2], [0, 1]] and B = [[1, 0], [2, 1]] freely generate a free subgroup of rank two of SL(2, ℤ) (Sanov). The proof is ping-pong on ℤ²: every nonzero power of A maps the cone {|x| < |y|} into the cone {|y| < |x|}, and every nonzero power of B does the reverse. In Mathlib's vocabulary, A and B are the transvections Matrix.SpecialLinearGroup.transvection with parameter 2 at the positions (0, 1) and (1, 0).

The conjugates Bᵏ A B⁻ᵏ, for k ranging over any set of distinct integers, also freely generate a free subgroup. Hence every free group of countable rank embeds in SL(2, ℤ), and, comparing with the rank-two embedding, the elements bᵏ a b⁻ᵏ of the free group F(a, b) freely generate a free subgroup of F(a, b). In particular FreeGroup (Fin n) embeds in FreeGroup (Fin 2) by sending the i-th generator to bⁱ a b⁻ⁱ.

Linearity over the Noetherian ring ℤ is the input from which equational Noetherianity of free groups of finite rank follows, through the Hilbert basis theorem.

Main results

• TauCeti.injective_freeGroup_lift_transvection_of_two_le_abs: Sanov's theorem, in the general form over a linearly ordered commutative ring: the transvections with parameters c, d, 2 ≤ |c|, 2 ≤ |d|, freely generate a free subgroup of SL(2, R).
• TauCeti.injective_freeGroup_lift_conj_transvection_of_two_le_abs: the conjugates Bᵏ A B⁻ᵏ for distinct k freely generate a free subgroup of SL(2, R).
• TauCeti.injective_freeGroup_lift_transvection_two: Sanov's theorem, A and B freely generate a free subgroup of SL(2, ℤ).
• TauCeti.injective_freeGroup_lift_conj_transvection_two: the conjugates Bᵏ A B⁻ᵏ for distinct k freely generate a free subgroup of SL(2, ℤ).
• TauCeti.exists_injective_freeGroup_SL: every free group of countable rank embeds in SL(2, ℤ).
• TauCeti.injective_freeGroup_lift_conj_zpow_of: the elements bᵏ a b⁻ᵏ for distinct k freely generate a free subgroup of FreeGroup (Fin 2).

References

• I. N. Sanov, A property of a representation of a free group, Doklady Akad. Nauk SSSR 57 (1947), 657–659.
• P. de la Harpe, Topics in geometric group theory, University of Chicago Press, 2000, §II.B.
• G. Baumslag, A. Myasnikov, V. Remeslennikov, Algebraic geometry over groups I. Algebraic sets and ideal theory, J. Algebra 219 (1999), §2.2 (free groups are linear, hence equationally Noetherian).

theorem TauCeti.injective_freeGroup_lift_transvection_of_two_le_abs {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {c d : R} (hc : 2 ≤ |c|) (hd : 2 ≤ |d|) : Function.Injective ⇑(FreeGroup.lift ![Matrix.SpecialLinearGroup.transvection ⋯ c, Matrix.SpecialLinearGroup.transvection ⋯ d])

Sanov's theorem, in the general form over a linearly ordered commutative ring R: for c, d : R with 2 ≤ |c| and 2 ≤ |d|, the matrices [[1, c], [0, 1]] and [[1, 0], [d, 1]] freely generate a free subgroup of rank two of SL(2, R).

theorem TauCeti.injective_freeGroup_lift_conj_transvection_of_two_le_abs {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {ι : Type u_2} {k : ι → ℤ} (hk : Function.Injective k) {c d : R} (hc : 2 ≤ |c|) (hd : 2 ≤ |d|) : Function.Injective ⇑(FreeGroup.lift fun (i : ι) => Matrix.SpecialLinearGroup.transvection ⋯ d ^ k i * Matrix.SpecialLinearGroup.transvection ⋯ c * (Matrix.SpecialLinearGroup.transvection ⋯ d ^ k i)⁻¹)

For distinct integers k i, the conjugates Bᵏ⁽ⁱ⁾ A B⁻ᵏ⁽ⁱ⁾ of A = [[1, c], [0, 1]] by powers of B = [[1, 0], [d, 1]], with 2 ≤ |c| and 2 ≤ |d|, freely generate a free subgroup of SL(2, R).

theorem TauCeti.injective_freeGroup_lift_transvection_two : Function.Injective ⇑(FreeGroup.lift ![Matrix.SpecialLinearGroup.transvection ⋯ 2, Matrix.SpecialLinearGroup.transvection ⋯ 2])

Sanov's theorem. The matrices [[1, 2], [0, 1]] and [[1, 0], [2, 1]] freely generate a free subgroup of rank two of SL(2, ℤ). This is the case R = ℤ, c = d = 2 of injective_freeGroup_lift_transvection_of_two_le_abs.

theorem TauCeti.injective_freeGroup_lift_conj_transvection_two {ι : Type u_2} {k : ι → ℤ} (hk : Function.Injective k) : Function.Injective ⇑(FreeGroup.lift fun (i : ι) => Matrix.SpecialLinearGroup.transvection ⋯ 2 ^ k i * Matrix.SpecialLinearGroup.transvection ⋯ 2 * (Matrix.SpecialLinearGroup.transvection ⋯ 2 ^ k i)⁻¹)

For distinct integers k i, the conjugates Bᵏ⁽ⁱ⁾ A B⁻ᵏ⁽ⁱ⁾ of A = [[1, 2], [0, 1]] by powers of B = [[1, 0], [2, 1]] freely generate a free subgroup of SL(2, ℤ). This is the case R = ℤ, c = d = 2 of injective_freeGroup_lift_conj_transvection_of_two_le_abs.

theorem TauCeti.exists_injective_freeGroup_SL (ι : Type u_2) [Countable ι] : ∃ (f : FreeGroup ι →* Matrix.SpecialLinearGroup (Fin 2) ℤ), Function.Injective ⇑f

Free groups of countable rank are linear over ℤ. Every free group on a countable basis embeds in SL(2, ℤ).

theorem TauCeti.injective_freeGroup_lift_conj_zpow_of {ι : Type u_2} {k : ι → ℤ} (hk : Function.Injective k) : Function.Injective ⇑(FreeGroup.lift fun (i : ι) => FreeGroup.of 1 ^ k i * FreeGroup.of 0 * (FreeGroup.of 1 ^ k i)⁻¹)

For distinct integers k i, the elements bᵏ⁽ⁱ⁾ a b⁻ᵏ⁽ⁱ⁾ of the free group F(a, b) freely generate a free subgroup. In particular FreeGroup (Fin n) embeds in FreeGroup (Fin 2) by sending the i-th generator to bⁱ a b⁻ⁱ.