Documentation

TauCeti.Algebra.Lie.GeneralLinear.CAR.Occupation

Occupation elements in the CAR algebra #

For the Clifford algebra of the trace form on matrices, write dᵢⱼ = ι(Eᵢⱼ). This file studies the normalized quadratic elements

pᵢⱼ = 1/2 dᵢⱼ dⱼᵢ.

When i ≠ j, these are occupation projections for the hyperbolic plane spanned by Eᵢⱼ and Eⱼᵢ. Their two orders are orthogonal. When 2 is invertible, the CAR relations also give pᵢⱼ + pⱼᵢ = 1; in characteristic two the normalization vanishes instead, so the elements remain idempotent in every characteristic. All of the occupation elements commute with one another. Finally, the diagonal normal-ordered lift is the sum Fᵢᵢ = ∑ k, pᵢₖ; for a linearly ordered index type this can be oriented using only the positive pairs. These formulas supply the commuting off-diagonal zero-one operators used to calculate weights in the left regular CAR module.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.carOccupationElement {K : Type u_1} {n : Type u_2} [Field K] [Fintype n] (i j : n) :
CliffordAlgebra (traceQuadraticForm K n)

The occupation element for the ordered matrix-unit pair (i, j), normalized so that it is an idempotent off the diagonal. For i = j it is the scalar 1/2.

Equations
Instances For
    source
    theorem TauCeti.carOccupationElement_def {K : Type u_1} {n : Type u_2} [Field K] [Fintype n] (i j : n) :
    carOccupationElement i j = 2⁻¹ • (carGenerator i j * carGenerator j i)

    The occupation element written in terms of the canonical matrix-unit generators.

    source
    @[simp]
    theorem TauCeti.carOccupationElement_self {K : Type u_1} {n : Type u_2} [Field K] [Fintype n] (i : n) :
    carOccupationElement i i = 2⁻¹ • 1

    The diagonal occupation element is the scalar 1/2.

    source
    @[simp]
    theorem TauCeti.carOccupationElement_mul_swap {K : Type u_1} {n : Type u_2} [Field K] [Fintype n] {i j : n} (hij : i ≠ j) :
    carOccupationElement i j * carOccupationElement j i = 0

    Oppositely oriented off-diagonal occupation elements are orthogonal in this order.

    source
    @[simp]
    theorem TauCeti.carOccupationElement_add_swap {K : Type u_1} {n : Type u_2} [Field K] [Fintype n] [Invertible 2] (i j : n) :
    carOccupationElement i j + carOccupationElement j i = 1

    The two orientations of an occupation element are complementary. This also holds on the diagonal, where both terms are the scalar 1/2.

    source
    theorem TauCeti.carOccupationElement_swap {K : Type u_1} {n : Type u_2} [Field K] [Fintype n] [Invertible 2] (i j : n) :
    carOccupationElement j i = 1 - carOccupationElement i j

    Reversing an occupation element gives its complement.

    source
    theorem TauCeti.isIdempotentElem_carOccupationElement {K : Type u_1} {n : Type u_2} [Field K] [Fintype n] {i j : n} (hij : i ≠ j) :
    IsIdempotentElem (carOccupationElement i j)

    Every off-diagonal occupation element is idempotent over every field.

    source
    @[simp]
    theorem TauCeti.carOccupationElement_mul_self {K : Type u_1} {n : Type u_2} [Field K] [Fintype n] {i j : n} (hij : i ≠ j) :
    carOccupationElement i j * carOccupationElement i j = carOccupationElement i j

    Multiplication by an off-diagonal occupation element twice is multiplication by it once.

    source
    theorem TauCeti.commute_carOccupationElement {K : Type u_1} {n : Type u_2} [Field K] [Fintype n] {i j k l : n} :
    Commute (carOccupationElement i j) (carOccupationElement k l)

    All occupation elements commute, including equal and oppositely oriented pairs.

    source
    theorem TauCeti.glCliffordHom_single_self_eq_sum_occupation {K : Type u_1} {n : Type u_2} [Field K] [Fintype n] [Invertible 2] (i : n) :
    glCliffordHom (Matrix.single i i 1) = ∑ k : n, carOccupationElement i k

    A diagonal normal-ordered generator is the sum of all occupation elements with its first index fixed. The diagonal summand is the scalar 1/2.

    source
    theorem TauCeti.glCliffordHom_single_self_eq_sum_positive_occupation {K : Type u_1} {n : Type u_2} [Field K] [Fintype n] [Invertible 2] [LinearOrder n] (i : n) :
    glCliffordHom (Matrix.single i i 1) = ∑ k : n, if k < i then 1 - carOccupationElement k i else carOccupationElement i k

    Orient the diagonal lift using only positive-pair occupation projections. Below i, the opposite orientation is replaced by its complement.

    source
    theorem TauCeti.sum_glCliffordHom_single_self_eq_cut_occupation {K : Type u_1} {n : Type u_2} [Field K] [Fintype n] [Invertible 2] (s : Finset n) :
    ∑ i ∈ s, glCliffordHom (Matrix.single i i 1) = (↑s.card ^ 2 / 2) • 1 + ∑ ij ∈ s.product (Finset.univ \ s), carOccupationElement ij.1 ij.2

    Summing the diagonal normal-ordered lifts over s leaves the scalar contribution from pairs with both indices in s, together with the occupation elements whose first index lies in s and whose second index lies outside it. The scalar is |s|² / 2, including the diagonal halves.