English
For a crystallographic root system, the map (i,k) ↦ P.pairingIn ℤ i k is injective in i for each k, implying linear independence of root-related maps.
Русский
Для кристаллической корневой системы отображение (i,k) ↦ P.pairingIn ℤ i k инъективно по i для каждого k; это порождает линейную независимость соответствующих образов корней.
LaTeX
$$Injective (fun i k => P.pairingIn ℤ i k)$$
Lean4
theorem root_sub_nsmul_mem_range_iff_le_chainBotCoeff {n : ℕ} :
P.root j - n • P.root i ∈ range P.root ↔ n ≤ P.chainBotCoeff i j :=
by
set S : Set ℤ := {z | P.root j + z • P.root i ∈ range P.root} with S_def
suffices -(n : ℤ) ∈ S ↔ n ≤ P.chainBotCoeff i j by
simpa only [S_def, mem_setOf_eq, neg_smul, natCast_zsmul, ← sub_eq_add_neg] using this
have aux : P.chainBotCoeff i j = (-(P.setOf_root_add_zsmul_eq_Icc_of_linearIndependent h).choose).toNat := by
simp [chainBotCoeff, h]
obtain ⟨hq, p, hp, h₂ : S = _⟩ := (P.setOf_root_add_zsmul_eq_Icc_of_linearIndependent h).choose_spec
rw [aux, h₂, mem_Icc]
cutsat
