English
For a primitive vector, the action of h on the ψ-sequence grows by μ − 2n at step n, i.e., [h, ψ_n] = (μ − 2n) ψ_n.
Русский
Действие h на последовательность ψ_n возрастает на каждом шаге по мере роста μ − 2n: [h, ψ_n] = (μ − 2n) ψ_n.
LaTeX
$$∀ n, \,[h, ψ_n] = (μ - 2·n) · ψ_n$$
Lean4
/-- The subalgebra associated to an `sl₂` triple. -/
def toLieSubalgebra (t : IsSl2Triple h e f) : LieSubalgebra R L
where
__ := span R { e, f, h }
lie_mem' {x y} hx
hy := by
simp only [carrier_eq_coe, SetLike.mem_coe] at hx hy ⊢
induction hx using span_induction with
| zero => simp
| add u v hu hv hu' hv' => simpa only [add_lie] using add_mem hu' hv'
| smul t u hu hu' => simpa only [smul_lie] using smul_mem _ t hu'
| mem u hu =>
induction hy using span_induction with
| zero => simp
| add u v hu hv hu' hv' => simpa only [lie_add] using add_mem hu' hv'
| smul t u hv hv' => simpa only [lie_smul] using smul_mem _ t hv'
| mem v hv =>
simp only [mem_insert_iff, mem_singleton_iff] at hu hv
rcases hu with rfl | rfl | rfl <;> rcases hv with rfl | rfl | rfl <;> (try simp only [lie_self, zero_mem])
· rw [t.lie_e_f]
apply subset_span
simp
· rw [← lie_skew, t.lie_h_e_nsmul, neg_mem_iff]
apply nsmul_mem <| subset_span _
simp
· rw [← lie_skew, t.lie_e_f, neg_mem_iff]
apply subset_span
simp
· rw [← lie_skew, t.lie_h_f_nsmul, neg_neg]
apply nsmul_mem <| subset_span _
simp
· rw [t.lie_h_e_nsmul]
apply nsmul_mem <| subset_span _
simp
· rw [t.lie_h_f_nsmul, neg_mem_iff]
apply nsmul_mem <| subset_span _
simp
