English
The omega-conjugate Lie submodule is top if and only if the starting submodule is top.
Русский
Ли-подмодуль, полученный через ω-коньюгирование, равен верхнему, если и только если исходный подмодуль равен верхнему.
LaTeX
$$$\\omegaConjLieSubmodule N = \\top \\iff N = \\top$$$
Lean4
/-- This is Lemma 2.5 (b) from [Geck](Geck2017). -/
theorem root_add_root_mem_of_mem_of_mem (hk : α k + α i - α j ∈ Φ) (hkj : α k ≠ -α i) (hk' : α k - α j ∈ Φ) :
α k + α i ∈ Φ := by
let _i := P.indexNeg
replace hk : α (-k) + α j - α i ∈ Φ := by
rw [← neg_mem_range_root_iff]
convert hk using 1
simp only [indexNeg_neg, root_reflectionPerm, reflection_apply_self]
module
rw [← neg_mem_range_root_iff]
convert
b.root_sub_root_mem_of_mem_of_mem j i (-k) hij.symm hj hi hk (by contrapose! hkj; aesop)
(by convert P.neg_mem_range_root_iff.mpr hk' using 1; simp [neg_add_eq_sub]) using
1
simp only [indexNeg_neg, root_reflectionPerm, reflection_apply_self]
module
