English
The instance asserts irreducibility of a certain subtype related to weight spaces in the Killing context.
Русский
Инстанс утверждает ирредуцируемость подпространства весов в контексте Killing.
LaTeX
$$(IsIrreducible root system) ∈ IsKilling context$$
Lean4
/-- Constructs a Lie ideal from an invariant submodule of the dual space of a Cartan subalgebra.
Given a submodule `q` of the dual space `Dual K H` that is invariant under all root reflections,
this produces a Lie ideal by taking the sum of all `sl₂` subalgebras corresponding to roots
whose linear forms lie in `q`. -/
noncomputable def invtSubmoduleToLieIdeal (q : Submodule K (Dual K H))
(hq : ∀ i, q ∈ End.invtSubmodule ((rootSystem H).reflection i)) : LieIdeal K L
where
__ := ⨆ α : { α : Weight K H L // ↑α ∈ q ∧ α.IsNonZero }, sl2SubmoduleOfRoot α.2.2
lie_mem := by
intro x m hm
have hx : x ∈ ⨆ χ : Weight K H L, genWeightSpace L χ := by simp [LieModule.iSup_genWeightSpace_eq_top']
induction hx using LieSubmodule.iSup_induction' with
| mem χ x_χ hx_χ =>
induction hm using LieSubmodule.iSup_induction' with
| mem α m_α hm_α => exact invtSubmoduleToLieIdeal_aux q hq χ x_χ m_α hx_χ α.1 α.2.1 α.2.2 hm_α
| zero => simp only [Submodule.carrier_eq_coe, lie_zero, SetLike.mem_coe, zero_mem]
| add m₁ m₂ _ _ ih₁
ih₂ =>
simp only [lie_add, Submodule.carrier_eq_coe, SetLike.mem_coe] at ih₁ ih₂ ⊢
exact add_mem ih₁ ih₂
| zero => simp only [Submodule.carrier_eq_coe, zero_lie, SetLike.mem_coe, zero_mem]
| add x₁ x₂ _ _ ih₁
ih₂ =>
simp only [add_lie, Submodule.carrier_eq_coe, SetLike.mem_coe] at ih₁ ih₂ ⊢
exact add_mem ih₁ ih₂
