English
Given a representation with an sl2-triple, a simultaneous eigenvector for h and e with prescribed eigenvalues yields a primitive vector for the triple.
Русский
Для представления с тройкой sl2 существующее совместное собственное векторное состояние даёт примитивный вектор тройки.
LaTeX
$$mk' [NoZeroSMulDivisors ℤ M] (t : IsSl2Triple h e f) (m : M) (μ ρ : R) (hm : m ≠ 0) (hm' : ⁅h, m⁆ = μ • m) (he : ⁅e, m⁆ = ρ • m) : HasPrimitiveVectorWith t m μ$$
Lean4
/-- Given a representation of a Lie algebra with distinguished `sl₂` triple, a simultaneous
eigenvector for the action of both `h` and `e` necessarily has eigenvalue zero for `e`. -/
theorem mk' [NoZeroSMulDivisors ℤ M] (t : IsSl2Triple h e f) (m : M) (μ ρ : R) (hm : m ≠ 0) (hm' : ⁅h, m⁆ = μ • m)
(he : ⁅e, m⁆ = ρ • m) : HasPrimitiveVectorWith t m μ
where
ne_zero := hm
lie_h := hm'
lie_e := by
suffices 2 • ⁅e, m⁆ = 0 by simpa using this
rw [← nsmul_lie, ← t.lie_h_e_nsmul, lie_lie, hm', lie_smul, he, lie_smul, hm', smul_smul, smul_smul, mul_comm ρ μ,
sub_self]
