Freeness and dimension of an exterior algebra

Mathlib records the graded pieces of an exterior algebra in full: exteriorPower.instFree says that ⋀[R]^n M is free when M is, and exteriorPower.finrank_eq computes its rank as (finrank R M).choose n. It also builds the basis Module.Basis.ExteriorAlgebra of the whole algebra, indexed by the finite subsets of the index set of a basis of M. What it does not record is the consequence: ExteriorAlgebra R M is itself a free module, of rank 2 ^ finrank R M when M is finite free.

This file supplies that. Nothing here is new mathematics — the basis does all the work, and the rank count is Fintype.card_finset, the observation that a finite set with n elements has 2 ^ n subsets, which is the same ∑ₖ (n choose k) = 2 ^ n that summing exteriorPower.finrank_eq over the graded pieces would give. The point is to have the statement, because it is what the dimension count for a Clifford algebra rests on: over a ring in which 2 is invertible, CliffordAlgebra.equivExterior identifies CliffordAlgebra Q with ExteriorAlgebra R M as a module, so every rank statement about the Clifford algebra is a rank statement about the exterior algebra transported along that isomorphism. See TauCeti/LinearAlgebra/CliffordAlgebra/Dimension.lean.

The hypotheses are the weakest the basis needs: a commutative ring R and a free R-module M, with no invertibility of 2 anywhere, since the exterior algebra has a basis over any commutative ring.

Main results

• TauCeti.ExteriorAlgebra.instFree: the exterior algebra of a free module is free.
• TauCeti.ExteriorAlgebra.instFinite: the exterior algebra of a finite free module is a finite module.
• TauCeti.ExteriorAlgebra.finrank_eq_two_pow: finrank R (ExteriorAlgebra R M) = 2 ^ finrank R M.

References

• Clifford algebras, Pin and Spin, and spin representations roadmap, Layer 0, "The associated graded is the exterior algebra (a PBW-type theorem)".

instance TauCeti.ExteriorAlgebra.instFree {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] : Module.Free R (ExteriorAlgebra R M)

The exterior algebra of a free module is free, on the finite subsets of a basis index set.

instance TauCeti.ExteriorAlgebra.instFinite {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] : Module.Finite R (ExteriorAlgebra R M)

The exterior algebra of a finite free module is a finite module: its basis is indexed by the finite subsets of a finite basis index set.

theorem TauCeti.ExteriorAlgebra.finrank_eq_two_pow {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Nontrivial R] [Module.Free R M] [Module.Finite R M] : Module.finrank R (ExteriorAlgebra R M) = 2 ^ Module.finrank R M

The exterior algebra of a finite free module of rank n has rank 2 ^ n: a basis of it is indexed by the subsets of a basis index set of M.