/-- **Sanov's theorem (1947).** The matrices `A = [[1, 2], [0, 1]]` and `B = [[1, 0], [2, 1]]`
generate a free group of rank two inside `SL(2, ℤ)`: the homomorphism from the free group on two
letters sending the letters to `A` and `B` is injective, so no non-trivial reduced word in
`A^{±1}, B^{±1}` equals the identity. Proof by **ping-pong** on `ℤ²`: let `X₀ = {|x| > |y|}` and
`X₁ = {|x| < |y|}`; non-zero powers of `A` send `X₁` into `X₀` (`upper_ping`) and non-zero powers
of `B` send `X₀` into `X₁` (`lower_pong`). Mathlib's ping-pong lemma for free products
(`Monoid.CoprodI.lift_injective_of_ping_pong`) turns these two estimates into injectivity, via
`F₂ ≅ ℤ * ℤ` (`freeGroupEquivCoprodI`). -/
theorem sanov_free : Function.Injective (FreeGroup.lift ![sanovA, sanovB]) := by
classical
-- The ping-pong table: `X 0 = {|x| > |y|}` and `X 1 = {|x| < |y|}`.
let X : Fin 2 → Set (Fin 2 → ℤ) := ![{v | |v 1| < |v 0|}, {v | |v 0| < |v 1|}]
let H : Fin 2 → Type := fun _ => FreeGroup Unit
let f : ∀ i, H i →* SL(2, ℤ) := fun i => FreeGroup.lift fun _ => ![sanovA, sanovB] i
-- A free group is the free product of copies of `ℤ = FreeGroup Unit`.
have hlift : FreeGroup.lift ![sanovA, sanovB] =
(Monoid.CoprodI.lift f).comp (@freeGroupEquivCoprodI (Fin 2)).toMonoidHom := by
refine FreeGroup.ext_hom _ _ fun i => ?_
simp only [f, MonoidHom.coe_comp, MulEquiv.coe_toMonoidHom, Function.comp_apply,
freeGroupEquivCoprodI_apply]
rw [FreeGroup.lift_apply_of, FreeGroup.lift_apply_of, Monoid.CoprodI.lift_of,
FreeGroup.lift_apply_of]
rw [hlift, MonoidHom.coe_comp]
refine Function.Injective.comp ?_ (MulEquiv.injective _)
refine Monoid.CoprodI.lift_injective_of_ping_pong f ?_ X ?_ ?_ ?_
· -- one factor has at least three elements
right
refine ⟨0, ?_⟩
simp only [H]
rw [FreeGroup.freeGroupUnitEquivInt.cardinal_eq, Cardinal.mk_denumerable]
exact natCast_le_aleph0
· intro i
fin_cases i
· exact ⟨![1, 0], by simp [X]⟩
· exact ⟨![0, 1], by simp [X]⟩
· intro i j hij
fin_cases i <;> fin_cases j
· exact absurd rfl hij
· exact Set.disjoint_left.2 fun v h1 h2 => by simp [X] at h1 h2; linarith
· exact Set.disjoint_left.2 fun v h1 h2 => by simp [X] at h1 h2; linarith
· exact absurd rfl hij
· intro i j hij
refine FreeGroup.freeGroupUnitEquivInt.forall_congr_left.mpr ?_
intro n hne1
have hn : n ≠ 0 := by
rintro rfl
apply hne1
simp [FreeGroup.freeGroupUnitEquivInt]
change FreeGroup.lift (fun _ => ![sanovA, sanovB] i) (FreeGroup.of () ^ n) • X j ⊆ X i
rw [map_zpow, FreeGroup.lift_apply_of]
rw [Set.smul_set_subset_iff]
fin_cases i <;> fin_cases j
· exact absurd rfl hij
· intro v hv
have hpow : sanovA ^ n = upperHom (Multiplicative.ofAdd n) := by
rw [sanovA, ← map_zpow, ← ofAdd_zsmul, smul_eq_mul, mul_one]
change |v 0| < |v 1| at hv
change |(sanovA ^ n • v) 1| < |(sanovA ^ n • v) 0|
rw [hpow]
exact upper_ping n hn v hv
· intro v hv
have hpow : sanovB ^ n = lowerHom (Multiplicative.ofAdd n) := by
rw [sanovB, ← map_zpow, ← ofAdd_zsmul, smul_eq_mul, mul_one]
change |v 1| < |v 0| at hv
change |(sanovB ^ n • v) 0| < |(sanovB ^ n • v) 1|
rw [hpow]
exact lower_pong n hn v hv
· exact absurd rfl hij