Exterior Algebras #
We construct the exterior algebra of a module
M over a commutative semiring
The exterior algebra of the
M is denoted as
ExteriorAlgebra R M.
It is endowed with the structure of an
Given a linear morphism
f : M → A from a module
M to another
A, such that
cond : ∀ m : M, f m * f m = 0, there is a (unique) lift of
f to an
which is denoted
ExteriorAlgebra.lift R f cond.
The main theorems proved ensure that
ExteriorAlgebra R M satisfies the universal property
of the exterior algebra.
ι_comp_liftis the fact that the composition of
lift R f condagrees with
lift_uniqueensures the uniqueness of
lift R f condwith respect to 1.
Implementation details #
Given a linear map
f : M →ₗ[R] A into an
A, which satisfies the condition:
cond : ∀ m : M, f m * f m = 0, this is the canonical lift of
f to a morphism of
ExteriorAlgebra R M to
See note [partially-applied ext lemmas].
The product of
n terms of the form
ι R m is an alternating map.