Integral matrices of type-B spin generators

The invariant spin lattice gives an integral matrix for each numbered simple root generator. Each generator squares to zero, so its root subgroup points are 1 + u X over any commutative ring. The matrix construction and its column formulas use the generic Kostant lattice API. The carrier interface follows TauCeti.Algebra.Lie.Symplectic.StandardCarrier.IntegralMatrix.

References

C. Chevalley, The Algebraic Theory of Spinors, Chapter II.

noncomputable def TauCeti.TypeBSpinCarrier.rootIntMatrix (n : ℕ) (j : Fin (n + 1) ⊕ Fin (n + 1)) : Matrix (Fin (dimension n)) (Fin (dimension n)) ℤ

The integral matrix of a represented numbered simple root generator in the lattice basis.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.TypeBSpinCarrier.rep_rootGenerator_latticeBasis_eq_sum (n : ℕ) (j : Fin (n + 1) ⊕ Fin (n + 1)) (s : Fin (dimension n)) : ((rep n) ((UniversalEnvelopingAlgebra.ι ℚ) (typeBSimpleRootGeneratorFamily j))) ↑((latticeBasis n) s) = ∑ r : Fin (dimension n), rootIntMatrix n j r s • ↑((latticeBasis n) r)

A represented root generator acts on a lattice basis vector by its integral matrix column.

theorem TauCeti.TypeBSpinCarrier.rootIntMatrix_apply_of_eq (n : ℕ) (j : Fin (n + 1) ⊕ Fin (n + 1)) {a a' : Fin (dimension n)} {c : ℤˣ} (h : ((rep n) ((UniversalEnvelopingAlgebra.ι ℚ) (typeBSimpleRootGeneratorFamily j))) ↑((latticeBasis n) a) = c • ↑((latticeBasis n) a')) (r : Fin (dimension n)) : rootIntMatrix n j r a = if r = a' then ↑c else 0

A signed root-generator step gives the corresponding signed integral matrix column.

theorem TauCeti.TypeBSpinCarrier.coe_rootSubgroupPoints_eq_one_add_smul (n : ℕ) (j : Fin (n + 1) ⊕ Fin (n + 1)) (A : Type v) [CommRing A] (u : Multiplicative A) : ↑↑((rootSubgroupPoints n j A) u) = 1 + Multiplicative.toAdd u • (rootIntMatrix n j).map Int.cast

A numbered root subgroup point is 1 + u X for the integral matrix of its generator.