English
If x is in the lieAlgebra b, then ωConj b x lies in lieAlgebra b.
Русский
Если x ∈ lieAlgebra b, то ωConj b x ∈ lieAlgebra.
LaTeX
$$$x \\in \\mathrm{lieAlgebra}(b) \\Rightarrow \\omegaConj(b)\\, x \\in \\mathrm{lieAlgebra}(b)$$$
Lean4
/-- This is Lemma 2.5 (a) from [Geck](Geck2017). -/
theorem root_sub_root_mem_of_mem_of_mem (hk : α k + α i - α j ∈ Φ) (hkj : k ≠ j) (hk' : α k + α i ∈ Φ) :
α k - α j ∈ Φ := by
rcases lt_or_ge 0 (P.pairingIn ℤ j k) with hm | hm
· rw [← neg_mem_range_root_iff, neg_sub]
exact P.root_sub_root_mem_of_pairingIn_pos hm hkj.symm
obtain ⟨l, hl⟩ := hk
have hli : l ≠ i := by
rintro rfl
rw [add_comm, add_sub_assoc, left_eq_add, sub_eq_zero, P.root.injective.eq_iff] at hl
exact hkj hl
suffices 0 < P.pairingIn ℤ l i
by
convert P.root_sub_root_mem_of_pairingIn_pos this hli using 1
rw [hl]
module
have hkl : l ≠ k := by rintro rfl; exact hij <| by simpa [add_sub_assoc, sub_eq_zero] using hl
replace hkl : P.pairingIn ℤ l k ≤ 0 :=
by
suffices α l - α k ∉ Φ by contrapose! this; exact P.root_sub_root_mem_of_pairingIn_pos this hkl
replace hl : α l - α k = α i - α j := by rw [hl]; module
rw [hl]
exact b.sub_notMem_range_root hi hj
have hki : P.pairingIn ℤ i k ≤ -2 :=
by
suffices P.pairingIn ℤ l k = 2 + P.pairingIn ℤ i k - P.pairingIn ℤ j k by linarith
apply algebraMap_injective ℤ R
simp only [algebraMap_pairingIn, map_sub, map_add, map_ofNat]
simpa using (P.coroot' k : M →ₗ[R] R).congr_arg hl
replace hki : P.pairingIn ℤ k i = -1 :=
by
replace hk' : α i ≠ -α k := by
rw [← sub_ne_zero, sub_neg_eq_add, add_comm]
intro contra
rw [contra] at hk'
exact P.ne_zero _ hk'.choose_spec
have aux (h : P.pairingIn ℤ i k = -2) : ¬P.pairingIn ℤ k i = -2 :=
by
have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
contrapose! hk'; exact (P.pairingIn_neg_two_neg_two_iff ℤ i k).mp ⟨h, hk'⟩
have := P.pairingIn_pairingIn_mem_set_of_isCrystallographic i k
aesop -- https://github.com/leanprover-community/mathlib4/issues/24551 (this should be faster)
replace hki : P.pairing k i = -1 := by rw [← P.algebraMap_pairingIn ℤ, hki]; simp
have : P.pairingIn ℤ l i = 1 - P.pairingIn ℤ j i :=
by
apply algebraMap_injective ℤ R
simp only [algebraMap_pairingIn, map_sub, map_one, algebraMap_pairingIn]
convert (P.coroot' i : M →ₗ[R] R).congr_arg hl using 1
simp only [map_sub, map_add, LinearMap.flip_apply, root_coroot_eq_pairing, hki, pairing_same, sub_left_inj]
ring
replace hij := pairingIn_le_zero_of_ne b hij.symm hj hi
omega
