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.

ι_comp_lift is fact that the composition of ι R with lift R f cond agrees with f.
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.

source

@[reducible]

def exterior_algebra (R : Type u1) [comm_ring R] (M : Type u2) [add_comm_group M] [module R M] :

Type (max u1 u2)

The exterior algebra of an R-module M.

Equations

exterior_algebra R M = clifford_algebra 0

source

@[reducible]

def exterior_algebra.ι (R : Type u1) [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] :

M →ₗ[R] exterior_algebra R M

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

Equations

exterior_algebra.ι R = clifford_algebra.ι 0

source

@[simp]

theorem exterior_algebra.ι_sq_zero {R : Type u1} [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] (m : M) :

⇑(exterior_algebra.ι R) m * ⇑(exterior_algebra.ι R) m = 0

As well as being linear, ι m squares to zero

source

@[simp]

theorem exterior_algebra.comp_ι_sq_zero {R : Type u1} [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] {A : Type u_1} [semiring A] [algebra R A] (g : exterior_algebra R M →ₐ[R] A) (m : M) :

⇑g (⇑(exterior_algebra.ι R) m) * ⇑g (⇑(exterior_algebra.ι R) m) = 0

source

def exterior_algebra.lift (R : Type u1) [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] {A : Type u_1} [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

exterior_algebra.lift R = ((equiv.refl (M →ₗ[R] A)).subtype_equiv _).trans (clifford_algebra.lift 0)

source

@[simp]

theorem exterior_algebra.lift_symm_apply (R : Type u1) [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] {A : Type u_1} [semiring A] [algebra R A] (ᾰ : exterior_algebra R M →ₐ[R] A) :

⇑((exterior_algebra.lift R).symm) ᾰ = ⟨ᾰ.to_linear_map.comp (clifford_algebra.ι 0), _⟩

source

@[simp]

theorem exterior_algebra.ι_comp_lift (R : Type u1) [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] {A : Type u_1} [semiring A] [algebra R A] (f : M →ₗ[R] A) (cond : ∀ (m : M), ⇑f m * ⇑f m = 0) :

(⇑(exterior_algebra.lift R) ⟨f, cond⟩).to_linear_map.comp (exterior_algebra.ι R) = f

source

@[simp]

theorem exterior_algebra.lift_ι_apply (R : Type u1) [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] {A : Type u_1} [semiring A] [algebra R A] (f : M →ₗ[R] A) (cond : ∀ (m : M), ⇑f m * ⇑f m = 0) (x : M) :

⇑(⇑(exterior_algebra.lift R) ⟨f, cond⟩) (⇑(exterior_algebra.ι R) x) = ⇑f x

source

@[simp]

theorem exterior_algebra.lift_unique (R : Type u1) [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] {A : Type u_1} [semiring A] [algebra R A] (f : M →ₗ[R] A) (cond : ∀ (m : M), ⇑f m * ⇑f m = 0) (g : exterior_algebra R M →ₐ[R] A) :

g.to_linear_map.comp (exterior_algebra.ι R) = f ↔ g = ⇑(exterior_algebra.lift R) ⟨f, cond⟩

source

@[simp]

theorem exterior_algebra.lift_comp_ι {R : Type u1} [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] {A : Type u_1} [semiring A] [algebra R A] (g : exterior_algebra R M →ₐ[R] A) :

⇑(exterior_algebra.lift R) ⟨g.to_linear_map.comp (exterior_algebra.ι R), _⟩ = g

source

@[ext]

theorem exterior_algebra.hom_ext {R : Type u1} [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] {A : Type u_1} [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

See note [partially-applied ext lemmas].

source

theorem exterior_algebra.induction {R : Type u1} [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] {C : exterior_algebra R M → Prop} (h_grade0 : ∀ (r : R), C (⇑(algebra_map R (exterior_algebra R M)) r)) (h_grade1 : ∀ (x : M), C (⇑(exterior_algebra.ι R) x)) (h_mul : ∀ (a b : exterior_algebra R M), C a → C b → C (a * b)) (h_add : ∀ (a b : exterior_algebra R M), C a → C b → C (a + b)) (a : exterior_algebra R 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.

source

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

exterior_algebra R M →ₐ[R] R

The left-inverse of algebra_map.

Equations

exterior_algebra.algebra_map_inv = ⇑(exterior_algebra.lift R) ⟨0, _⟩

source

theorem exterior_algebra.algebra_map_left_inverse {R : Type u1} [comm_ring R] (M : Type u2) [add_comm_group M] [module R M] :

function.left_inverse ⇑exterior_algebra.algebra_map_inv ⇑(algebra_map R (exterior_algebra R M))

source

@[simp]

theorem exterior_algebra.algebra_map_inj {R : Type u1} [comm_ring R] (M : Type u2) [add_comm_group M] [module R M] (x y : R) :

⇑(algebra_map R (exterior_algebra R M)) x = ⇑(algebra_map R (exterior_algebra R M)) y ↔ x = y

source

@[simp]

theorem exterior_algebra.algebra_map_eq_zero_iff {R : Type u1} [comm_ring R] (M : Type u2) [add_comm_group M] [module R M] (x : R) :

⇑(algebra_map R (exterior_algebra R M)) x = 0 ↔ x = 0

source

@[simp]

theorem exterior_algebra.algebra_map_eq_one_iff {R : Type u1} [comm_ring R] (M : Type u2) [add_comm_group M] [module R M] (x : R) :

⇑(algebra_map R (exterior_algebra R M)) x = 1 ↔ x = 1

source

theorem exterior_algebra.is_unit_algebra_map {R : Type u1} [comm_ring R] (M : Type u2) [add_comm_group M] [module R M] (r : R) :

is_unit (⇑(algebra_map R (exterior_algebra R M)) r) ↔ is_unit r

source

@[simp]

theorem exterior_algebra.invertible_algebra_map_equiv_symm_apply_inv_of {R : Type u1} [comm_ring R] (M : Type u2) [add_comm_group M] [module R M] (r : R) (_x : invertible r) :

⅟ (⇑(algebra_map R (exterior_algebra R M)) r) = ⇑(algebra_map R (exterior_algebra R M)) (⅟ r)

source

@[simp]

theorem exterior_algebra.invertible_algebra_map_equiv_apply_inv_of {R : Type u1} [comm_ring R] (M : Type u2) [add_comm_group M] [module R M] (r : R) (_x : invertible (⇑(algebra_map R (exterior_algebra R M)) r)) :

⅟ r = ⅟ (⇑exterior_algebra.algebra_map_inv (⇑(algebra_map R (exterior_algebra R M)) r))

source

def exterior_algebra.invertible_algebra_map_equiv {R : Type u1} [comm_ring R] (M : Type u2) [add_comm_group M] [module R M] (r : R) :

invertible (⇑(algebra_map R (exterior_algebra R M)) r) ≃ invertible r

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

Equations

exterior_algebra.invertible_algebra_map_equiv M r = invertible_equiv_of_left_inverse (algebra_map R (exterior_algebra R M)) exterior_algebra.algebra_map_inv r _

source

def exterior_algebra.to_triv_sq_zero_ext {R : Type u1} [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] [module Rᵐᵒᵖ M] [is_central_scalar R M] :

exterior_algebra R M →ₐ[R] triv_sq_zero_ext R 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

exterior_algebra.to_triv_sq_zero_ext = ⇑(exterior_algebra.lift R) ⟨triv_sq_zero_ext.inr_hom R M _inst_3, _⟩

source

@[simp]

theorem exterior_algebra.to_triv_sq_zero_ext_ι {R : Type u1} [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] [module Rᵐᵒᵖ M] [is_central_scalar R M] (x : M) :

⇑exterior_algebra.to_triv_sq_zero_ext (⇑(exterior_algebra.ι R) x) = triv_sq_zero_ext.inr x

source

def exterior_algebra.ι_inv {R : Type u1} [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] :

exterior_algebra R M →ₗ[R] M

The left-inverse of ι.

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

Equations

exterior_algebra.ι_inv = let _inst : module Rᵐᵒᵖ M := module.comp_hom M ((ring_hom.id R).from_opposite exterior_algebra.ι_inv._proof_1) in (triv_sq_zero_ext.snd_hom R M).comp exterior_algebra.to_triv_sq_zero_ext.to_linear_map

source

theorem exterior_algebra.ι_left_inverse {R : Type u1} [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] :

function.left_inverse ⇑exterior_algebra.ι_inv ⇑(exterior_algebra.ι R)

source

@[simp]

theorem exterior_algebra.ι_inj (R : Type u1) [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] (x y : M) :

⇑(exterior_algebra.ι R) x = ⇑(exterior_algebra.ι R) y ↔ x = y

source

@[simp]

theorem exterior_algebra.ι_eq_zero_iff {R : Type u1} [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] (x : M) :

⇑(exterior_algebra.ι R) x = 0 ↔ x = 0

source

@[simp]

theorem exterior_algebra.ι_eq_algebra_map_iff {R : Type u1} [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] (x : M) (r : R) :

⇑(exterior_algebra.ι R) x = ⇑(algebra_map R (exterior_algebra R M)) r ↔ x = 0 ∧ r = 0

source

@[simp]

theorem exterior_algebra.ι_ne_one {R : Type u1} [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] [nontrivial R] (x : M) :

⇑(exterior_algebra.ι R) x ≠ 1

source

theorem exterior_algebra.ι_range_disjoint_one {R : Type u1} [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] :

disjoint (linear_map.range (exterior_algebra.ι R)) 1

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

source

@[simp]

theorem exterior_algebra.ι_add_mul_swap {R : Type u1} [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] (x y : M) :

⇑(exterior_algebra.ι R) x * ⇑(exterior_algebra.ι R) y + ⇑(exterior_algebra.ι R) y * ⇑(exterior_algebra.ι R) x = 0

source

theorem exterior_algebra.ι_mul_prod_list {R : Type u1} [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] {n : ℕ} (f : fin n → M) (i : fin n) :

⇑(exterior_algebra.ι R) (f i) * (list.of_fn (λ (i : fin n), ⇑(exterior_algebra.ι R) (f i))).prod = 0

source

def exterior_algebra.ι_multi (R : Type u1) [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] (n : ℕ) :

alternating_map R M (exterior_algebra R 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

exterior_algebra.ι_multi R n = let F : multilinear_map R (λ (i : fin n), M) (exterior_algebra R M) := (multilinear_map.mk_pi_algebra_fin R n (exterior_algebra R M)).comp_linear_map (λ (i : fin n), exterior_algebra.ι R) in {to_fun := ⇑F, map_add' := _, map_smul' := _, map_eq_zero_of_eq' := _}

source

theorem exterior_algebra.ι_multi_apply {R : Type u1} [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] {n : ℕ} (v : fin n → M) :

⇑(exterior_algebra.ι_multi R n) v = (list.of_fn (λ (i : fin n), ⇑(exterior_algebra.ι R) (v i))).prod

source

@[simp]

theorem exterior_algebra.ι_multi_zero_apply {R : Type u1} [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] (v : fin 0 → M) :

⇑(exterior_algebra.ι_multi R 0) v = 1

source

@[simp]

theorem exterior_algebra.ι_multi_succ_apply {R : Type u1} [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] {n : ℕ} (v : fin n.succ → M) :

⇑(exterior_algebra.ι_multi R n.succ) v = ⇑(exterior_algebra.ι R) (v 0) * ⇑(exterior_algebra.ι_multi R n) (matrix.vec_tail v)

source

theorem exterior_algebra.ι_multi_succ_curry_left {R : Type u1} [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] {n : ℕ} (m : M) :

⇑((exterior_algebra.ι_multi R n.succ).curry_left) m = ⇑((linear_map.mul_left R (⇑(exterior_algebra.ι R) m)).comp_alternating_map) (exterior_algebra.ι_multi R n)

source

def tensor_algebra.to_exterior {R : Type u1} [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] :

tensor_algebra R M →ₐ[R] exterior_algebra R M

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

Equations

tensor_algebra.to_exterior = ⇑(tensor_algebra.lift R) (exterior_algebra.ι R)

source

@[simp]

theorem tensor_algebra.to_exterior_ι {R : Type u1} [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] (m : M) :

⇑tensor_algebra.to_exterior (⇑(tensor_algebra.ι R) m) = ⇑(exterior_algebra.ι R) m