The constant term of an exterior algebra element

Mathlib's ExteriorAlgebra.algebraMapInv : ExteriorAlgebra R M →ₐ[R] R is the algebra homomorphism killing every generator; it reads off the degree-zero component, the left inverse of algebraMap. This file records how it interacts with the operations that the exterior algebra inherits from being the Clifford algebra of the zero form: the grade involution and reversion preserve the constant term, and contracting from the left or from the right against a linear functional produces the same constant term.

These are the facts that make the scalar part of a Clifford algebra, read through CliffordAlgebra.equivExterior, invariant under the grade involution and reversion, and cyclic.

Main results

• ExteriorAlgebra.algebraMapInv_ι: generators have constant term zero.
• ExteriorAlgebra.algebraMapInv_involute and ExteriorAlgebra.algebraMapInv_reverse: the grade involution and reversion preserve the constant term.
• ExteriorAlgebra.algebraMapInv_contractRight: left and right contraction against the same functional have the same constant term.
• Module.Basis.exteriorAlgebra_repr_empty: the constant term is the coordinate at the empty index set in the basis Module.Basis.ExteriorAlgebra attached to any basis of M.

@[simp]

theorem ExteriorAlgebra.algebraMapInv_ι {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (m : M) : algebraMapInv ((ι R) m) = 0

A generator of the exterior algebra has constant term zero.

@[simp]

theorem ExteriorAlgebra.algebraMapInv_involute {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (x : ExteriorAlgebra R M) : algebraMapInv (CliffordAlgebra.involute x) = algebraMapInv x

The grade involution preserves the constant term.

@[simp]

theorem ExteriorAlgebra.algebraMapInv_reverse {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (x : ExteriorAlgebra R M) : algebraMapInv (CliffordAlgebra.reverse x) = algebraMapInv x

Reversion preserves the constant term.

theorem ExteriorAlgebra.algebraMapInv_contractRight {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (d : Module.Dual R M) (x : ExteriorAlgebra R M) : algebraMapInv ((CliffordAlgebra.contractRight x) d) = algebraMapInv ((CliffordAlgebra.contractLeft d) x)

Contracting from the right or from the left against the same functional d gives the same constant term: both are d evaluated on the degree-one component.

@[simp]

theorem Module.Basis.exteriorAlgebra_repr_empty {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {I : Type u_1} [LinearOrder I] (b : Basis I R M) (x : _root_.ExteriorAlgebra R M) : (b.ExteriorAlgebra.repr x) ∅ = ExteriorAlgebra.algebraMapInv x

The constant term is the coordinate at the empty index set in the exterior-algebra basis attached to any basis b of M: every other basis vector is a product of at least one generator, so has constant term zero.