English
A characterization of the connectedness of the Dynkin diagram for irreducible root pairings: if a property p on the simple roots holds at some i and, whenever p(i) and the Cartan matrix entry to j is nonzero implies p(j), then p holds for all simple roots j.
Русский
Характеризация связности диаграммы Динкина для неразделимых пар корней: если свойство p на простых корнях выполняется в точке i и если из p(i) следует p(j) при ненулевой записи Картона, то p выполнено для всех простых корней j.
LaTeX
$$$[P.IsReduced]([P.IsIrreducible])\; (p: b.support \to \{0,1\}) (i)\; (hi: p(i))\; (hp: \forall i,j, p(i) \Rightarrow (b.cartanMatrix(j,i) \neq 0 \Rightarrow p(j))) \Longrightarrow p(j)$$$
Lean4
/-- Note that it is often more convenient to use `RootPairing.root_add_zsmul_mem_range_iff` than
to invoke this lemma directly. -/
theorem setOf_root_add_zsmul_eq_Icc_of_linearIndependent (h : LinearIndependent R ![P.root i, P.root j]) :
∃ᵉ (q ≤ 0) (p ≥ 0), {z : ℤ | P.root j + z • P.root i ∈ range P.root} = Icc q p :=
by
replace h := LinearIndependent.pair_iff.mp <| h.restrict_scalars' ℤ
set S : Set ℤ := {z | P.root j + z • P.root i ∈ range P.root} with S_def
have hS₀ : 0 ∈ S := by simp [S]
have h_fin : S.Finite :=
by
suffices Injective (fun z : S ↦ z.property.choose) from Finite.of_injective _ this
intro ⟨z, hz⟩ ⟨z', hz'⟩ hzz
have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
have : NoZeroSMulDivisors ℤ M := .int_of_charZero R M
have : z • P.root i = z' • P.root i := by
rwa [← add_right_inj (P.root j), ← hz.choose_spec, ← hz'.choose_spec, P.root.injective.eq_iff]
exact Subtype.ext <| smul_left_injective ℤ (P.ne_zero i) this
have h_ne : S.Nonempty := ⟨0, by simp [S_def]⟩
refine
⟨sInf S, csInf_le h_fin.bddBelow hS₀, sSup S, le_csSup h_fin.bddAbove hS₀,
(h_ne.eq_Icc_iff_int h_fin.bddBelow h_fin.bddAbove).mpr fun r ⟨k, hk⟩ s ⟨l, hl⟩ hrs ↦ ?_⟩
by_contra! contra
have hki_notMem : P.root k + P.root i ∉ range P.root :=
by
replace hk : P.root k + P.root i = P.root j + (r + 1) • P.root i := by rw [hk]; module
replace contra : r + 1 ∉ S := hrs.notMem_of_mem_left <| by simp [contra]
simpa only [hk, S_def, mem_setOf_eq, S] using contra
have hki_ne : P.root k ≠ -P.root i := by
rw [hk]
contrapose! h
replace h : r • P.root i = -P.root j - P.root i := by rw [← sub_eq_of_eq_add h.symm]; module
exact ⟨r + 1, 1, by simp [add_smul, h], by cutsat⟩
have hli_notMem : P.root l - P.root i ∉ range P.root :=
by
replace hl : P.root l - P.root i = P.root j + (s - 1) • P.root i := by rw [hl]; module
replace contra : s - 1 ∉ S := hrs.notMem_of_mem_left <| by simp [lt_sub_right_of_add_lt contra]
simpa only [hl, S_def, mem_setOf_eq, S] using contra
have hli_ne : P.root l ≠ P.root i := by
rw [hl]
contrapose! h
replace h : s • P.root i = P.root i - P.root j := by rw [← sub_eq_of_eq_add h.symm]; module
exact ⟨s - 1, 1, by simp [sub_smul, h], by cutsat⟩
have h₁ : 0 ≤ P.pairingIn ℤ k i :=
by
have := P.root_add_root_mem_of_pairingIn_neg (i := k) (j := i)
contrapose! this
exact ⟨this, hki_ne, hki_notMem⟩
have h₂ : P.pairingIn ℤ k i = P.pairingIn ℤ j i + r * 2 :=
by
apply algebraMap_injective ℤ R
rw [algebraMap_pairingIn, map_add, map_mul, algebraMap_pairingIn, ← root_coroot'_eq_pairing, hk]
simp
have h₃ : P.pairingIn ℤ l i ≤ 0 :=
by
have := P.root_sub_root_mem_of_pairingIn_pos (i := l) (j := i)
contrapose! this
exact ⟨this, fun x ↦ hli_ne (congrArg P.root x), hli_notMem⟩
have h₄ : P.pairingIn ℤ l i = P.pairingIn ℤ j i + s * 2 :=
by
apply algebraMap_injective ℤ R
rw [algebraMap_pairingIn, map_add, map_mul, algebraMap_pairingIn, ← root_coroot'_eq_pairing, hl]
simp
cutsat
