English
The weight space generated by the zero weight coincides with the span of the U-objects in Geck construction.
Русский
Весовое пространство,生成ное нулевым весом, совпадает с параллельным охватом оригана U объектов в Geck-конструкции.
LaTeX
$$$\\mathrm{genWeightSpace}(b.support \\oplus \\iota \\to K) (0) = \\operatorname{span}_K (\\operatorname{range} u)$$$
Lean4
theorem coe_genWeightSpace_zero_eq_span_range_u :
genWeightSpace (b.support ⊕ ι → K) (0 : H → K) = span K (range <| u (b := b)) :=
by
refine le_antisymm (fun w hw ↦ Pi.mem_span_range_single_inl_iff.mpr fun i ↦ ?_) ?_
· replace hw : ∀ (x) (hx : x ∈ lieAlgebra b), ⟨x, hx⟩ ∈ H → ∃ k, (x.toLin' ^ k) w = 0 := by
simpa [mem_genWeightSpace] using hw
obtain ⟨j, hj⟩ : ∃ j : b.support, P.pairingIn ℤ i j ≠ 0 :=
by
obtain ⟨j, hj, hj₀⟩ := b.exists_mem_support_pos_pairingIn_ne_zero i
rw [ne_eq, P.pairingIn_eq_zero_iff] at hj₀
exact ⟨⟨j, hj⟩, hj₀⟩
obtain ⟨k, hk⟩ := hw (h j) (h_mem_lieAlgebra j) (h_mem_cartanSubalgebra' j _)
simpa [h_eq_diagonal, ← toLin'_pow, fromBlocks_diagonal_pow, diagonal_pow, mulVec_eq_sum, diagonal_apply, hj] using
congr_fun hk (Sum.inr i)
· rw [span_le]
rintro - ⟨i, rfl⟩
simp only [SetLike.mem_coe, LieSubmodule.mem_toSubmodule, mem_genWeightSpace]
rintro ⟨⟨x, -⟩, hx⟩
exact
⟨1, funext fun j ↦ by simpa using apply_sum_inl_eq_zero_of_mem_span_h i j hx⟩
-- TODO Turn this `Fact` into a lemma: it is always true and may be proved via Perron-Frobenius
-- See https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Eigenvalues.20of.20Cartan.20matrices/near/516844801
