isCompl_ker_weight_span_coroot — Mathlib

English

The kernel of weights and the coroot submodule are complementary as a direct sum inside the ambient space.

Русский

Ядро весов и коротовое подмножество образуют прямую сумму в пространстве.

LaTeX

$$IsCompl(α.ker, K ∙ coroot α)$$

Lean4

theorem isCompl_ker_weight_span_coroot (α : Weight K H L) : IsCompl α.ker (K ∙ coroot α) := by
  if hα : α.IsZero then
    simpa [Weight.coe_toLinear_eq_zero_iff.mpr hα, coroot_eq_zero_iff.mpr hα, Weight.ker] using isCompl_top_bot
  else
    rw [← coe_corootSpace_eq_span_singleton]
    apply Module.Dual.isCompl_ker_of_disjoint_of_ne_bot (by simp_all) (disjoint_ker_weight_corootSpace α)
    replace hα : corootSpace α ≠ ⊥ := by simpa using hα
    rwa [ne_eq, ← LieSubmodule.toSubmodule_inj] at hα

Похожие утверждения