English
Linear independence of the two roots is equivalent to both indices being different and roots not summing to a negation, in the Coxeter framework.
Русский
Линейная независимость пары корней эквивалентна разности индексов и тому, что корни не равны минус друг друга в рамках кокетерной теории.
LaTeX
$$$$ \\operatorname{LI}_R(\\![P.root i, P.root j]\\!) \\iff i \\neq j \\wedge P.root i \\neq -P.root j. $$$$
Lean4
/-- See also `RootPairing.linearIndependent_iff_coxeterWeightIn_ne_four`. -/
theorem linearIndependent_iff_coxeterWeight_ne_four :
LinearIndependent R ![P.root i, P.root j] ↔ P.coxeterWeight i j ≠ 4 :=
by
have : NoZeroSMulDivisors ℤ M := NoZeroSMulDivisors.int_of_charZero R M
refine ⟨coxeterWeight_ne_four_of_linearIndependent P, fun h ↦ ?_⟩
contrapose! h
have h₁ := P.pairing_smul_root_eq_of_not_linearIndependent h
rw [LinearIndependent.pair_symm_iff] at h
have h₂ := P.pairing_smul_root_eq_of_not_linearIndependent h
suffices P.coxeterWeight i j • P.root i = (4 : R) • P.root i from smul_left_injective R (P.ne_zero i) this
calc
P.coxeterWeight i j • P.root i = (P.pairing i j * P.pairing j i) • P.root i := by rfl
_ = P.pairing i j • (2 : R) • P.root j := by rw [mul_smul, h₁]
_ = (4 : R) • P.root i := by rw [smul_comm, h₂, ← mul_smul]; norm_num
