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) [CommRing R] (M : Type u2) [AddCommGroup M] [Module R M] : Type (max u2 u1)

The exterior algebra of an R-module M.

Equations

• ExteriorAlgebra R M = CliffordAlgebra 0

@[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.

Equations

• ExteriorAlgebra.ι R = CliffordAlgebra.ι 0

@[inline, reducible]

abbrev ExteriorAlgebra.exteriorPower (R : Type u1) [CommRing R] (n : ℕ) (M : Type u2) [AddCommGroup M] [Module R M] : Submodule R (ExteriorAlgebra 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

• ⋀[R]^n M = LinearMap.range (ExteriorAlgebra.ι R) ^ n

def ExteriorAlgebra.«term⋀[_]^_» : Lean.ParserDescr

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.

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.

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

@[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 := ⋯ }

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 →ₗ[R] A // ∀ (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.

Equations

• ExteriorAlgebra.lift R = (Equiv.subtypeEquiv (Equiv.refl (M →ₗ[R] A)) ⋯).trans (CliffordAlgebra.lift 0)

@[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) : AlgHom.toLinearMap ((ExteriorAlgebra.lift R) { val := f, property := cond }) ∘ₗ ExteriorAlgebra.ι R = f

@[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

@[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) : AlgHom.toLinearMap g ∘ₗ ExteriorAlgebra.ι R = f ↔ g = (ExteriorAlgebra.lift R) { val := f, property := cond }

@[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 := AlgHom.toLinearMap g ∘ₗ ExteriorAlgebra.ι R, property := ⋯ } = g

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 : AlgHom.toLinearMap f ∘ₗ ExteriorAlgebra.ι R = AlgHom.toLinearMap g ∘ₗ ExteriorAlgebra.ι R) : f = g

See note [partially-applied ext lemmas].

theorem ExteriorAlgebra.induction {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {C : ExteriorAlgebra R M → Prop} (algebraMap : ∀ (r : R), C ((_root_.algebraMap R (ExteriorAlgebra R M)) r)) (ι : ∀ (x : M), C ((ExteriorAlgebra.ι R) x)) (mul : ∀ (a b : ExteriorAlgebra R M), C a → C b → C (a * b)) (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.

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.

Equations

• ExteriorAlgebra.algebraMapInv = (ExteriorAlgebra.lift R) { val := 0, property := ⋯ }

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))

@[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

@[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

@[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

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

@[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)

@[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))

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.

Equations

• ExteriorAlgebra.invertibleAlgebraMapEquiv M r = invertibleEquivOfLeftInverse (algebraMap R (ExteriorAlgebra R M)) ExteriorAlgebra.algebraMapInv r ⋯

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.

Equations

• ExteriorAlgebra.toTrivSqZeroExt = (ExteriorAlgebra.lift R) { val := TrivSqZeroExt.inrHom R M, property := ⋯ }

@[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

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.

Equations

• ExteriorAlgebra.ιInv = TrivSqZeroExt.sndHom R M ∘ₗ AlgHom.toLinearMap ExteriorAlgebra.toTrivSqZeroExt

theorem ExteriorAlgebra.ι_leftInverse {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] : Function.LeftInverse ⇑ExteriorAlgebra.ιInv ⇑(ExteriorAlgebra.ι R)

@[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

@[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

@[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

@[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

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.

@[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

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 : Fin n) => (ExteriorAlgebra.ι R) (f i)) = 0

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

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.

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 : Fin n) => (ExteriorAlgebra.ι R) (v i))

@[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

@[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)

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)

theorem ExteriorAlgebra.ιMulti_range (R : Type u1) [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (n : ℕ) : Set.range ⇑(ExteriorAlgebra.ιMulti R 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) [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (n : ℕ) : Submodule.span R (Set.range ⇑(ExteriorAlgebra.ιMulti R 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) [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (n : ℕ) {I : Type u_2} [LinearOrder I] (v : I → M) (s : { s : Finset I // s.card = n }) : ExteriorAlgebra R M

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

• ExteriorAlgebra.ιMulti_family R n v s = (ExteriorAlgebra.ιMulti R n) fun (i : Fin n) => v ↑((Finset.orderIsoOfFin ↑s ⋯) i)

instance ExteriorAlgebra.instNontrivialExteriorAlgebra {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] [Nontrivial R] : Nontrivial (ExteriorAlgebra R M)

An ExteriorAlgebra over a nontrivial ring is nontrivial.

Equations

• ⋯ = ⋯

Functoriality of the exterior algebra.

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

The morphism of exterior algebras induced by a linear map.

Equations

• ExteriorAlgebra.map f = CliffordAlgebra.map { toLinearMap := f, map_app' := ⋯ }

@[simp]

theorem ExteriorAlgebra.map_comp_ι {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {N : Type u4} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) : AlgHom.toLinearMap (ExteriorAlgebra.map f) ∘ₗ ExteriorAlgebra.ι R = ExteriorAlgebra.ι R ∘ₗ f

@[simp]

theorem ExteriorAlgebra.map_apply_ι {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {N : Type u4} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (m : M) : (ExteriorAlgebra.map f) ((ExteriorAlgebra.ι R) m) = (ExteriorAlgebra.ι R) (f m)

@[simp]

theorem ExteriorAlgebra.map_apply_ιMulti {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {N : Type u4} [AddCommGroup N] [Module R N] {n : ℕ} (f : M →ₗ[R] N) (m : Fin n → M) : (ExteriorAlgebra.map f) ((ExteriorAlgebra.ιMulti R n) m) = (ExteriorAlgebra.ιMulti R n) (⇑f ∘ m)

@[simp]

theorem ExteriorAlgebra.map_comp_ιMulti {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {N : Type u4} [AddCommGroup N] [Module R N] {n : ℕ} (f : M →ₗ[R] N) : (LinearMap.compAlternatingMap (AlgHom.toLinearMap (ExteriorAlgebra.map f))) (ExteriorAlgebra.ιMulti R n) = AlternatingMap.compLinearMap (ExteriorAlgebra.ιMulti R n) f

@[simp]

theorem ExteriorAlgebra.map_id {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] : ExteriorAlgebra.map LinearMap.id = AlgHom.id R (ExteriorAlgebra R M)

@[simp]

theorem ExteriorAlgebra.map_comp_map {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {N : Type u4} {N' : Type u5} [AddCommGroup N] [Module R N] [AddCommGroup N'] [Module R N'] (f : M →ₗ[R] N) (g : N →ₗ[R] N') : AlgHom.comp (ExteriorAlgebra.map g) (ExteriorAlgebra.map f) = ExteriorAlgebra.map (g ∘ₗ f)

@[simp]

theorem ExteriorAlgebra.ι_range_map_map {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {N : Type u4} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) : Submodule.map (AlgHom.toLinearMap (ExteriorAlgebra.map f)) (LinearMap.range (ExteriorAlgebra.ι R)) = Submodule.map (ExteriorAlgebra.ι R) (LinearMap.range f)

theorem ExteriorAlgebra.toTrivSqZeroExt_comp_map {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {N : Type u4} [AddCommGroup N] [Module R N] [Module Rᵐᵒᵖ M] [IsCentralScalar R M] [Module Rᵐᵒᵖ N] [IsCentralScalar R N] (f : M →ₗ[R] N) : AlgHom.comp ExteriorAlgebra.toTrivSqZeroExt (ExteriorAlgebra.map f) = AlgHom.comp (TrivSqZeroExt.map f) ExteriorAlgebra.toTrivSqZeroExt

theorem ExteriorAlgebra.ιInv_comp_map {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {N : Type u4} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) : ExteriorAlgebra.ιInv ∘ₗ AlgHom.toLinearMap (ExteriorAlgebra.map f) = f ∘ₗ ExteriorAlgebra.ιInv

@[simp]

theorem ExteriorAlgebra.leftInverse_map_iff {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {N : Type u4} [AddCommGroup N] [Module R N] {f : M →ₗ[R] N} {g : N →ₗ[R] M} : Function.LeftInverse ⇑(ExteriorAlgebra.map g) ⇑(ExteriorAlgebra.map f) ↔ Function.LeftInverse ⇑g ⇑f

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} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {N : Type u4} [AddCommGroup N] [Module R N] {f : M →ₗ[R] N} (hf : ∃ (g : N →ₗ[R] M), g ∘ₗ f = LinearMap.id) : Function.Injective ⇑(ExteriorAlgebra.map f)

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} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {N : Type u4} [AddCommGroup N] [Module R N] {f : M →ₗ[R] N} : Function.Surjective ⇑(ExteriorAlgebra.map f) ↔ Function.Surjective ⇑f

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} [Field K] [AddCommGroup E] [Module K E] [AddCommGroup F] [Module K F] {f : E →ₗ[K] F} (hf : LinearMap.ker f = ⊥) : Function.Injective ⇑(ExteriorAlgebra.map f)

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

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.

Equations

• TensorAlgebra.toExterior = (TensorAlgebra.lift R) (ExteriorAlgebra.ι R)

@[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