coe_corootSpace_eq_span_singleton

English

The coe-coroot space is generated by a single coroot.

Русский

Пространство ко-коорт образуется порождением одного корота.

LaTeX

$$(corootSpace α).toSubmodule = K ∙ (cartanEquivDual H).symm α$$

Lean4

theorem coe_corootSpace_eq_span_singleton (α : Weight K H L) : (corootSpace α).toSubmodule = K ∙ coroot α := by
  if hα : α.IsZero then simp [hα.eq, coroot_eq_zero_iff.mpr hα]
  else
    set α' := (cartanEquivDual H).symm α
    suffices (K ∙ coroot α) = K ∙ α' by rw [coe_corootSpace_eq_span_singleton']; exact this.symm
    have : IsUnit (2 * (α α')⁻¹) := by simpa using root_apply_cartanEquivDual_symm_ne_zero hα
    change (K ∙ (2 • (α α')⁻¹ • α')) = _
    simpa [← Nat.cast_smul_eq_nsmul K, smul_smul] using Submodule.span_singleton_smul_eq this _

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