English
If indices i ≠ j, then b.cartanMatrix i j lies among the finite integer set {−3,−2,−1,0}, reflecting root-pairing constraints.
Русский
Если i ≠ j, то Cartan(i,j) принадлежит ограниченному множеству {−3,−2,−1,0}.
LaTeX
$$$b.cartanMatrix i j \\in \\{ -3, -2, -1, 0 \\}$ for i ≠ j$$
Lean4
theorem cartanMatrix_mem_of_ne {i j : b.support} (hij : i ≠ j) : b.cartanMatrix i j ∈ ({-3, -2, -1, 0} : Set ℤ) :=
by
have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
have : Module.IsReflexive R N := .of_isPerfPair P.flip.toLinearMap
simp only [cartanMatrix, cartanMatrixIn_def]
have h₁ := P.pairingIn_pairingIn_mem_set_of_isCrystallographic i j
have h₂ : P.pairingIn ℤ i j ≤ 0 := b.cartanMatrix_le_zero_of_ne i j hij
suffices P.pairingIn ℤ i j ≠ -4 by aesop
by_contra contra
replace contra : P.pairingIn ℤ j i = -1 ∧ P.pairingIn ℤ i j = -4 := ⟨by simp_all, contra⟩
rw [pairingIn_neg_one_neg_four_iff] at contra
refine (not_linearIndependent_iff.mpr ?_) b.linearIndepOn_root
refine ⟨⟨{ i, j }, by simpa⟩, Finsupp.single i (1 : R) + Finsupp.single j (2 : R), ?_⟩
simp [contra, hij, hij.symm]
