English
The two-two pairing criterion characterizes when the pair of roots have weight two in both directions, which forces i = j when the index set is finite.
Русский
Критерий пары два-два описывает, когда кокетер вес равен двум в обоих направлениях; в конечном случае это приводит к i = j.
LaTeX
$$$$ (P.pairing i j = 2) \\land (P.pairing j i = 2) \\Rightarrow i = j. $$$$
Lean4
/-- See also `RootPairing.pairingIn_two_two_iff`. -/
@[simp]
theorem pairing_two_two_iff : P.pairing i j = 2 ∧ P.pairing j i = 2 ↔ i = j :=
by
refine ⟨fun ⟨h₁, h₂⟩ ↦ ?_, fun h ↦ by simp [h]⟩
have : ¬LinearIndependent R ![P.root i, P.root j] := by
rw [← coxeterWeight_eq_four_iff_not_linearIndependent, coxeterWeight, h₁, h₂]; norm_num
replace this := P.pairing_smul_root_eq_of_not_linearIndependent this
exact P.root.injective <| smul_right_injective M two_ne_zero (h₂ ▸ this)
