OAI/Algebra/AffineCancellation/HighestWeight.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ComplexCancellation.SL2.no_negative_highest line 12

   Source documentation

   A highest weight vector in a locally finite sl₂ representation has nonnegative weight. Only local nilpotence of the lowering operator on this vector is needed.

   lemma no_negative_highest (δ η H : R →ₗ[ℂ] R)
       (hcomm : ∀ r, δ (η r) - η (δ r) = H r)
       (hlower : ∀ r, H (η r) = η (H r) - (2 : ℂ) • η r)
       (r : R) (w : ℤ) (hw : w < 0) (hδ : δ r = 0)
       (hH : H r = (w : ℂ) • r) (hη : ∃ n : ℕ, (η : R → R)^[n] r = 0) : r = 0 := by
   …

   Mentions: OAI.ComplexCancellation.H