The positive simple-root span in the type-D Serre presentation

This file packages the Lie subalgebra generated by the positive simple-root vectors of the type-D Serre presentation. Its universal property turns generatorwise containment into containment of the full Lie span, and in any representation it promotes generatorwise annihilation of a vector to annihilation by that span.

Main results

• TauCeti.TypeDStd.positiveSimpleRootLieSpan_le_iff characterizes containment of the span.
• TauCeti.TypeDStd.positiveSimpleRootLieSpan_le_lieAnnihilator applies that characterization to an arbitrary Lie module.

noncomputable def TauCeti.TypeDStd.positiveSimpleRootLieSpan (n : ℕ) : LieSubalgebra ℚ (Matrix.ToLieAlgebra ℚ (CartanMatrix.D n))

The Lie subalgebra generated by the positive simple-root vectors in the type-D Serre presentation.

Equations

• TauCeti.TypeDStd.positiveSimpleRootLieSpan n = LieSubalgebra.lieSpan ℚ (Matrix.ToLieAlgebra ℚ (CartanMatrix.D n)) (Set.range fun (i : Fin n) => TauCeti.serreE ℚ (CartanMatrix.D n) i)

@[simp]

theorem TauCeti.TypeDStd.serreE_mem_positiveSimpleRootLieSpan (n : ℕ) (i : Fin n) : serreE ℚ (CartanMatrix.D n) i ∈ positiveSimpleRootLieSpan n

Every positive simple-root vector belongs to their generated Lie subalgebra.

theorem TauCeti.TypeDStd.positiveSimpleRootLieSpan_le_iff (n : ℕ) (S : LieSubalgebra ℚ (Matrix.ToLieAlgebra ℚ (CartanMatrix.D n))) : positiveSimpleRootLieSpan n ≤ S ↔ ∀ (i : Fin n), serreE ℚ (CartanMatrix.D n) i ∈ S

The positive simple-root span is contained in a Lie subalgebra exactly when every positive simple generator belongs to it.

theorem TauCeti.TypeDStd.positiveSimpleRootLieSpan_le_lieAnnihilator (n : ℕ) {M : Type u} [AddCommGroup M] [Module ℚ M] [LieRingModule (Matrix.ToLieAlgebra ℚ (CartanMatrix.D n)) M] [LieModule ℚ (Matrix.ToLieAlgebra ℚ (CartanMatrix.D n)) M] (v : M) (hv : ∀ (i : Fin n), ⁅serreE ℚ (CartanMatrix.D n) i, v⁆ = 0) : positiveSimpleRootLieSpan n ≤ lieAnnihilator ℚ (Matrix.ToLieAlgebra ℚ (CartanMatrix.D n)) v

In any representation of the type-D Serre presentation, a vector annihilated by every positive simple-root vector is annihilated by their Lie span.