Documentation

TauCeti.Algebra.Lie.GeneralLinear.Clifford

The quadratic Clifford lift of the general linear Lie algebra #

The adjoint action of gl n K preserves its trace form. Adding the central character (card n / 2) trace to its quadratic realization gives the normal-ordered quadratic lift in the corresponding Clifford algebra.

Main results #

References #

source
noncomputable def TauCeti.glCliffordHom {K : Type u_1} {n : Type u_2} [Field K] [Fintype n] [Invertible 2] :
Matrix n n K →ₗ⁅K⁆ CliffordAlgebra (traceQuadraticForm K n)

The normal-ordered quadratic Clifford lift of the general linear Lie algebra.

Equations
Instances For
    source
    theorem TauCeti.glCliffordHom_apply {K : Type u_1} {n : Type u_2} [Field K] [Fintype n] [Invertible 2] (X : Matrix n n K) :
    glCliffordHom X = (CliffordAlgebra.quadraticLift (traceQuadraticForm K n) ⋯ (traceAdjointSO K n)) X + (algebraMap K (CliffordAlgebra (traceQuadraticForm K n))) (↑(Fintype.card n) / 2 * X.trace)

    The normal-ordered lift is the sum of the quadratic lift and its scalar trace correction.

    source
    @[simp]
    theorem TauCeti.glCliffordHom_one {K : Type u_1} {n : Type u_2} [Field K] [Fintype n] [Invertible 2] :
    glCliffordHom 1 = (algebraMap K (CliffordAlgebra (traceQuadraticForm K n))) (↑(Fintype.card n) ^ 2 / 2)

    The normal-ordered lift sends the identity matrix to the scalar (Fintype.card n : K) ^ 2 / 2.

    source
    @[simp]
    theorem TauCeti.glCliffordHom_lie_ι {K : Type u_1} {n : Type u_2} [Field K] [Fintype n] [Invertible 2] (X Y : Matrix n n K) :
    ⁅glCliffordHom X, (CliffordAlgebra.ι (traceQuadraticForm K n)) Y⁆ = (CliffordAlgebra.ι (traceQuadraticForm K n)) ⁅X, Y⁆

    The normal-ordered lift acts on Clifford generators by the matrix commutator.

    source
    theorem TauCeti.glCliffordHom_normalOrdering {K : Type u_1} {n : Type u_2} [Field K] [Fintype n] [Invertible 2] (i j : n) :
    glCliffordHom (Matrix.single i j 1) = 2⁻¹ • ∑ k : n, CliffordAlgebra.bivector (traceQuadraticForm K n) (Matrix.single i k 1) (Matrix.single k j 1) + (algebraMap K (CliffordAlgebra (traceQuadraticForm K n))) (if i = j then ↑(Fintype.card n) / 2 else 0)

    The matrix-unit lift is its antisymmetrized quadratic part plus the central normal-ordering constant.

    source
    @[simp]
    theorem TauCeti.glCliffordHom_single {K : Type u_1} {n : Type u_2} [Field K] [Fintype n] [Invertible 2] [decEq : DecidableEq n] (i j : n) :
    glCliffordHom (Matrix.single i j 1) = 2⁻¹ • ∑ k : n, carGenerator i k * carGenerator k j

    On a matrix unit, the lift is the normal-ordered quadratic sum Eᵢⱼ ↦ 1/2 ∑ₖ dᵢₖ dₖⱼ, expressed using the canonical carGenerator API.

    source
    theorem TauCeti.glCliffordHom_single_lie_carGenerator {K : Type u_1} {n : Type u_2} [Field K] [Fintype n] [Invertible 2] (i j a b : n) :
    ⁅glCliffordHom (Matrix.single i j 1), carGenerator a b⁆ = (if j = a then carGenerator i b else 0) - if b = i then carGenerator a j else 0

    The matrix-unit Clifford lift acts on the canonical matrix-unit generators by the defining matrix-unit commutator.

    Injectivity #

    source
    theorem TauCeti.glCliffordHom_injective {K : Type u_1} {n : Type u_2} [Field K] [Fintype n] [Invertible 2] (h : ↑(Fintype.card n) ≠ 0) :
    Function.Injective ⇑glCliffordHom

    The normal-ordered lift is injective as soon as Fintype.card n is invertible in K. The adjoint action of gl n K is not faithful — its kernel is the centre, the scalar matrices (TauCeti.ker_traceAdjointSO) — so the quadratic part alone is not injective; this is the reductive-not-semisimple behaviour that distinguishes gl n K from a Killing-semisimple Lie algebra, where CliffordAlgebra.adjointCliffordHom_injective needs no hypothesis. It is the normal-ordering constant that repairs it: on the scalar matrix r • 1 the lift is the scalar (card n) ^ 2 * r / 2, nonzero exactly when r is. The hypothesis is not removable, since in characteristic dividing card n those scalar matrices are again killed.