English
For i ≠ j with α_i ≠ −α_j, if α_i + α_j ∉ Φ and α_i − α_j ∉ Φ, then the root pairing P.pairing i j = 0 (the result also holds after mapping to the integer pairing).
Русский
Для i ≠ j с α_i ≠ −α_j, если α_i + α_j ∉ Φ и α_i − α_j ∉ Φ, то P.pairing i j = 0.
LaTeX
$$$\forall i,j\in ι,\ (i \neq j) \land (α_i \neq -α_j) \land (α_i + α_j \notin Φ) \land (α_i - α_j \notin Φ) \Rightarrow P.pairing i j = 0$$$
Lean4
theorem root_mem_submodule_iff_of_add_mem_invtSubmodule {K : Type*} [Field K] [NeZero (2 : K)] [Module K M] [Module K N]
{P : RootPairing ι K M N} (q : P.invtRootSubmodule) (hij : P.root i + P.root j ∈ range P.root) :
P.root i ∈ (q : Submodule K M) ↔ P.root j ∈ (q : Submodule K M) :=
by
obtain ⟨q, hq⟩ := q
rw [mem_invtRootSubmodule_iff] at hq
suffices ∀ i j, P.root i + P.root j ∈ range P.root → P.root i ∈ q → P.root j ∈ q by
have aux := this j i (by rwa [add_comm]); tauto
rintro i j ⟨k, hk⟩ hi
rcases eq_or_ne (P.pairing i j) 0 with hij₀ | hij₀
· have hik : P.pairing i k ≠ 0 :=
by
rw [ne_eq, P.pairing_eq_zero_iff, ← root_coroot_eq_pairing, hk]
simpa [P.pairing_eq_zero_iff.mp hij₀] using two_ne_zero
suffices P.root k ∈ q from (q.add_mem_iff_right hi).mp <| hk ▸ this
replace hq : P.root i - P.pairing i k • P.root k ∈ q := by simpa [reflection_apply_root] using hq k hi
rwa [q.sub_mem_iff_right hi, q.smul_mem_iff hik] at hq
· replace hq : P.root i - P.pairing i j • P.root j ∈ q := by simpa [reflection_apply_root] using hq j hi
rwa [q.sub_mem_iff_right hi, q.smul_mem_iff hij₀] at hq
