English
Let P be a crystallographic, reduced, irreducible root system with nonempty index set ι. Then the Lie algebra lieAlgebra(b) acts irreducibly on the K-vector space V = (b.support ⊕ ι) → K; equivalently, every Lie submodule of V is either {0} or V.
Русский
Пусть P — кристаллическая, редуцированная и неприводимая корневая система с непустым множеством индексов ι. Тогда над K-модулем V = (помощь b) ⊕ ι → K отображение алгебры Ли lieAlgebra(b) является неразложимым; то есть любая подмодуля Ли V либо равна нулю, либо всему V.
LaTeX
$$$\text{Let }V=(b.\mathrm{support}\oplus ι)\to K.\text{ Then }V\text{ is an irreducible Lie }\\mathfrak{g}\text{-module, i.e. for any Lie submodule }U\\le V,\;U=0\ \text{or}\ U=V.$$$
Lean4
/-- Lemma 4.2 from [Geck](Geck2017). -/
instance instIsIrreducible [Nonempty ι] : LieModule.IsIrreducible K (lieAlgebra b) (b.support ⊕ ι → K) :=
by
refine LieModule.IsIrreducible.mk fun U hU ↦ ?_
suffices ∃ i, v b i ∈ U by obtain ⟨i, hi⟩ := this; exact instIsIrreducible_aux₂ hi
let U' : LieSubmodule K H (b.support ⊕ ι → K) := { U with lie_mem := U.lie_mem }
apply instIsIrreducible_aux₁ U'
contrapose! hU
replace hU : U ≤ span K (range (u (b := b))) := by rwa [← coe_genWeightSpace_zero_eq_span_range_u]
refine (LieSubmodule.eq_bot_iff _).mpr fun x hx ↦ ?_
obtain ⟨c, hc⟩ : ∃ c : b.support → K, ∑ i, c i • u i = x := (mem_span_range_iff_exists_fun K).mp <| hU hx
suffices c = 0 by simp [this, ← hc]
have hCM : (4 - b.cartanMatrix).det ≠ 0 := Fact.out
contrapose! hCM
suffices ((Int.castRingHom K).mapMatrix (4 - b.cartanMatrix)).det = 0 by
simpa only [← RingHom.map_det, eq_intCast, Int.cast_eq_zero] using this
rw [← exists_mulVec_eq_zero_iff]
suffices (b.cartanMatrix.map abs).map (↑) *ᵥ c = 0 from ⟨c, hCM, by simpa using this⟩
ext j
suffices ∑ k, c k * |b.cartanMatrix j k| = 0 by simpa [mulVec_eq_sum, -Base.cartanMatrix_map_abs]
by_contra contra
have key : v b j ∈ U := by
have : ⁅e j, x⁆ ∈ U := U.lie_mem (x := ⟨e j, e_mem_lieAlgebra j⟩) hx
have aux (k : b.support) : ⁅e j, u k⁆ = |b.cartanMatrix j k| • v b j := e_lie_u j k
simp_rw [← hc, lie_sum, lie_smul, aux, smul_comm (M := K), ← smul_assoc, ← Finset.sum_smul, zsmul_eq_mul, mul_comm,
← LieSubmodule.mem_toSubmodule, U.smul_mem_iff contra] at this
assumption
have : v b j ∉ U := fun hj ↦ by simpa [v] using apply_inr_eq_zero_of_mem_span_range_u b j (hU hj)
contradiction
