English
Conjugation by ω preserves lieAlgebra membership: if x lies in lieAlgebra b, so does ωConj b x.
Русский
Сопряжение ω сохраняет принадлежность к lieAlgebra: если x ∈ lieAlgebra b, то и ωConj b x ∈ lieAlgebra.
LaTeX
$$If $x ∈ \\mathrm{lieAlgebra}(b)$ then $\\omegaConj(b)\\, x ∈ \\mathrm{lieAlgebra}(b)$$$
Lean4
theorem ωConj_mem_of_mem {x : Matrix (b.support ⊕ ι) (b.support ⊕ ι) R} (hx : x ∈ lieAlgebra b) :
ωConj b x ∈ lieAlgebra b := by
induction hx using LieSubalgebra.lieSpan_induction with
| mem u
hu =>
obtain (⟨i, rfl⟩ | ⟨i, rfl⟩ | ⟨i, rfl⟩) : (∃ j, h j = u) ∨ (∃ j, e j = u) ∨ (∃ j, f j = u) := by
simpa only [mem_union, mem_range, or_assoc] using hu
· rw [← neg_mem_iff]
exact LieSubalgebra.subset_lieSpan <| by simp [ω_mul_h, mul_assoc]
· exact LieSubalgebra.subset_lieSpan <| by simp [ω_mul_e, mul_assoc]
· exact LieSubalgebra.subset_lieSpan <| by simp [ω_mul_f, mul_assoc]
| zero => simp
| add u v _ _ hu hv => simpa [mul_add, add_mul] using add_mem hu hv
| smul t u _ hu => simpa using SMulMemClass.smul_mem _ hu
| lie u v _ _ hu hv =>
rw [LieEquiv.map_lie]
exact (lieAlgebra b).lie_mem hu hv
