Documentation

TauCeti.Algebra.Lie.Orthogonal.TypeD.SpinCarrier.IntegralMatrix

Integral matrices of type-D spin generators #

The invariant spin lattice gives an integral matrix for each numbered simple root generator of type Dₙ. Each generator squares to zero, so its root subgroup points are 1 + u X over any commutative ring.

Each generator acts through an even Clifford element, so it preserves the exterior parity of the spin module: it maps the even half-spin summand S⁺ and the odd one S⁻ into themselves. In the lattice basis, indexed by sign sets, this says that the integral matrix vanishes at every entry joining two sign sets whose cardinalities have different parities.

Main declarations #

References #

The matrix construction and its column formula use the generic Kostant lattice API, and the carrier interface follows the type-B one in TauCeti.Algebra.Lie.Orthogonal.TypeB.SpinCarrier.IntegralMatrix.

source
noncomputable def TauCeti.TypeDSpinCarrier.rootIntMatrix (n : ℕ) (hn : 4 ≤ n) (k : Fin n ⊕ Fin n) :
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.
Instances For
    source
    theorem TauCeti.TypeDSpinCarrier.rep_rootGenerator_latticeBasis_eq_sum (n : ℕ) (hn : 4 ≤ n) (k : Fin n ⊕ Fin n) (s : Fin (dimension n)) :
    ((rep n hn) ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator (CartanMatrix.D n) k))) ↑((latticeBasis n) s) = ∑ r : Fin (dimension n), rootIntMatrix n hn k r s • ↑((latticeBasis n) r)

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

    source
    theorem TauCeti.TypeDSpinCarrier.rootIntMatrix_apply_of_eq (n : ℕ) (hn : 4 ≤ n) (j : Fin n ⊕ Fin n) {a a' : Fin (dimension n)} {c : ℤˣ} (h : ((rep n hn) ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator (CartanMatrix.D n) j))) ↑((latticeBasis n) a) = c • ↑((latticeBasis n) a')) (r : Fin (dimension n)) :
    rootIntMatrix n hn j r a = if r = a' then ↑c else 0

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

    source
    theorem TauCeti.TypeDSpinCarrier.coe_rootSubgroupPoints_eq_one_add_smul (n : ℕ) (hn : 4 ≤ n) (k : Fin n ⊕ Fin n) (A : Type v) [CommRing A] (u : Multiplicative A) :
    ↑↑((rootSubgroupPoints n hn k A) u) = 1 + Multiplicative.toAdd u • (rootIntMatrix n hn k).map Int.cast

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

    source
    theorem TauCeti.TypeDSpinCarrier.rootIntMatrix_eq_zero_of_card_ne (n : ℕ) (hn : 4 ≤ n) (k : Fin n ⊕ Fin n) {a b : Fin (dimension n)} (hab : ↑(signSet n a).card ≠ ↑(signSet n b).card) :
    rootIntMatrix n hn k a b = 0

    The integral matrix of a numbered root generator does not join the two half-spin summands: its entry vanishes whenever the two sign sets have cardinalities of different parities.