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.

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.

ι_comp_lift is the 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 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.

source

@[reducible]

def ExteriorAlgebra (R : Type u1) [CommRing R] (M : Type u2) [AddCommGroup M] [Module R M] :

Type (max u2 u1)

The exterior algebra of an R-module M.

Instances For

source

@[reducible]

def ExteriorAlgebra.ι (R : Type u1) [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] :

M →ₗ[R] ExteriorAlgebra R M

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

Instances For

source

theorem ExteriorAlgebra.ι_sq_zero {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (m : M) :

↑(ExteriorAlgebra.ι R) m * ↑(ExteriorAlgebra.ι R) m = 0

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

source

theorem ExteriorAlgebra.comp_ι_sq_zero {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {A : Type u_1} [Semiring A] [Algebra R A] (g : ExteriorAlgebra R M →ₐ[R] A) (m : M) :

↑g (↑(ExteriorAlgebra.ι R) m) * ↑g (↑(ExteriorAlgebra.ι R) m) = 0

source

@[simp]

theorem ExteriorAlgebra.lift_symm_apply (R : Type u1) [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {A : Type u_1} [Semiring A] [Algebra R A] :

∀ (a : ExteriorAlgebra R M →ₐ[R] A), ↑(ExteriorAlgebra.lift R).symm a = { val := ↑(↑(CliffordAlgebra.lift 0).symm a), property := (_ : ∀ (m : M), ↑↑(↑(CliffordAlgebra.lift 0).symm a) m * ↑↑(↑(CliffordAlgebra.lift 0).symm a) m = 0) }

source

def ExteriorAlgebra.lift (R : Type u1) [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {A : Type u_1} [Semiring A] [Algebra R A] :

{ f // ∀ (m : M), ↑f m * ↑f m = 0 } ≃ (ExteriorAlgebra 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 ExteriorAlgebra R M to A.

Instances For

source

@[simp]

theorem ExteriorAlgebra.ι_comp_lift (R : Type u1) [CommRing R] {M : Type u2} [AddCommGroup 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) :

LinearMap.comp (AlgHom.toLinearMap (↑(ExteriorAlgebra.lift R) { val := f, property := cond })) (ExteriorAlgebra.ι R) = f

source

@[simp]

theorem ExteriorAlgebra.lift_ι_apply (R : Type u1) [CommRing R] {M : Type u2} [AddCommGroup 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) :

↑(↑(ExteriorAlgebra.lift R) { val := f, property := cond }) (↑(ExteriorAlgebra.ι R) x) = ↑f x

source

@[simp]

theorem ExteriorAlgebra.lift_unique (R : Type u1) [CommRing R] {M : Type u2} [AddCommGroup 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 : ExteriorAlgebra R M →ₐ[R] A) :

LinearMap.comp (AlgHom.toLinearMap g) (ExteriorAlgebra.ι R) = f ↔ g = ↑(ExteriorAlgebra.lift R) { val := f, property := cond }

source

@[simp]

theorem ExteriorAlgebra.lift_comp_ι {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {A : Type u_1} [Semiring A] [Algebra R A] (g : ExteriorAlgebra R M →ₐ[R] A) :

↑(ExteriorAlgebra.lift R) { val := LinearMap.comp (AlgHom.toLinearMap g) (ExteriorAlgebra.ι R), property := (_ : ∀ (m : M), ↑g (↑(ExteriorAlgebra.ι R) m) * ↑g (↑(ExteriorAlgebra.ι R) m) = 0) } = g

source

theorem ExteriorAlgebra.hom_ext {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {A : Type u_1} [Semiring A] [Algebra R A] {f : ExteriorAlgebra R M →ₐ[R] A} {g : ExteriorAlgebra R M →ₐ[R] A} (h : LinearMap.comp (AlgHom.toLinearMap f) (ExteriorAlgebra.ι R) = LinearMap.comp (AlgHom.toLinearMap g) (ExteriorAlgebra.ι R)) :

f = g

See note [partially-applied ext lemmas].

source

theorem ExteriorAlgebra.induction {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {C : ExteriorAlgebra R M → Prop} (h_grade0 : (r : R) → C (↑(algebraMap R (ExteriorAlgebra R M)) r)) (h_grade1 : (x : M) → C (↑(ExteriorAlgebra.ι R) x)) (h_mul : (a b : ExteriorAlgebra R M) → C a → C b → C (a * b)) (h_add : (a b : ExteriorAlgebra R M) → C a → C b → C (a + b)) (a : ExteriorAlgebra R M) :

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.

source

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

ExteriorAlgebra R M →ₐ[R] R

The left-inverse of algebraMap.

Instances For

source

theorem ExteriorAlgebra.algebraMap_leftInverse {R : Type u1} [CommRing R] (M : Type u2) [AddCommGroup M] [Module R M] :

Function.LeftInverse ↑ExteriorAlgebra.algebraMapInv ↑(algebraMap R (ExteriorAlgebra R M))

source

@[simp]

theorem ExteriorAlgebra.algebraMap_inj {R : Type u1} [CommRing R] (M : Type u2) [AddCommGroup M] [Module R M] (x : R) (y : R) :

↑(algebraMap R (ExteriorAlgebra R M)) x = ↑(algebraMap R (ExteriorAlgebra R M)) y ↔ x = y

source

@[simp]

theorem ExteriorAlgebra.algebraMap_eq_zero_iff {R : Type u1} [CommRing R] (M : Type u2) [AddCommGroup M] [Module R M] (x : R) :

↑(algebraMap R (ExteriorAlgebra R M)) x = 0 ↔ x = 0

source

@[simp]

theorem ExteriorAlgebra.algebraMap_eq_one_iff {R : Type u1} [CommRing R] (M : Type u2) [AddCommGroup M] [Module R M] (x : R) :

↑(algebraMap R (ExteriorAlgebra R M)) x = 1 ↔ x = 1

source

theorem ExteriorAlgebra.isUnit_algebraMap {R : Type u1} [CommRing R] (M : Type u2) [AddCommGroup M] [Module R M] (r : R) :

IsUnit (↑(algebraMap R (ExteriorAlgebra R M)) r) ↔ IsUnit r

source

@[simp]

theorem ExteriorAlgebra.invertibleAlgebraMapEquiv_symm_apply_invOf_toQuot {R : Type u1} [CommRing R] (M : Type u2) [AddCommGroup M] [Module R M] (r : R) :

∀ (x : Invertible r), (⅟(↑(algebraMap R (ExteriorAlgebra R M)) r)).toQuot = Quot.mk (RingQuot.Rel (CliffordAlgebra.Rel 0)) (↑(algebraMap R (TensorAlgebra R M)) ⅟r)

source

@[simp]

theorem ExteriorAlgebra.invertibleAlgebraMapEquiv_apply_invOf {R : Type u1} [CommRing R] (M : Type u2) [AddCommGroup M] [Module R M] (r : R) :

∀ (x : Invertible (↑(algebraMap R (ExteriorAlgebra R M)) r)), ⅟r = ⅟(↑ExteriorAlgebra.algebraMapInv (↑(algebraMap R (ExteriorAlgebra R M)) r))

source

def ExteriorAlgebra.invertibleAlgebraMapEquiv {R : Type u1} [CommRing R] (M : Type u2) [AddCommGroup M] [Module R M] (r : R) :

Invertible (↑(algebraMap R (ExteriorAlgebra R M)) r) ≃ Invertible r

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

Instances For

source

def ExteriorAlgebra.toTrivSqZeroExt {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] [Module Rᵐᵒᵖ M] [IsCentralScalar R M] :

ExteriorAlgebra R M →ₐ[R] TrivSqZeroExt R M

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

Instances For

source

@[simp]

theorem ExteriorAlgebra.toTrivSqZeroExt_ι {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] [Module Rᵐᵒᵖ M] [IsCentralScalar R M] (x : M) :

↑ExteriorAlgebra.toTrivSqZeroExt (↑(ExteriorAlgebra.ι R) x) = TrivSqZeroExt.inr x

source

def ExteriorAlgebra.ιInv {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] :

ExteriorAlgebra R M →ₗ[R] M

The left-inverse of ι.

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

Instances For

source

theorem ExteriorAlgebra.ι_leftInverse {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] :

Function.LeftInverse ↑ExteriorAlgebra.ιInv.toAddHom ↑(ExteriorAlgebra.ι R)

source

@[simp]

theorem ExteriorAlgebra.ι_inj (R : Type u1) [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (x : M) (y : M) :

↑(ExteriorAlgebra.ι R) x = ↑(ExteriorAlgebra.ι R) y ↔ x = y

source

@[simp]

theorem ExteriorAlgebra.ι_eq_zero_iff {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (x : M) :

↑(ExteriorAlgebra.ι R) x = 0 ↔ x = 0

source

@[simp]

theorem ExteriorAlgebra.ι_eq_algebraMap_iff {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (x : M) (r : R) :

↑(ExteriorAlgebra.ι R) x = ↑(algebraMap R (ExteriorAlgebra R M)) r ↔ x = 0 ∧ r = 0

source

@[simp]

theorem ExteriorAlgebra.ι_ne_one {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] [Nontrivial R] (x : M) :

↑(ExteriorAlgebra.ι R) x ≠ 1

source

theorem ExteriorAlgebra.ι_range_disjoint_one {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] :

Disjoint (LinearMap.range (ExteriorAlgebra.ι R)) 1

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

source

@[simp]

theorem ExteriorAlgebra.ι_add_mul_swap {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (x : M) (y : M) :

↑(ExteriorAlgebra.ι R) x * ↑(ExteriorAlgebra.ι R) y + ↑(ExteriorAlgebra.ι R) y * ↑(ExteriorAlgebra.ι R) x = 0

source

theorem ExteriorAlgebra.ι_mul_prod_list {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {n : ℕ} (f : Fin n → M) (i : Fin n) :

↑(ExteriorAlgebra.ι R) (f i) * List.prod (List.ofFn fun i => ↑(ExteriorAlgebra.ι R) (f i)) = 0

source

def ExteriorAlgebra.ιMulti (R : Type u1) [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (n : ℕ) :

AlternatingMap R M (ExteriorAlgebra R M) (Fin 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.

Instances For

source

theorem ExteriorAlgebra.ιMulti_apply {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {n : ℕ} (v : Fin n → M) :

↑(ExteriorAlgebra.ιMulti R n) v = List.prod (List.ofFn fun i => ↑(ExteriorAlgebra.ι R) (v i))

source

@[simp]

theorem ExteriorAlgebra.ιMulti_zero_apply {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (v : Fin 0 → M) :

↑(ExteriorAlgebra.ιMulti R 0) v = 1

source

@[simp]

theorem ExteriorAlgebra.ιMulti_succ_apply {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {n : ℕ} (v : Fin (Nat.succ n) → M) :

↑(ExteriorAlgebra.ιMulti R (Nat.succ n)) v = ↑(ExteriorAlgebra.ι R) (v 0) * ↑(ExteriorAlgebra.ιMulti R n) (Matrix.vecTail v)

source

theorem ExteriorAlgebra.ιMulti_succ_curryLeft {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {n : ℕ} (m : M) :

↑(AlternatingMap.curryLeft (ExteriorAlgebra.ιMulti R (Nat.succ n))) m = ↑(LinearMap.compAlternatingMap (LinearMap.mulLeft R (↑(ExteriorAlgebra.ι R) m))) (ExteriorAlgebra.ιMulti R n)

source

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

TensorAlgebra R M →ₐ[R] ExteriorAlgebra R M

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

Instances For

source

@[simp]

theorem TensorAlgebra.toExterior_ι {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (m : M) :

↑TensorAlgebra.toExterior (↑(TensorAlgebra.ι R) m) = ↑(ExteriorAlgebra.ι R) m