# mathlib3documentation

linear_algebra.exterior_algebra.basic

# Exterior Algebras #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 exterior_algebra R M. It is endowed with the structure of an R-algebra.

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 exterior_algebra.lift R f cond.

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

## Theorems #

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

1. ι_comp_lift is 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 alternating_map corresponding to the wedge product of ι R m terms.

## Implementation details #

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

@[reducible]
def exterior_algebra (R : Type u1) [comm_ring R] (M : Type u2) [ M] :
Type (max u1 u2)

The exterior algebra of an R-module M.

Equations
@[reducible]
def exterior_algebra.ι (R : Type u1) [comm_ring R] {M : Type u2} [ M] :

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

Equations
@[simp]
theorem exterior_algebra.ι_sq_zero {R : Type u1} [comm_ring R] {M : Type u2} [ M] (m : M) :
m * m = 0

As well as being linear, ι m squares to zero

@[simp]
theorem exterior_algebra.comp_ι_sq_zero {R : Type u1} [comm_ring R] {M : Type u2} [ M] {A : Type u_1} [semiring A] [ A] (g : →ₐ[R] A) (m : M) :
g ( m) * g ( m) = 0
def exterior_algebra.lift (R : Type u1) [comm_ring R] {M : Type u2} [ M] {A : Type u_1} [semiring A] [ A] :
{f // (m : M), f m * f m = 0} M →ₐ[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 exterior_algebra R M to A.

Equations
@[simp]
theorem exterior_algebra.lift_symm_apply (R : Type u1) [comm_ring R] {M : Type u2} [ M] {A : Type u_1} [semiring A] [ A] (ᾰ : →ₐ[R] A) :
.symm) = , _⟩
@[simp]
theorem exterior_algebra.ι_comp_lift (R : Type u1) [comm_ring R] {M : Type u2} [ M] {A : Type u_1} [semiring A] [ A] (f : M →ₗ[R] A) (cond : (m : M), f m * f m = 0) :
f, cond⟩).to_linear_map.comp = f
@[simp]
theorem exterior_algebra.lift_ι_apply (R : Type u1) [comm_ring R] {M : Type u2} [ M] {A : Type u_1} [semiring A] [ A] (f : M →ₗ[R] A) (cond : (m : M), f m * f m = 0) (x : M) :
f, cond⟩) ( x) = f x
@[simp]
theorem exterior_algebra.lift_unique (R : Type u1) [comm_ring R] {M : Type u2} [ M] {A : Type u_1} [semiring A] [ A] (f : M →ₗ[R] A) (cond : (m : M), f m * f m = 0) (g : →ₐ[R] A) :
= f g = f, cond⟩
@[simp]
theorem exterior_algebra.lift_comp_ι {R : Type u1} [comm_ring R] {M : Type u2} [ M] {A : Type u_1} [semiring A] [ A] (g : →ₐ[R] A) :
, _⟩ = g
@[ext]
theorem exterior_algebra.hom_ext {R : Type u1} [comm_ring R] {M : Type u2} [ M] {A : Type u_1} [semiring A] [ A] {f g : →ₐ[R] A} (h : = ) :
f = g
theorem exterior_algebra.induction {R : Type u1} [comm_ring R] {M : Type u2} [ M] {C : Prop} (h_grade0 : (r : R), C ( M)) r)) (h_grade1 : (x : M), C ( x)) (h_mul : (a b : M), C a C b C (a * b)) (h_add : (a b : M), C a C b C (a + b)) (a : M) :
C a

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

def exterior_algebra.algebra_map_inv {R : Type u1} [comm_ring R] {M : Type u2} [ M] :

The left-inverse of algebra_map.

Equations
theorem exterior_algebra.algebra_map_left_inverse {R : Type u1} [comm_ring R] (M : Type u2) [ M] :
@[simp]
theorem exterior_algebra.algebra_map_inj {R : Type u1} [comm_ring R] (M : Type u2) [ M] (x y : R) :
M)) x = M)) y x = y
@[simp]
theorem exterior_algebra.algebra_map_eq_zero_iff {R : Type u1} [comm_ring R] (M : Type u2) [ M] (x : R) :
M)) x = 0 x = 0
@[simp]
theorem exterior_algebra.algebra_map_eq_one_iff {R : Type u1} [comm_ring R] (M : Type u2) [ M] (x : R) :
M)) x = 1 x = 1
theorem exterior_algebra.is_unit_algebra_map {R : Type u1} [comm_ring R] (M : Type u2) [ M] (r : R) :
is_unit ( M)) r)
@[simp]
theorem exterior_algebra.invertible_algebra_map_equiv_symm_apply_inv_of {R : Type u1} [comm_ring R] (M : Type u2) [ M] (r : R) (_x : invertible r) :
( M)) r) = M)) ( r)
@[simp]
def exterior_algebra.invertible_algebra_map_equiv {R : Type u1} [comm_ring R] (M : Type u2) [ M] (r : R) :
invertible ( M)) r)

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

Equations
def exterior_algebra.to_triv_sq_zero_ext {R : Type u1} [comm_ring R] {M : Type u2} [ M] [ M] [ M] :

The canonical map from exterior_algebra R M into triv_sq_zero_ext R M that sends exterior_algebra.ι to triv_sq_zero_ext.inr.

Equations
@[simp]
theorem exterior_algebra.to_triv_sq_zero_ext_ι {R : Type u1} [comm_ring R] {M : Type u2} [ M] [ M] [ M] (x : M) :
def exterior_algebra.ι_inv {R : Type u1} [comm_ring R] {M : Type u2} [ M] :

The left-inverse of ι.

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

Equations
theorem exterior_algebra.ι_left_inverse {R : Type u1} [comm_ring R] {M : Type u2} [ M] :
@[simp]
theorem exterior_algebra.ι_inj (R : Type u1) [comm_ring R] {M : Type u2} [ M] (x y : M) :
x = y x = y
@[simp]
theorem exterior_algebra.ι_eq_zero_iff {R : Type u1} [comm_ring R] {M : Type u2} [ M] (x : M) :
x = 0 x = 0
@[simp]
theorem exterior_algebra.ι_eq_algebra_map_iff {R : Type u1} [comm_ring R] {M : Type u2} [ M] (x : M) (r : R) :
x = M)) r x = 0 r = 0
@[simp]
theorem exterior_algebra.ι_ne_one {R : Type u1} [comm_ring R] {M : Type u2} [ M] [nontrivial R] (x : M) :
x 1
theorem exterior_algebra.ι_range_disjoint_one {R : Type u1} [comm_ring R] {M : Type u2} [ M] :

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

@[simp]
theorem exterior_algebra.ι_add_mul_swap {R : Type u1} [comm_ring R] {M : Type u2} [ M] (x y : M) :
x * y + y * x = 0
theorem exterior_algebra.ι_mul_prod_list {R : Type u1} [comm_ring R] {M : Type u2} [ M] {n : } (f : fin n M) (i : fin n) :
(f i) * (list.of_fn (λ (i : fin n), (f i))).prod = 0
def exterior_algebra.ι_multi (R : Type u1) [comm_ring R] {M : Type u2} [ M] (n : ) :
M) (fin n)

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

This is a special case of multilinear_map.mk_pi_algebra_fin, and the exterior algebra version of tensor_algebra.tprod.

Equations
theorem exterior_algebra.ι_multi_apply {R : Type u1} [comm_ring R] {M : Type u2} [ M] {n : } (v : fin n M) :
v = (list.of_fn (λ (i : fin n), (v i))).prod
@[simp]
theorem exterior_algebra.ι_multi_zero_apply {R : Type u1} [comm_ring R] {M : Type u2} [ M] (v : fin 0 M) :
v = 1
@[simp]
theorem exterior_algebra.ι_multi_succ_apply {R : Type u1} [comm_ring R] {M : Type u2} [ M] {n : } (v : fin n.succ M) :
v = (v 0) *
theorem exterior_algebra.ι_multi_succ_curry_left {R : Type u1} [comm_ring R] {M : Type u2} [ M] {n : } (m : M) :
def tensor_algebra.to_exterior {R : Type u1} [comm_ring R] {M : Type u2} [ M] :

The canonical image of the tensor_algebra in the exterior_algebra, which maps tensor_algebra.ι R x to exterior_algebra.ι R x.

Equations
@[simp]
theorem tensor_algebra.to_exterior_ι {R : Type u1} [comm_ring R] {M : Type u2} [ M] (m : M) :