# Exterior Algebras #

We construct the exterior algebra of a module M over a commutative semiring R.

## Notation #

The exterior algebra of the R-module M is denoted as ExteriorAlgebra R M. It is endowed with the structure of an R-algebra.

The nth exterior power of the R-module M is denoted by exteriorPower R n M; it is of type Submodule R (ExteriorAlgebra R M) and defined as LinearMap.range (ExteriorAlgebra.ι R : M →ₗ[R] ExteriorAlgebra R M) ^ n. We also introduce the notation ⋀[R]^n M for exteriorPower R n M.

Given a linear morphism f : M → A from a module M to another R-algebra A, such that cond : ∀ m : M, f m * f m = 0, there is a (unique) lift of f to an R-algebra morphism, which is denoted ExteriorAlgebra.lift R f cond.

The canonical linear map M → ExteriorAlgebra R M is denoted ExteriorAlgebra.ι R.

## Theorems #

The main theorems proved ensure that ExteriorAlgebra R M satisfies the universal property of the exterior algebra.

1. ι_comp_lift is the fact that the composition of ι R with lift R f cond agrees with f.
2. lift_unique ensures the uniqueness of lift R f cond with respect to 1.

## Definitions #

• ιMulti is the AlternatingMap corresponding to the wedge product of ι R m terms.

## Implementation details #

The exterior algebra of M is constructed as simply CliffordAlgebra (0 : QuadraticForm R M), as this avoids us having to duplicate API.

@[reducible]
def ExteriorAlgebra (R : Type u1) [] (M : Type u2) [] [Module R M] :
Type (max u2 u1)

The exterior algebra of an R-module M.

Equations
Instances For
@[reducible]
def ExteriorAlgebra.ι (R : Type u1) [] {M : Type u2} [] [Module R M] :

The canonical linear map M →ₗ[R] ExteriorAlgebra R M.

Equations
Instances For
@[inline, reducible]
abbrev ExteriorAlgebra.exteriorPower (R : Type u1) [] (n : ) (M : Type u2) [] [Module R M] :

Definition of the nth exterior power of a R-module N. We introduce the notation ⋀[R]^n M for exteriorPower R n M.

Equations
Instances For

Definition of the nth exterior power of a R-module N. We introduce the notation ⋀[R]^n M for exteriorPower R n M.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem ExteriorAlgebra.ι_sq_zero {R : Type u1} [] {M : Type u2} [] [Module R M] (m : M) :
m * m = 0

As well as being linear, ι m squares to zero.

theorem ExteriorAlgebra.comp_ι_sq_zero {R : Type u1} [] {M : Type u2} [] [Module R M] {A : Type u_1} [] [Algebra R A] (g : →ₐ[R] A) (m : M) :
g ( m) * g ( m) = 0
@[simp]
theorem ExteriorAlgebra.lift_symm_apply (R : Type u1) [] {M : Type u2} [] [Module R M] {A : Type u_1} [] [Algebra R A] :
∀ (a : →ₐ[R] A), .symm a = { val := (.symm a), property := }
def ExteriorAlgebra.lift (R : Type u1) [] {M : Type u2} [] [Module R M] {A : Type u_1} [] [Algebra R A] :
{ f : M →ₗ[R] A // ∀ (m : M), f m * f m = 0 } ( →ₐ[R] A)

Given a linear map f : M →ₗ[R] A into an R-algebra A, which satisfies the condition: cond : ∀ m : M, f m * f m = 0, this is the canonical lift of f to a morphism of R-algebras from ExteriorAlgebra R M to A.

Equations
Instances For
@[simp]
theorem ExteriorAlgebra.ι_comp_lift (R : Type u1) [] {M : Type u2} [] [Module R M] {A : Type u_1} [] [Algebra R A] (f : M →ₗ[R] A) (cond : ∀ (m : M), f m * f m = 0) :
AlgHom.toLinearMap ( { val := f, property := cond }) ∘ₗ = f
@[simp]
theorem ExteriorAlgebra.lift_ι_apply (R : Type u1) [] {M : Type u2} [] [Module R M] {A : Type u_1} [] [Algebra R A] (f : M →ₗ[R] A) (cond : ∀ (m : M), f m * f m = 0) (x : M) :
( { val := f, property := cond }) ( x) = f x
@[simp]
theorem ExteriorAlgebra.lift_unique (R : Type u1) [] {M : Type u2} [] [Module R M] {A : Type u_1} [] [Algebra R A] (f : M →ₗ[R] A) (cond : ∀ (m : M), f m * f m = 0) (g : →ₐ[R] A) :
= f g = { val := f, property := cond }
@[simp]
theorem ExteriorAlgebra.lift_comp_ι {R : Type u1} [] {M : Type u2} [] [Module R M] {A : Type u_1} [] [Algebra R A] (g : →ₐ[R] A) :
{ val := , property := } = g
theorem ExteriorAlgebra.hom_ext {R : Type u1} [] {M : Type u2} [] [Module R M] {A : Type u_1} [] [Algebra R A] {f : →ₐ[R] A} {g : →ₐ[R] A} (h : ) :
f = g

See note [partially-applied ext lemmas].

theorem ExteriorAlgebra.induction {R : Type u1} [] {M : Type u2} [] [Module R M] {C : Prop} (algebraMap : ∀ (r : R), C (() r)) (ι : ∀ (x : M), C ( x)) (mul : ∀ (a b : ), C aC bC (a * b)) (add : ∀ (a b : ), C aC bC (a + b)) (a : ) :
C a

If C holds for the algebraMap of r : R into ExteriorAlgebra R M, the ι of x : M, and is preserved under addition and muliplication, then it holds for all of ExteriorAlgebra R M.

def ExteriorAlgebra.algebraMapInv {R : Type u1} [] {M : Type u2} [] [Module R M] :

The left-inverse of algebraMap.

Equations
• ExteriorAlgebra.algebraMapInv = { val := 0, property := }
Instances For
theorem ExteriorAlgebra.algebraMap_leftInverse {R : Type u1} [] (M : Type u2) [] [Module R M] :
Function.LeftInverse ExteriorAlgebra.algebraMapInv (algebraMap R ())
@[simp]
theorem ExteriorAlgebra.algebraMap_inj {R : Type u1} [] (M : Type u2) [] [Module R M] (x : R) (y : R) :
(algebraMap R ()) x = (algebraMap R ()) y x = y
@[simp]
theorem ExteriorAlgebra.algebraMap_eq_zero_iff {R : Type u1} [] (M : Type u2) [] [Module R M] (x : R) :
(algebraMap R ()) x = 0 x = 0
@[simp]
theorem ExteriorAlgebra.algebraMap_eq_one_iff {R : Type u1} [] (M : Type u2) [] [Module R M] (x : R) :
(algebraMap R ()) x = 1 x = 1
theorem ExteriorAlgebra.isUnit_algebraMap {R : Type u1} [] (M : Type u2) [] [Module R M] (r : R) :
IsUnit ((algebraMap R ()) r)
@[simp]
theorem ExteriorAlgebra.invertibleAlgebraMapEquiv_symm_apply_invOf_toQuot {R : Type u1} [] (M : Type u2) [] [Module R M] (r : R) :
∀ (x : ), (((algebraMap R ()) r)).toQuot = Quot.mk ((algebraMap R ()) r)
@[simp]
theorem ExteriorAlgebra.invertibleAlgebraMapEquiv_apply_invOf {R : Type u1} [] (M : Type u2) [] [Module R M] (r : R) :
∀ (x : Invertible ((algebraMap R ()) r)), r = (ExteriorAlgebra.algebraMapInv ((algebraMap R ()) r))
def ExteriorAlgebra.invertibleAlgebraMapEquiv {R : Type u1} [] (M : Type u2) [] [Module R M] (r : R) :

Invertibility in the exterior algebra is the same as invertibility of the base ring.

Equations
Instances For
def ExteriorAlgebra.toTrivSqZeroExt {R : Type u1} [] {M : Type u2} [] [Module R M] [] [] :

The canonical map from ExteriorAlgebra R M into TrivSqZeroExt R M that sends ExteriorAlgebra.ι to TrivSqZeroExt.inr.

Equations
• ExteriorAlgebra.toTrivSqZeroExt = { val := , property := }
Instances For
@[simp]
theorem ExteriorAlgebra.toTrivSqZeroExt_ι {R : Type u1} [] {M : Type u2} [] [Module R M] [] [] (x : M) :
ExteriorAlgebra.toTrivSqZeroExt ( x) =
def ExteriorAlgebra.ιInv {R : Type u1} [] {M : Type u2} [] [Module R M] :

The left-inverse of ι.

As an implementation detail, we implement this using TrivSqZeroExt which has a suitable algebra structure.

Equations
Instances For
theorem ExteriorAlgebra.ι_leftInverse {R : Type u1} [] {M : Type u2} [] [Module R M] :
Function.LeftInverse ExteriorAlgebra.ιInv
@[simp]
theorem ExteriorAlgebra.ι_inj (R : Type u1) [] {M : Type u2} [] [Module R M] (x : M) (y : M) :
x = y x = y
@[simp]
theorem ExteriorAlgebra.ι_eq_zero_iff {R : Type u1} [] {M : Type u2} [] [Module R M] (x : M) :
x = 0 x = 0
@[simp]
theorem ExteriorAlgebra.ι_eq_algebraMap_iff {R : Type u1} [] {M : Type u2} [] [Module R M] (x : M) (r : R) :
x = (algebraMap R ()) r x = 0 r = 0
@[simp]
theorem ExteriorAlgebra.ι_ne_one {R : Type u1} [] {M : Type u2} [] [Module R M] [] (x : M) :
x 1
theorem ExteriorAlgebra.ι_range_disjoint_one {R : Type u1} [] {M : Type u2} [] [Module R M] :

The generators of the exterior algebra are disjoint from its scalars.

@[simp]
theorem ExteriorAlgebra.ι_add_mul_swap {R : Type u1} [] {M : Type u2} [] [Module R M] (x : M) (y : M) :
x * y + y * x = 0
theorem ExteriorAlgebra.ι_mul_prod_list {R : Type u1} [] {M : Type u2} [] [Module R M] {n : } (f : Fin nM) (i : Fin n) :
(f i) * List.prod (List.ofFn fun (i : Fin n) => (f i)) = 0
def ExteriorAlgebra.ιMulti (R : Type u1) [] {M : Type u2} [] [Module R M] (n : ) :

The product of n terms of the form ι R m is an alternating map.

This is a special case of MultilinearMap.mkPiAlgebraFin, and the exterior algebra version of TensorAlgebra.tprod.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem ExteriorAlgebra.ιMulti_apply {R : Type u1} [] {M : Type u2} [] [Module R M] {n : } (v : Fin nM) :
() v = List.prod (List.ofFn fun (i : Fin n) => (v i))
@[simp]
theorem ExteriorAlgebra.ιMulti_zero_apply {R : Type u1} [] {M : Type u2} [] [Module R M] (v : Fin 0M) :
() v = 1
@[simp]
theorem ExteriorAlgebra.ιMulti_succ_apply {R : Type u1} [] {M : Type u2} [] [Module R M] {n : } (v : Fin ()M) :
() v = (v 0) * () ()
theorem ExteriorAlgebra.ιMulti_succ_curryLeft {R : Type u1} [] {M : Type u2} [] [Module R M] {n : } (m : M) :
= () ()
theorem ExteriorAlgebra.ιMulti_range (R : Type u1) [] {M : Type u2} [] [Module R M] (n : ) :
(⋀[R]^n M)

The image of ExteriorAlgebra.ιMulti R n is contained in the nth exterior power.

theorem ExteriorAlgebra.ιMulti_span_fixedDegree (R : Type u1) [] {M : Type u2} [] [Module R M] (n : ) :
= ⋀[R]^n M

The image of ExteriorAlgebra.ιMulti R n spans the nth exterior power, as a submodule of the exterior algebra.

@[inline, reducible]
abbrev ExteriorAlgebra.ιMulti_family (R : Type u1) [] {M : Type u2} [] [Module R M] (n : ) {I : Type u_2} [] (v : IM) (s : { s : // s.card = n }) :

Given a linearly ordered family v of vectors of M and a natural number n, produce the family of nfold exterior products of elements of v, seen as members of the exterior algebra.

Equations
• = () fun (i : Fin n) => v (() i)
Instances For
instance ExteriorAlgebra.instNontrivialExteriorAlgebra {R : Type u1} [] {M : Type u2} [] [Module R M] [] :

An ExteriorAlgebra over a nontrivial ring is nontrivial.

Equations
• =

Functoriality of the exterior algebra.

def ExteriorAlgebra.map {R : Type u1} [] {M : Type u2} [] [Module R M] {N : Type u4} [] [Module R N] (f : M →ₗ[R] N) :

The morphism of exterior algebras induced by a linear map.

Equations
Instances For
@[simp]
theorem ExteriorAlgebra.map_comp_ι {R : Type u1} [] {M : Type u2} [] [Module R M] {N : Type u4} [] [Module R N] (f : M →ₗ[R] N) :
= ∘ₗ f
@[simp]
theorem ExteriorAlgebra.map_apply_ι {R : Type u1} [] {M : Type u2} [] [Module R M] {N : Type u4} [] [Module R N] (f : M →ₗ[R] N) (m : M) :
( m) = (f m)
@[simp]
theorem ExteriorAlgebra.map_apply_ιMulti {R : Type u1} [] {M : Type u2} [] [Module R M] {N : Type u4} [] [Module R N] {n : } (f : M →ₗ[R] N) (m : Fin nM) :
(() m) = () (f m)
@[simp]
theorem ExteriorAlgebra.map_comp_ιMulti {R : Type u1} [] {M : Type u2} [] [Module R M] {N : Type u4} [] [Module R N] {n : } (f : M →ₗ[R] N) :
@[simp]
theorem ExteriorAlgebra.map_id {R : Type u1} [] {M : Type u2} [] [Module R M] :
ExteriorAlgebra.map LinearMap.id = AlgHom.id R ()
@[simp]
theorem ExteriorAlgebra.map_comp_map {R : Type u1} [] {M : Type u2} [] [Module R M] {N : Type u4} {N' : Type u5} [] [Module R N] [] [Module R N'] (f : M →ₗ[R] N) (g : N →ₗ[R] N') :
= ExteriorAlgebra.map (g ∘ₗ f)
@[simp]
theorem ExteriorAlgebra.ι_range_map_map {R : Type u1} [] {M : Type u2} [] [Module R M] {N : Type u4} [] [Module R N] (f : M →ₗ[R] N) :
theorem ExteriorAlgebra.toTrivSqZeroExt_comp_map {R : Type u1} [] {M : Type u2} [] [Module R M] {N : Type u4} [] [Module R N] [] [] [] [] (f : M →ₗ[R] N) :
AlgHom.comp ExteriorAlgebra.toTrivSqZeroExt = AlgHom.comp ExteriorAlgebra.toTrivSqZeroExt
theorem ExteriorAlgebra.ιInv_comp_map {R : Type u1} [] {M : Type u2} [] [Module R M] {N : Type u4} [] [Module R N] (f : M →ₗ[R] N) :
ExteriorAlgebra.ιInv ∘ₗ = f ∘ₗ ExteriorAlgebra.ιInv
@[simp]
theorem ExteriorAlgebra.leftInverse_map_iff {R : Type u1} [] {M : Type u2} [] [Module R M] {N : Type u4} [] [Module R N] {f : M →ₗ[R] N} {g : N →ₗ[R] M} :

For a linear map f from M to N, ExteriorAlgebra.map g is a retraction of ExteriorAlgebra.map f iff g is a retraction of f.

theorem ExteriorAlgebra.map_injective {R : Type u1} [] {M : Type u2} [] [Module R M] {N : Type u4} [] [Module R N] {f : M →ₗ[R] N} (hf : ∃ (g : N →ₗ[R] M), g ∘ₗ f = LinearMap.id) :

A morphism of modules that admits a linear retraction induces an injective morphism of exterior algebras.

@[simp]
theorem ExteriorAlgebra.map_surjective_iff {R : Type u1} [] {M : Type u2} [] [Module R M] {N : Type u4} [] [Module R N] {f : M →ₗ[R] N} :

A morphism of modules is surjective if and only the morphism of exterior algebras that it induces is surjective.

theorem ExteriorAlgebra.map_injective_field {K : Type u_2} {E : Type u_3} {F : Type u_4} [] [] [Module K E] [] [Module K F] {f : E →ₗ[K] F} (hf : ) :

An injective morphism of vector spaces induces an injective morphism of exterior algebras.

def TensorAlgebra.toExterior {R : Type u1} [] {M : Type u2} [] [Module R M] :

The canonical image of the TensorAlgebra in the ExteriorAlgebra, which maps TensorAlgebra.ι R x to ExteriorAlgebra.ι R x.

Equations
• TensorAlgebra.toExterior =
Instances For
@[simp]
theorem TensorAlgebra.toExterior_ι {R : Type u1} [] {M : Type u2} [] [Module R M] (m : M) :
TensorAlgebra.toExterior (() m) = m