mathlib documentation

linear_algebra.exterior_algebra

Exterior Algebras

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

Notation

The exterior algebra of the R-semimodule 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 semimodule 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.

Implementation details

The exterior algebra of M is constructed as a quotient of the tensor algebra, as follows.

  1. We define a relation exterior_algebra.rel R M on tensor_algebra R M. This is the smallest relation which identifies squares of elements of M with 0.
  2. The exterior algebra is the quotient of the tensor algebra by this relation.
inductive exterior_algebra.rel (R : Type u_1) [comm_semiring R] (M : Type u_2) [add_comm_monoid M] [semimodule R M] :
tensor_algebra R Mtensor_algebra R M → Prop

rel relates each ι m * ι m, for m : M, with 0.

The exterior algebra of M is defined as the quotient modulo this relation.

def exterior_algebra (R : Type u_1) [comm_semiring R] (M : Type u_2) [add_comm_monoid M] [semimodule R M] :
Type (max u_1 u_2)

The exterior algebra of an R-semimodule M.

Equations
@[instance]
def exterior_algebra.inst (R : Type u_1) [comm_semiring R] (M : Type u_2) [add_comm_monoid M] [semimodule R M] :

@[instance]
def exterior_algebra.inhabited (R : Type u_1) [comm_semiring R] (M : Type u_2) [add_comm_monoid M] [semimodule R M] :

@[instance]
def exterior_algebra.semiring (R : Type u_1) [comm_semiring R] (M : Type u_2) [add_comm_monoid M] [semimodule R M] :

@[instance]
def exterior_algebra.ring {M : Type u_2} [add_comm_monoid M] {S : Type u_1} [comm_ring S] [semimodule S M] :

Equations
def exterior_algebra.ι (R : Type u_1) [comm_semiring R] {M : Type u_2} [add_comm_monoid M] [semimodule R M] :

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

Equations
@[simp]
theorem exterior_algebra.ι_square_zero {R : Type u_1} [comm_semiring R] {M : Type u_2} [add_comm_monoid M] [semimodule R M] (m : M) :

As well as being linear, ι m squares to zero

@[simp]
theorem exterior_algebra.comp_ι_square_zero {R : Type u_1} [comm_semiring R] {M : Type u_2} [add_comm_monoid M] [semimodule R M] {A : Type u_3} [semiring A] [algebra R A] (g : exterior_algebra R M →ₐ[R] A) (m : M) :

def exterior_algebra.lift (R : Type u_1) [comm_semiring R] {M : Type u_2} [add_comm_monoid M] [semimodule R M] {A : Type u_3} [semiring A] [algebra R A] :
{f // ∀ (m : M), (f m) * f m = 0} (exterior_algebra R 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 u_1) [comm_semiring R] {M : Type u_2} [add_comm_monoid M] [semimodule R M] {A : Type u_3} [semiring A] [algebra R A] (F : exterior_algebra R M →ₐ[R] A) :

@[simp]
theorem exterior_algebra.ι_comp_lift (R : Type u_1) [comm_semiring R] {M : Type u_2} [add_comm_monoid M] [semimodule R M] {A : Type u_3} [semiring A] [algebra R A] (f : M →ₗ[R] A) (cond : ∀ (m : M), (f m) * f m = 0) :

@[simp]
theorem exterior_algebra.lift_ι_apply (R : Type u_1) [comm_semiring R] {M : Type u_2} [add_comm_monoid M] [semimodule R M] {A : Type u_3} [semiring A] [algebra R A] (f : M →ₗ[R] A) (cond : ∀ (m : M), (f m) * f m = 0) (x : M) :

@[simp]
theorem exterior_algebra.lift_unique (R : Type u_1) [comm_semiring R] {M : Type u_2} [add_comm_monoid M] [semimodule R M] {A : Type u_3} [semiring A] [algebra R A] (f : M →ₗ[R] A) (cond : ∀ (m : M), (f m) * f m = 0) (g : exterior_algebra R M →ₐ[R] A) :

@[simp]
theorem exterior_algebra.lift_comp_ι {R : Type u_1} [comm_semiring R] {M : Type u_2} [add_comm_monoid M] [semimodule R M] {A : Type u_3} [semiring A] [algebra R A] (g : exterior_algebra R M →ₐ[R] A) :

@[ext]
theorem exterior_algebra.hom_ext {R : Type u_1} [comm_semiring R] {M : Type u_2} [add_comm_monoid M] [semimodule R M] {A : Type u_3} [semiring A] [algebra R A] {f g : exterior_algebra R M →ₐ[R] A} (h : f.to_linear_map.comp (exterior_algebra.ι R) = g.to_linear_map.comp (exterior_algebra.ι R)) :
f = g