The trace form of gl n R and the anticommutation relations it induces

The general linear Lie algebra gl n R is Matrix n n R with the commutator bracket. Over a field of characteristic zero, and for nonempty finite n, it is reductive rather than semisimple (in characteristic p it need not even be that: for n of cardinality 2 in characteristic 2, sl n is a solvable ideal strictly larger than the centre). Whatever the characteristic, and again for nonempty n over a nontrivial ring, its Killing form is degenerate: the identity matrix is central and nonzero, so it lies in the radical of every invariant form built from the adjoint representation. The form that replaces it is the trace form of the standard representation, ⟨X, Y⟩ = trace (X * Y).

That motivation is what singles the form out; none of the hypotheses behind it are needed to build it. The trace form is symmetric and nondegenerate over an arbitrary commutative semiring and an arbitrary finite index type, and invariant for the commutator bracket as soon as R is a commutative ring.

This file builds that form, both as a bilinear form (TauCeti.traceBilinForm) and as the quadratic form X ↦ trace (X * X) (TauCeti.traceQuadraticForm), whose Clifford algebra is the one carrying the anticommutation relations below, and records the three facts a Clifford construction consumes: the polar form is 2 • ⟨·, ·⟩, the form is nondegenerate once 2 is invertible, and the adjoint action lands in the skew-adjoint endomorphisms of the polar form.

The factors of two are then pinned once and for all on the matrix units. Writing d_ij for ι (Eᵢⱼ), the Clifford relation ι v * ι v = Q v polarizes to the anticommutation relations d_ij d_kl + d_kl d_ij = 2 δ_jk δ_li, d_ij d_ij = δ_ij. These are relations in the Clifford algebra of the trace form, and nothing beyond that is claimed of them here. Reading them, as the roadmap does, as the relations of a CAR algebra would need a splitting of the generators into creation and annihilation operators, an involution, and an identification of this Clifford algebra with a CAR algebra; none of that is supplied.

Main definitions

• TauCeti.traceBilinForm R n: the bilinear form (X, Y) ↦ trace (X * Y) on Matrix n n R.
• TauCeti.traceQuadraticForm R n: the quadratic form X ↦ trace (X * X), the form whose Clifford algebra carries the anticommutation relations below.
• TauCeti.traceAdjointSO R n: the adjoint homomorphism of gl n R read into the skew-adjoint endomorphisms of the polar form of TauCeti.traceQuadraticForm R n.

Main results

• TauCeti.traceBilinForm_lieInvariant: the trace form is invariant, by cyclicity of the trace.
• TauCeti.traceBilinForm_nondegenerate: it is nondegenerate over any commutative semiring, a matrix being determined by the traces of its products.
• TauCeti.polarBilin_traceQuadraticForm: the polar form of the trace quadratic form is 2 * trace (X * Y), the normalization the roadmap pins; TauCeti.polarBilin_traceQuadraticForm_eq_two_smul is the same statement as an equality of bilinear forms, 2 • traceBilinForm.
• TauCeti.traceQuadraticForm_nondegenerate: the quadratic form is nondegenerate when 2 is invertible.
• TauCeti.traceQuadraticForm_ι_mul_ι_add_swap: the anticommutation relation ι X ι Y + ι Y ι X = 2 trace (X * Y) for arbitrary generators, of which TauCeti.traceQuadraticForm_ι_single_mul_ι_single_add_swap, the anticommutation relations d_ij d_kl + d_kl d_ij = 2 δ_jk δ_li on the matrix units, is the specialization; and TauCeti.traceQuadraticForm_ι_single_mul_self: the squares d_ij d_ij = δ_ij.
• TauCeti.carGenerator: the opaque public matrix-unit generator used by the CAR consumers, together with its generator-level anticommutation and square equations.

Implementation notes

The roadmap pins these declarations over ℂ for Matrix (Fin N) (Fin N) ℂ. Nothing in the statements or proofs asks for that: the form, its symmetry and its nondegeneracy are stated over an arbitrary commutative semiring and an arbitrary finite index type, exactly as for the Killing form in TauCeti/Algebra/Lie/SkewAdjoint.lean. Additive inverses are assumed only where the construction being made needs them: the commutator bracket, QuadraticMap.polarBilin and CliffordAlgebra are all available only over a CommRing, so the invariance, polar-form, adjoint and anticommutation declarations carry [CommRing R]. Only the transfer of nondegeneracy from the bilinear form to the quadratic form asks for an invertible 2, carried as an Invertible hypothesis on the single result that needs it.

Mathlib's Algebra.traceForm R S is the trace form of the regular representation of an algebra, which on Matrix n n R is Fintype.card n times the form built here, so it is not a reparametrization of it; and LieModule.traceForm, which does specialize to this form on the standard representation, is unavailable without the non-instance LieRingModule.ofAssociativeModule. The form is therefore assembled directly from Matrix.traceLinearMap and LinearMap.mul.

The two steps that the trace form shares with the Killing form — the polar form of the quadratic form of a symmetric B is 2 • B, and nondegeneracy passes from B to that quadratic form once 2 is invertible — are general facts about a bilinear form, stated once in TauCeti/LinearAlgebra/QuadraticForm/Radical.lean (LinearMap.BilinMap.polarBilin_toQuadraticMap_of_flip and LinearMap.BilinForm.Nondegenerate.toQuadraticMap); the declarations here and their Killing counterparts in TauCeti/Algebra/Lie/SkewAdjoint.lean are applications of them.

Mathlib does not register LieRing.ofAssociativeRing as a global instance, so, as in Mathlib/Algebra/Lie/Matrix.lean, it is a local instance here.

References

This is the opening of the gl_N worked instance ("the CAR algebra") of Layer 9 of TauCetiRoadmap/RepresentationTheory/SpinRepresentations/README.md: "its form is the trace form Q X = tr (X²) (nondegenerate where the Killing form is not) ... the generators d_ab = ι (E_ab) satisfy the CAR relations d_ab d_cd + d_cd d_ab = 2 δ_bc δ_ad (pinned as the polar-form equation)", together with the trace-form instance of the layer's adjoint homomorphism ad : 𝔤 →ₗ⁅K⁆ 𝔰𝔬(𝔤, B).

def TauCeti.traceBilinForm (R : Type u_1) (n : Type u_2) [Fintype n] [CommSemiring R] : LinearMap.BilinForm R (Matrix n n R)

The trace form of gl n R, (X, Y) ↦ trace (X * Y): the trace form of the standard representation, which is nondegenerate where the Killing form of gl n R is not.

Equations

• TauCeti.traceBilinForm R n = (LinearMap.mul R (Matrix n n R)).compr₂ (Matrix.traceLinearMap n R R)

@[simp]

theorem TauCeti.traceBilinForm_apply {R : Type u_1} {n : Type u_2} [Fintype n] [CommSemiring R] (X Y : Matrix n n R) : ((traceBilinForm R n) X) Y = (X * Y).trace

@[simp]

theorem TauCeti.traceBilinForm_flip (R : Type u_1) (n : Type u_2) [Fintype n] [CommSemiring R] : LinearMap.flip (traceBilinForm R n) = traceBilinForm R n

The trace form is its own flip, by cyclicity of the trace.

theorem TauCeti.traceBilinForm_isSymm (R : Type u_1) (n : Type u_2) [Fintype n] [CommSemiring R] : (traceBilinForm R n).IsSymm

The trace form is symmetric, the predicate form of TauCeti.traceBilinForm_flip.

theorem TauCeti.traceBilinForm_nondegenerate (R : Type u_1) (n : Type u_2) [Fintype n] [CommSemiring R] : (traceBilinForm R n).Nondegenerate

The trace form is nondegenerate, over any commutative semiring and any finite index type: a matrix is determined by the traces of its products.

@[simp]

theorem TauCeti.traceBilinForm_single_single {R : Type u_1} {n : Type u_2} [Fintype n] [CommSemiring R] [DecidableEq n] (i j k l : n) (a b : R) : ((traceBilinForm R n) (Matrix.single i j a)) (Matrix.single k l b) = if j = k ∧ l = i then a * b else 0

The trace form pairs the matrix units perfectly: ⟨Eᵢⱼ a, E_kl b⟩ = δ_jk δ_li a b. This is the δ bookkeeping that the anticommutation relations inherit.

theorem TauCeti.traceBilinForm_lieInvariant (R : Type u_1) (n : Type u_2) [Fintype n] [CommRing R] [DecidableEq n] : LinearMap.BilinForm.lieInvariant (Matrix n n R) (traceBilinForm R n)

The trace form is invariant: trace (⁅X, Y⁆ * Z) = -trace (Y * ⁅X, Z⁆), which is cyclicity of the trace after expanding both brackets. Invariance is what makes the adjoint action skew-adjoint for the form, hence what produces TauCeti.traceAdjointSO.

def TauCeti.traceQuadraticForm (R : Type u_1) (n : Type u_2) [Fintype n] [CommSemiring R] : QuadraticForm R (Matrix n n R)

The trace quadratic form of gl n R, X ↦ trace (X * X). Its Clifford algebra is the one whose generators satisfy the anticommutation relations TauCeti.traceQuadraticForm_ι_single_mul_ι_single_add_swap.

Equations

• TauCeti.traceQuadraticForm R n = LinearMap.BilinMap.toQuadraticMap (TauCeti.traceBilinForm R n)

@[simp]

theorem TauCeti.traceQuadraticForm_apply {R : Type u_1} {n : Type u_2} [Fintype n] [CommSemiring R] (X : Matrix n n R) : (traceQuadraticForm R n) X = (X * X).trace

The trace quadratic form evaluates at X to trace (X * X). This is the equation the roadmap pins TauCeti.traceQuadraticForm by.

@[simp]

theorem TauCeti.polarBilin_traceQuadraticForm_eq_two_smul (R : Type u_1) (n : Type u_2) [Fintype n] [CommRing R] : QuadraticMap.polarBilin (traceQuadraticForm R n) = 2 • traceBilinForm R n

The polar form of the trace quadratic form is 2 • ⟨·, ·⟩, the trace form being symmetric. Every factor of two in the anticommutation relations comes from this one equation.

theorem TauCeti.polarBilin_traceQuadraticForm {R : Type u_1} {n : Type u_2} [Fintype n] [CommRing R] (X Y : Matrix n n R) : ((QuadraticMap.polarBilin (traceQuadraticForm R n)) X) Y = 2 * (X * Y).trace

The polar form of the trace quadratic form, read pointwise: 2 * trace (X * Y). This is the normalization the roadmap pins, and the equation from which the anticommutation relations follow; TauCeti.polarBilin_traceQuadraticForm_eq_two_smul is the same statement for the forms themselves.

theorem TauCeti.traceQuadraticForm_nondegenerate (R : Type u_1) (n : Type u_2) [Fintype n] [CommRing R] [Invertible 2] : QuadraticMap.Nondegenerate

The trace quadratic form is nondegenerate over a ring in which 2 is invertible. What TauCeti.traceBilinForm_nondegenerate controls is the trace form B itself; 2 must be invertible both to transfer nondegeneracy from B to the polar form 2 • B and to pass from the polar form back to the quadratic form, a quadratic form being a finer invariant than its polar form.

def TauCeti.traceAdjointSO (R : Type u_1) (n : Type u_2) [Fintype n] [CommRing R] [DecidableEq n] : Matrix n n R →ₗ⁅R⁆ ↥(skewAdjointLieSubalgebra (QuadraticMap.polarBilin (traceQuadraticForm R n)))

The adjoint homomorphism of gl n R for the trace form: ad : gl n R →ₗ⁅R⁆ 𝔰𝔬(gl n R, Q), the trace-form instance of TauCeti.LieAlgebra.adjointSO. Composing it with the quadratic realization inside the Clifford algebra of TauCeti.traceQuadraticForm R n would give the adjoint quadratic lift; that composite is not built here.

Equations

• TauCeti.traceAdjointSO R n = TauCeti.LieAlgebra.adjointSO (TauCeti.traceBilinForm R n) ⋯

@[simp]

theorem TauCeti.coe_traceAdjointSO {R : Type u_1} {n : Type u_2} [Fintype n] [CommRing R] [DecidableEq n] (X : Matrix n n R) : ↑((traceAdjointSO R n) X) = (LieAlgebra.ad R (Matrix n n R)) X

The trace-form adjoint homomorphism is ad with its codomain restricted.

@[simp]

theorem TauCeti.ker_traceAdjointSO (R : Type u_1) (n : Type u_2) [Fintype n] [CommRing R] [DecidableEq n] : (traceAdjointSO R n).ker = LieAlgebra.center R (Matrix n n R)

The kernel of the trace-form adjoint homomorphism is the centre of gl n R, which for nonempty n over a nontrivial ring is nonzero: the map is not injective, and the adjoint representation of gl n R is therefore unfaithful — the reason the form here is the trace form of the standard representation and not the Killing form. Over a field of characteristic zero that failure is the reductive-not-semisimple behaviour of gl n R.

theorem TauCeti.traceQuadraticForm_ι_mul_ι_add_swap {R : Type u_1} {n : Type u_2} [Fintype n] [CommRing R] (X Y : Matrix n n R) : (CliffordAlgebra.ι (traceQuadraticForm R n)) X * (CliffordAlgebra.ι (traceQuadraticForm R n)) Y + (CliffordAlgebra.ι (traceQuadraticForm R n)) Y * (CliffordAlgebra.ι (traceQuadraticForm R n)) X = (algebraMap R (CliffordAlgebra (traceQuadraticForm R n))) (2 * (X * Y).trace)

The anticommutation relation in the Clifford algebra of the trace form: any two generators anticommute up to 2 trace (X * Y), the polar-form normalization.

theorem TauCeti.traceQuadraticForm_ι_single_mul_ι_single_add_swap {R : Type u_1} {n : Type u_2} [Fintype n] [CommRing R] [DecidableEq n] (i j k l : n) (a b : R) : (CliffordAlgebra.ι (traceQuadraticForm R n)) (Matrix.single i j a) * (CliffordAlgebra.ι (traceQuadraticForm R n)) (Matrix.single k l b) + (CliffordAlgebra.ι (traceQuadraticForm R n)) (Matrix.single k l b) * (CliffordAlgebra.ι (traceQuadraticForm R n)) (Matrix.single i j a) = (algebraMap R (CliffordAlgebra (traceQuadraticForm R n))) (if j = k ∧ l = i then 2 * (a * b) else 0)

The anticommutation relations of the matrix-unit generators: writing d_ij for ι (Eᵢⱼ) in the Clifford algebra of the trace quadratic form, d_ij d_kl + d_kl d_ij = 2 δ_jk δ_li, the matrix units being paired by the trace form exactly when j = k and l = i.

@[simp]

theorem TauCeti.traceQuadraticForm_ι_single_mul_self {R : Type u_1} {n : Type u_2} [Fintype n] [CommRing R] [DecidableEq n] (i j : n) (a : R) : (CliffordAlgebra.ι (traceQuadraticForm R n)) (Matrix.single i j a) * (CliffordAlgebra.ι (traceQuadraticForm R n)) (Matrix.single i j a) = (algebraMap R (CliffordAlgebra (traceQuadraticForm R n))) (if i = j then a * a else 0)

The squares of the matrix-unit generators: d_ij d_ij = δ_ij, so the off-diagonal units square to zero in the Clifford algebra and the diagonal ones square to a scalar.

theorem TauCeti.traceQuadraticForm_ι_single_mul_ι_single_comm_of_not_paired {R : Type u_1} {n : Type u_2} [Fintype n] [CommRing R] [DecidableEq n] (i j k l : n) (a b : R) (h : ¬(j = k ∧ l = i)) : (CliffordAlgebra.ι (traceQuadraticForm R n)) (Matrix.single i j a) * (CliffordAlgebra.ι (traceQuadraticForm R n)) (Matrix.single k l b) = -((CliffordAlgebra.ι (traceQuadraticForm R n)) (Matrix.single k l b) * (CliffordAlgebra.ι (traceQuadraticForm R n)) (Matrix.single i j a))

Two matrix-unit generators anticommute whenever they are not paired by the trace form: the δ_jk δ_li of TauCeti.traceQuadraticForm_ι_single_mul_ι_single_add_swap vanishes.

Matrix-unit Clifford generators

noncomputable def TauCeti.carGenerator {K : Type u_3} [CommRing K] {m : Type u_4} [Fintype m] (i j : m) : CliffordAlgebra (traceQuadraticForm K m)

The Clifford generator associated to the matrix unit Eᵢⱼ.

This is the common CAR generator used by the highest-weight, occupation, Casimir, and weight multiplicity calculations.

Equations

• TauCeti.carGenerator i j = (CliffordAlgebra.ι (TauCeti.traceQuadraticForm K m)) (Matrix.single i j 1)

theorem TauCeti.carGenerator_def {K : Type u_3} [CommRing K] {m : Type u_4} [Fintype m] (i j : m) : carGenerator i j = (CliffordAlgebra.ι (traceQuadraticForm K m)) (Matrix.single i j 1)

The matrix-unit formula for carGenerator.

@[simp]

theorem TauCeti.carGenerator_mul_add_swap {K : Type u_3} [CommRing K] {m : Type u_4} [Fintype m] (i j k l : m) : carGenerator i j * carGenerator k l + carGenerator k l * carGenerator i j = (algebraMap K (CliffordAlgebra (traceQuadraticForm K m))) (if j = k ∧ l = i then 2 else 0)

The matrix-unit generators satisfy the CAR anticommutation relation.

@[simp]

theorem TauCeti.carGenerator_mul_self {K : Type u_3} [CommRing K] {m : Type u_4} [Fintype m] (i j : m) : carGenerator i j * carGenerator i j = (algebraMap K (CliffordAlgebra (traceQuadraticForm K m))) (if i = j then 1 else 0)

The square of a matrix-unit generator is zero off the diagonal and scalar on the diagonal.

theorem TauCeti.carGenerator_mul_comm_of_not_paired {K : Type u_3} [CommRing K] {m : Type u_4} [Fintype m] (i j k l : m) (h : ¬(j = k ∧ l = i)) : carGenerator i j * carGenerator k l = -(carGenerator k l * carGenerator i j)

Non-paired matrix-unit generators anticommute.