English
If two root vectors are linearly independent, then their Coxeter weight is not equal to four.
Русский
Если две корневые векторы линейно независимы, их кокетер вес не равен четырём.
LaTeX
$$$$ \\operatorname{LI}_R(\\![P.root i, P.root j]\\!) \\Rightarrow P.coxeterWeight i j \\neq 4. $$$$
Lean4
theorem pairing_one_four_iff' (h2 : IsSMulRegular R (2 : R)) :
P.pairing i j = 1 ∧ P.pairing j i = 4 ↔ P.root j = (2 : R) • P.root i :=
by
have _i : NoZeroSMulDivisors ℤ M := NoZeroSMulDivisors.int_of_charZero R M
have _i : NoZeroSMulDivisors ℤ N := NoZeroSMulDivisors.int_of_charZero R N
refine ⟨fun ⟨h₁, h₂⟩ ↦ ?_, fun h ↦ ?_⟩
· have : ¬LinearIndependent R ![P.root i, P.root j] := by
rw [← coxeterWeight_eq_four_iff_not_linearIndependent, coxeterWeight, h₁, h₂]; simp
replace this := P.pairing_smul_root_eq_of_not_linearIndependent this
rw [h₂, show (4 : R) = 2 * 2 by norm_num, mul_smul] at this
exact smul_right_injective M two_ne_zero this.symm
· rw [← coroot_eq_smul_coroot_iff] at h
rw [pairing, pairing, h]
norm_num
suffices (2 : R) • P.pairing i j = (2 : R) • 1 from h2 this
rw [pairing, ← map_smul, ← h]
simp
