Coordinate projections on an exterior algebra

Left multiplication by a basis vector after contraction by its dual coordinate is the projection onto the exterior basis vectors containing that coordinate. This is the occupation-number projection used by both scalar detection in Clifford algebras and the matrix-unit construction from creation and annihilation operators.

Each of the two halves acts on an exterior basis vector by a single coordinate move, up to the shuffle sign that carries the moved coordinate to the front: contraction erases the coordinate from the index set, and left multiplication inserts it, each vanishing when the index set is on the wrong side of that move. Creation after contraction at distinct coordinates therefore replaces an occupied coordinate with an unoccupied one, with the product of their shuffle signs.

The grade involution is diagonal for the exterior basis as well: it multiplies an exterior monomial, and so the basis vector indexed by s, by the parity of its degree.

The basis vectors of index sets with one or two elements are the corresponding products of the exterior-algebra generators, in increasing order.

@[simp]

theorem TauCeti.ExteriorAlgebra.involute_ιMulti {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (v : Fin n → M) : CliffordAlgebra.involute ((ExteriorAlgebra.ιMulti R n) v) = (-1) ^ n • (ExteriorAlgebra.ιMulti R n) v

The grade involution acts on an exterior monomial by the parity of its degree. The monomial is the product of its n generators, each of which the involution negates.

@[simp]

theorem TauCeti.ExteriorAlgebra.involute_basis {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {I : Type w} [LinearOrder I] (b : Module.Basis I R M) (s : Finset I) : CliffordAlgebra.involute (b.ExteriorAlgebra s) = (-1) ^ s.card • b.ExteriorAlgebra s

The grade involution acts on an exterior-basis vector by the parity of its index set. The basis vector indexed by s is the monomial on s.card generators.

def TauCeti.ExteriorAlgebra.basisEraseSign {I : Type w} [LinearOrder I] (i : I) (s : Finset I) : ℤˣ

The shuffle sign for the singleton basis vector indexed by i followed by the basis vector indexed by s.erase i. When i ∈ s, this is the sign of moving i to the front of s.

Equations

• TauCeti.ExteriorAlgebra.basisEraseSign i s = Equiv.Perm.sign (Set.powersetCard.permOfDisjoint ⋯)

@[simp]

theorem TauCeti.ExteriorAlgebra.basis_singleton {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {I : Type w} [LinearOrder I] (b : Module.Basis I R M) (i : I) : b.ExteriorAlgebra {i} = (ExteriorAlgebra.ι R) (b i)

The exterior-basis vector indexed by a singleton is the image of the corresponding basis vector under the exterior-algebra generator.

theorem TauCeti.ExteriorAlgebra.basis_pair {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {I : Type w} [LinearOrder I] (b : Module.Basis I R M) {i j : I} (hij : i < j) : b.ExteriorAlgebra {i, j} = (ExteriorAlgebra.ι R) (b i) * (ExteriorAlgebra.ι R) (b j)

The exterior-basis vector indexed by a pair {i, j} with i < j is the product of the two basis vectors in increasing order.

theorem TauCeti.ExteriorAlgebra.basis_singleton_mul_basis_erase {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {I : Type w} [LinearOrder I] (b : Module.Basis I R M) (i : I) (s : Finset I) (hi : i ∈ s) : b.ExteriorAlgebra {i} * b.ExteriorAlgebra (s.erase i) = basisEraseSign i s • b.ExteriorAlgebra s

Multiplying the basis vector for i by the basis vector for s.erase i reconstructs the basis vector for s, with the shuffle sign that moves i to the front.

@[simp]

theorem TauCeti.ExteriorAlgebra.ι_mul_basis {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {I : Type w} [LinearOrder I] (b : Module.Basis I R M) (i : I) (s : Finset I) : (ExteriorAlgebra.ι R) (b i) * b.ExteriorAlgebra s = if i ∈ s then 0 else basisEraseSign i (insert i s) • b.ExteriorAlgebra (insert i s)

Creating a basis coordinate inserts it into the index set, with the shuffle sign that moves it to the front; it is zero when the coordinate is already present, since a repeated generator squares to zero.

@[simp]

theorem TauCeti.ExteriorAlgebra.contractLeft_coord_basis {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {I : Type w} [LinearOrder I] (b : Module.Basis I R M) (i : I) (s : Finset I) : (CliffordAlgebra.contractLeft (b.coord i)) (b.ExteriorAlgebra s) = if i ∈ s then basisEraseSign i s • b.ExteriorAlgebra (s.erase i) else 0

Contracting an exterior-basis vector erases the contracted coordinate, with the shuffle sign that moves that coordinate to the front; it is zero when the coordinate is absent.

theorem TauCeti.ExteriorAlgebra.ι_mul_contractLeft_coord_basis_of_not_mem_of_mem {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {I : Type w} [LinearOrder I] (b : Module.Basis I R M) (i j : I) (s : Finset I) (hi : i ∉ s) (hj : j ∈ s) : (ExteriorAlgebra.ι R) (b i) * (CliffordAlgebra.contractLeft (b.coord j)) (b.ExteriorAlgebra s) = (basisEraseSign j s * basisEraseSign i (insert i (s.erase j))) • b.ExteriorAlgebra (insert i (s.erase j))

Creating an unoccupied coordinate after contracting an occupied one replaces that coordinate in an exterior-basis vector, with the product of the two shuffle signs.

theorem TauCeti.ExteriorAlgebra.ι_mul_contractLeft_coord_basis {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {I : Type w} [LinearOrder I] (b : Module.Basis I R M) (i : I) (s : Finset I) : (ExteriorAlgebra.ι R) (b i) * (CliffordAlgebra.contractLeft (b.coord i)) (b.ExteriorAlgebra s) = if i ∈ s then b.ExteriorAlgebra s else 0

Creation after contraction by a basis coordinate is the projection onto exterior basis vectors containing that coordinate.

This is not a simp lemma because contractLeft_coord_basis is the canonical normal form for the contraction in its left-hand side.