A primitive vector generates a copy of V(n)

TauCeti/Algebra/Lie/Sl2/WeightString.lean and TauCeti/Algebra/Lie/Sl2/Classification.lean classify the modules that are irreducible over an sl₂ triple and carry a primitive vector: they are the standard modules V(n). That classification says nothing about a primitive vector sitting inside a larger module. This file supplies the missing statement: over a characteristic-zero field, in any finite-dimensional module over a Lie algebra generated by an sl₂ triple, the Lie submodule generated by a primitive vector of weight n : ℕ is already irreducible, hence is a copy of V(n).

This is the rank-one case of the general principle that a highest weight vector of a finite-dimensional module generates an irreducible highest weight module, and it is what turns an explicitly exhibited primitive vector into a named summand.

The argument

The weight string m, f • m, …, fⁿ • m spans the submodule generated by m (TauCeti.lieSpan_singleton_toSubmodule_eq_span, which reuses TauCeti.weightStringSubmodule), so a vector of the submodule is a combination ∑ᵢ aᵢ fⁱ • m. Raising annihilates a string vector once it has climbed past the top,

eʲ · (fⁱ • m) = 0 for i < j (TauCeti.pow_toEnd_e_pow_toEnd_f_eq_zero),

and returns a nonzero multiple of m when it climbs exactly to the top,

eʲ · (fʲ • m) = (∏_{i < j} (i + 1)(n - i)) • m (TauCeti.pow_toEnd_e_pow_toEnd_f_self).

So applying eʲ for the largest j with aⱼ ≠ 0 kills every term but one and leaves a nonzero multiple of m. A nonzero Lie submodule of the string therefore contains m, hence contains everything m generates: the string is an atom in the lattice of Lie submodules, which is irreducibility.

Main results

• TauCeti.lieSpan_singleton_toSubmodule_eq_span: the Lie submodule generated by a primitive vector is spanned by its weight string.
• TauCeti.isAtom_lieSpan_singleton and TauCeti.isIrreducible_lieSpan_singleton: that submodule is irreducible.
• TauCeti.finrank_lieSpan_singleton: it has dimension n + 1.
• TauCeti.weightStringSubmodule_le_eigenspace_sl2Casimir and TauCeti.iSupIndep_weightStringSubmodule_of_injective, with their lieSpan readings TauCeti.lieSpan_singleton_le_eigenspace_sl2Casimir and TauCeti.iSupIndep_lieSpan_singleton_of_injective: the Casimir operator acts on that submodule by the scalar attached to the weight, so submodules generated by primitive vectors of distinct weights are independent.
• TauCeti.Sl2Std.nonempty_lieModuleEquiv_lieSpan_singleton: over sl (Fin 2) K it is a copy of V(n).

References

This supports the Clebsch-Gordan item of Layer 0 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md.

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §7.2.

The submodule generated by a primitive vector

theorem TauCeti.lieSpan_singleton_toSubmodule_eq_span {K : Type u_1} [CommRing K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {M : Type u_3} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {h e f : L} {t : IsSl2Triple h e f} {m : M} {μ : K} (htop : IsSl2Triple.toLieSubalgebra K t = ⊤) (P : t.HasPrimitiveVectorWith m μ) : ↑(LieSubmodule.lieSpan K L {m}) = Submodule.span K (Set.range fun (i : ℕ) => ((LieModule.toEnd K L M) f ^ i) m)

The Lie submodule generated by a primitive vector is spanned by its weight string. One inclusion is that each string vector is reached from m by lowering; the other is that the weight string already spans a Lie submodule, namely TauCeti.weightStringSubmodule, read for the whole algebra through TauCeti.lieSubmoduleOfEqTop.

theorem TauCeti.hasPrimitiveVectorWith_lieSpan_singleton {K : Type u_1} [CommRing K] {L : Type u_2} [LieRing L] {M : Type u_3} [AddCommGroup M] [Module K M] [LieRingModule L M] {h e f : L} {t : IsSl2Triple h e f} {m : M} {μ : K} (P : t.HasPrimitiveVectorWith m μ) (hm : m ∈ LieSubmodule.lieSpan K L {m}) : t.HasPrimitiveVectorWith ⟨m, hm⟩ μ

The primitive vector, read as a vector of the Lie submodule it generates.

Irreducibility of the generated submodule

theorem TauCeti.lieSpan_singleton_toSubmodule_eq_span_fin {K : Type u_1} [Field K] [CharZero K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {M : Type u_3} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [IsNoetherian K M] {h e f : L} {t : IsSl2Triple h e f} {m : M} {n : ℕ} (htop : IsSl2Triple.toLieSubalgebra K t = ⊤) (P : t.HasPrimitiveVectorWith m ↑n) : ↑(LieSubmodule.lieSpan K L {m}) = Submodule.span K (Set.range fun (i : Fin (n + 1)) => ((LieModule.toEnd K L M) f ^ ↑i) m)

The weight string of a primitive vector of weight n : ℕ spans the Lie submodule it generates already as a family of n + 1 vectors, the string being zero from step n + 1 on.

theorem TauCeti.isAtom_lieSpan_singleton {K : Type u_1} [Field K] [CharZero K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {M : Type u_3} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [IsNoetherian K M] {h e f : L} {t : IsSl2Triple h e f} {m : M} {n : ℕ} (htop : IsSl2Triple.toLieSubalgebra K t = ⊤) (P : t.HasPrimitiveVectorWith m ↑n) : IsAtom (LieSubmodule.lieSpan K L {m})

A primitive vector generates an irreducible submodule. For a Lie algebra generated by an sl₂ triple, the Lie submodule generated by a primitive vector of weight n : ℕ is an atom in the lattice of Lie submodules.

theorem TauCeti.isIrreducible_lieSpan_singleton {K : Type u_1} [Field K] [CharZero K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {M : Type u_3} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [IsNoetherian K M] {h e f : L} {t : IsSl2Triple h e f} {m : M} {n : ℕ} (htop : IsSl2Triple.toLieSubalgebra K t = ⊤) (P : t.HasPrimitiveVectorWith m ↑n) : LieModule.IsIrreducible K L ↥(LieSubmodule.lieSpan K L {m})

A primitive vector generates an irreducible submodule. The module-level reading of TauCeti.isAtom_lieSpan_singleton.

theorem TauCeti.finrank_lieSpan_singleton {K : Type u_1} [Field K] [CharZero K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {M : Type u_3} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [IsNoetherian K M] {h e f : L} {t : IsSl2Triple h e f} {m : M} {n : ℕ} (htop : IsSl2Triple.toLieSubalgebra K t = ⊤) (P : t.HasPrimitiveVectorWith m ↑n) : Module.finrank K ↥(LieSubmodule.lieSpan K L {m}) = n + 1

The dimension of the submodule generated by a primitive vector of weight n is n + 1, the length of its weight string.

The Casimir operator on the generated submodule

theorem TauCeti.weightStringSubmodule_le_eigenspace_sl2Casimir {K : Type u_1} [Field K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {M : Type u_3} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {h e f : L} {t : IsSl2Triple h e f} {m : M} {n : ℕ} [NeZero 2] (P : t.HasPrimitiveVectorWith m ↑n) : ↑(weightStringSubmodule P) ≤ (sl2Casimir K h e f M).eigenspace (↑n * (↑n + 2) / 2)

The Casimir operator acts by a scalar on the weight string of a primitive vector. It does so on the primitive vector by TauCeti.sl2Casimir_apply_of_hasPrimitiveVectorWith, and it commutes with the lowering operator that sweeps out the rest of the string.

theorem TauCeti.lieSpan_singleton_le_eigenspace_sl2Casimir {K : Type u_1} [Field K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {M : Type u_3} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {h e f : L} {t : IsSl2Triple h e f} {m : M} {n : ℕ} [NeZero 2] (htop : IsSl2Triple.toLieSubalgebra K t = ⊤) (P : t.HasPrimitiveVectorWith m ↑n) : ↑(LieSubmodule.lieSpan K L {m}) ≤ (sl2Casimir K h e f M).eigenspace (↑n * (↑n + 2) / 2)

The reading of TauCeti.weightStringSubmodule_le_eigenspace_sl2Casimir for the submodule generated over the whole algebra, which the weight string is when the triple generates it.

theorem TauCeti.iSupIndep_weightStringSubmodule_of_injective {K : Type u_1} [Field K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {M : Type u_3} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {h e f : L} {t : IsSl2Triple h e f} [CharZero K] {ι : Type u_4} {v : ι → M} {p : ι → ℕ} (P : ∀ (i : ι), t.HasPrimitiveVectorWith (v i) ↑(p i)) (hp : Function.Injective p) : iSupIndep fun (i : ι) => ↑(weightStringSubmodule ⋯)

Primitive vectors of distinct weights have independent weight strings. The Casimir operator separates them: it acts on the weight string of a primitive vector of weight n by n(n + 2)/2, and those scalars are distinct for distinct weights, so the strings lie in distinct eigenspaces of a single endomorphism.

theorem TauCeti.iSupIndep_lieSpan_singleton_of_injective {K : Type u_1} [Field K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {M : Type u_3} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {h e f : L} {t : IsSl2Triple h e f} [CharZero K] {ι : Type u_4} (htop : IsSl2Triple.toLieSubalgebra K t = ⊤) {v : ι → M} {p : ι → ℕ} (P : ∀ (i : ι), t.HasPrimitiveVectorWith (v i) ↑(p i)) (hp : Function.Injective p) : iSupIndep fun (i : ι) => ↑(LieSubmodule.lieSpan K L {v i})

The reading of TauCeti.iSupIndep_weightStringSubmodule_of_injective for the submodules generated over the whole algebra, which the weight strings are when the triple generates it.

The generated submodule as a copy of V(n)

theorem TauCeti.Sl2Std.nonempty_lieModuleEquiv_lieSpan_singleton {K : Type u_1} [Field K] [CharZero K] {M : Type u_2} [AddCommGroup M] [Module K M] [LieRingModule (↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) M] [LieModule K (↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) M] [IsNoetherian K M] {m : M} {n : ℕ} (P : ⋯.HasPrimitiveVectorWith m ↑n) : Nonempty (↥(LieSubmodule.lieSpan K ↥(LieAlgebra.SpecialLinear.sl (Fin 2) K) {m}) ≃ₗ⁅K,↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)⁆ Sl2Std K n)

A primitive vector of sl (Fin 2) K generates a copy of V(n). The Lie submodule generated by a primitive vector of weight n is irreducible by TauCeti.isIrreducible_lieSpan_singleton, so the classification identifies it with the standard module.