Exterior Algebras #
We construct the exterior algebra of a module
M over a commutative semiring
The exterior algebra of the
M is denoted as
exterior_algebra 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
exterior_algebra.lift R f cond.
The main theorems proved ensure that
exterior_algebra R M satisfies the universal property
of the exterior algebra.
ι_comp_liftis fact that the composition of
lift R f condagrees with
lift_uniqueensures the uniqueness of
lift R f condwith respect to 1.
alternating_mapcorresponding to the wedge product of
ι R mterms.
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
exterior_algebra R M to
Invertibility in the exterior algebra is the same as invertibility of the base ring.
The left-inverse of
As an implementation detail, we implement this using
triv_sq_zero_ext which has a suitable
The product of
n terms of the form
ι R m is an alternating map.