Exterior powers

We study the exterior powers of a module M over a commutative ring R.

Definitions

• exteriorPower.ιMulti is the canonical alternating map on M with values in ⋀[R]^n M.

• exteriorPower.presentation R n M is the standard presentation of the R-module ⋀[R]^n M.

Theorems

• ιMulti_span: The image of exteriorPower.ιMulti spans ⋀[R]^n M.

• We construct exteriorPower.alternatingMapLinearEquiv which expresses the universal property of the exterior power as a linear equivalence (M [⋀^Fin n]→ₗ[R] N) ≃ₗ[R] ⋀[R]^n M →ₗ[R] N between alternating maps and linear maps from the exterior power.

The canonical alternating map from Fin n → M to ⋀[R]^n M.

def exteriorPower.ιMulti (R : Type u) [CommRing R] (n : ℕ) {M : Type u_1} [AddCommGroup M] [Module R M] : M [⋀^Fin n]→ₗ[R] ↥(⋀[R]^n M)

exteriorAlgebra.ιMulti is the alternating map from Fin n → M to ⋀[r]^n M induced by exteriorAlgebra.ιMulti, i.e. sending a family of vectors m : Fin n → M to the product of its entries.

Equations

• exteriorPower.ιMulti R n = (ExteriorAlgebra.ιMulti R n).codRestrict (⋀[R]^n M) ⋯

@[simp]

theorem exteriorPower.ιMulti_apply_coe (R : Type u) [CommRing R] (n : ℕ) {M : Type u_1} [AddCommGroup M] [Module R M] (a : Fin n → M) : ↑((exteriorPower.ιMulti R n) a) = (ExteriorAlgebra.ιMulti R n) a

theorem exteriorPower.ιMulti_span_fixedDegree (R : Type u) [CommRing R] (n : ℕ) (M : Type u_1) [AddCommGroup M] [Module R M] : Submodule.span R (Set.range ⇑(ExteriorAlgebra.ιMulti R n)) = ⋀[R]^n M

The image of ExteriorAlgebra.ιMulti R n spans the nth exterior power. Variant of ExteriorAlgebra.ιMulti_span_fixedDegree, useful in rewrites.

theorem exteriorPower.ιMulti_span (R : Type u) [CommRing R] (n : ℕ) (M : Type u_1) [AddCommGroup M] [Module R M] : Submodule.span R (Set.range ⇑(exteriorPower.ιMulti R n)) = ⊤

The image of exteriorPower.ιMulti spans ⋀[R]^n M.

inductive exteriorPower.presentation.Rels (R : Type u) (ι : Type u_4) (M : Type u_5) : Type (max (max u u_4) u_5)

The index type for the relations in the standard presentation of ⋀[R]^n M, in the particular case ι is Fin n.

• add {R : Type u} {ι : Type u_4} {M : Type u_5} (m : ι → M) (i : ι) (x y : M) : exteriorPower.presentation.Rels R ι M
• smul {R : Type u} {ι : Type u_4} {M : Type u_5} (m : ι → M) (i : ι) (r : R) (x : M) : exteriorPower.presentation.Rels R ι M
• alt {R : Type u} {ι : Type u_4} {M : Type u_5} (m : ι → M) (i j : ι) (hm : m i = m j) (hij : i ≠ j) : exteriorPower.presentation.Rels R ι M

noncomputable def exteriorPower.presentation.relations (R : Type u) [CommRing R] (ι : Type u_4) [DecidableEq ι] (M : Type u_5) [AddCommGroup M] [Module R M] : Module.Relations R

The relations in the standard presentation of ⋀[R]^n M with generators and relations.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem exteriorPower.presentation.relations_G (R : Type u) [CommRing R] (ι : Type u_4) [DecidableEq ι] (M : Type u_5) [AddCommGroup M] [Module R M] : (exteriorPower.presentation.relations R ι M).G = (ι → M)

@[simp]

theorem exteriorPower.presentation.relations_R (R : Type u) [CommRing R] (ι : Type u_4) [DecidableEq ι] (M : Type u_5) [AddCommGroup M] [Module R M] : (exteriorPower.presentation.relations R ι M).R = exteriorPower.presentation.Rels R ι M

@[simp]

theorem exteriorPower.presentation.relations_relation (R : Type u) [CommRing R] (ι : Type u_4) [DecidableEq ι] (M : Type u_5) [AddCommGroup M] [Module R M] (r : exteriorPower.presentation.Rels R ι M) : (exteriorPower.presentation.relations R ι M).relation r = match r with | exteriorPower.presentation.Rels.add m i x y => Finsupp.single (Function.update m i x) 1 + Finsupp.single (Function.update m i y) 1 - Finsupp.single (Function.update m i (x + y)) 1 | exteriorPower.presentation.Rels.smul m i r x => Finsupp.single (Function.update m i (r • x)) 1 - r • Finsupp.single (Function.update m i x) 1 | exteriorPower.presentation.Rels.alt m i j hm hij => Finsupp.single m 1

def exteriorPower.presentation.relationsSolutionEquiv {R : Type u} [CommRing R] {N : Type u_2} [AddCommGroup N] [Module R N] {ι : Type u_4} [DecidableEq ι] {M : Type u_5} [AddCommGroup M] [Module R M] : (exteriorPower.presentation.relations R ι M).Solution N ≃ M [⋀^ι]→ₗ[R] N

The solutions in a module N to the linear equations given by exteriorPower.relations R ι M identify to alternating maps to N.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem exteriorPower.presentation.relationsSolutionEquiv_apply_apply {R : Type u} [CommRing R] {N : Type u_2} [AddCommGroup N] [Module R N] {ι : Type u_4} [DecidableEq ι] {M : Type u_5} [AddCommGroup M] [Module R M] (s : (exteriorPower.presentation.relations R ι M).Solution N) (m : ι → M) : (exteriorPower.presentation.relationsSolutionEquiv s) m = s.var m

@[simp]

theorem exteriorPower.presentation.relationsSolutionEquiv_symm_apply_var {R : Type u} [CommRing R] {N : Type u_2} [AddCommGroup N] [Module R N] {ι : Type u_4} [DecidableEq ι] {M : Type u_5} [AddCommGroup M] [Module R M] (f : M [⋀^ι]→ₗ[R] N) (m : (exteriorPower.presentation.relations R ι M).G) : (exteriorPower.presentation.relationsSolutionEquiv.symm f).var m = f m

def exteriorPower.presentation.isPresentationCore (R : Type u) [CommRing R] (n : ℕ) (M : Type u_1) [AddCommGroup M] [Module R M] : (exteriorPower.presentation.relationsSolutionEquiv.symm (exteriorPower.ιMulti R n)).IsPresentationCore

The universal property of the exterior power.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def exteriorPower.presentation (R : Type u) [CommRing R] (n : ℕ) (M : Type u_1) [AddCommGroup M] [Module R M] : Module.Presentation R ↥(⋀[R]^n M)

The standard presentation of the R-module ⋀[R]^n M.

Equations

• exteriorPower.presentation R n M = Module.Presentation.ofIsPresentation ⋯

@[simp]

theorem exteriorPower.presentation_G (R : Type u) [CommRing R] (n : ℕ) (M : Type u_1) [AddCommGroup M] [Module R M] : (exteriorPower.presentation R n M).G = (Fin n → M)

@[simp]

theorem exteriorPower.presentation_relation (R : Type u) [CommRing R] (n : ℕ) (M : Type u_1) [AddCommGroup M] [Module R M] (r : (exteriorPower.presentation.relations R (Fin n) M).R) : (exteriorPower.presentation R n M).relation r = match r with | exteriorPower.presentation.Rels.add m i x y => Finsupp.single (Function.update m i x) 1 + Finsupp.single (Function.update m i y) 1 - Finsupp.single (Function.update m i (x + y)) 1 | exteriorPower.presentation.Rels.smul m i r x => Finsupp.single (Function.update m i (r • x)) 1 - Finsupp.single (Function.update m i x) r | exteriorPower.presentation.Rels.alt m i j hm hij => Finsupp.single m 1

@[simp]

theorem exteriorPower.presentation_R (R : Type u) [CommRing R] (n : ℕ) (M : Type u_1) [AddCommGroup M] [Module R M] : (exteriorPower.presentation R n M).R = exteriorPower.presentation.Rels R (Fin n) M

@[simp]

theorem exteriorPower.presentation_var (R : Type u) [CommRing R] (n : ℕ) (M : Type u_1) [AddCommGroup M] [Module R M] (m : (exteriorPower.presentation.relations R (Fin n) M).G) : (exteriorPower.presentation R n M).var m = (exteriorPower.ιMulti R n) m

theorem exteriorPower.linearMap_ext {R : Type u} [CommRing R] {n : ℕ} {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {f g : ↥(⋀[R]^n M) →ₗ[R] N} (heq : f.compAlternatingMap (exteriorPower.ιMulti R n) = g.compAlternatingMap (exteriorPower.ιMulti R n)) : f = g

Two linear maps on ⋀[R]^n M that agree on the image of exteriorPower.ιMulti are equal.

noncomputable def exteriorPower.alternatingMapLinearEquiv {R : Type u} [CommRing R] {n : ℕ} {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : M [⋀^Fin n]→ₗ[R] N ≃ₗ[R] ↥(⋀[R]^n M) →ₗ[R] N

The linear equivalence between n-fold alternating maps from M to N and linear maps from ⋀[R]^n M to N: this is the universal property of the nth exterior power of M.

Equations

• exteriorPower.alternatingMapLinearEquiv = ((⋯.linearMapEquiv.trans exteriorPower.presentation.relationsSolutionEquiv).toLinearEquiv ⋯).symm

@[simp]

theorem exteriorPower.alternatingMapLinearEquiv_comp_ιMulti {R : Type u} [CommRing R] {n : ℕ} {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M [⋀^Fin n]→ₗ[R] N) : (exteriorPower.alternatingMapLinearEquiv f).compAlternatingMap (exteriorPower.ιMulti R n) = f

@[simp]

theorem exteriorPower.alternatingMapLinearEquiv_apply_ιMulti {R : Type u} [CommRing R] {n : ℕ} {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M [⋀^Fin n]→ₗ[R] N) (a : Fin n → M) : (exteriorPower.alternatingMapLinearEquiv f) ((exteriorPower.ιMulti R n) a) = f a

@[simp]

theorem exteriorPower.alternatingMapLinearEquiv_symm_apply {R : Type u} [CommRing R] {n : ℕ} {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (F : ↥(⋀[R]^n M) →ₗ[R] N) (m : Fin n → M) : (exteriorPower.alternatingMapLinearEquiv.symm F) m = (F.compAlternatingMap (exteriorPower.ιMulti R n)) m

@[simp]

theorem exteriorPower.alternatingMapLinearEquiv_ιMulti {R : Type u} [CommRing R] {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module R M] : exteriorPower.alternatingMapLinearEquiv (exteriorPower.ιMulti R n) = LinearMap.id

theorem exteriorPower.alternatingMapLinearEquiv_comp {R : Type u} [CommRing R] {n : ℕ} {M : Type u_1} {N : Type u_2} {N' : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup N'] [Module R N'] (g : N →ₗ[R] N') (f : M [⋀^Fin n]→ₗ[R] N) : exteriorPower.alternatingMapLinearEquiv (g.compAlternatingMap f) = g ∘ₗ exteriorPower.alternatingMapLinearEquiv f

If f is an alternating map from M to N, alternatingMapLinearEquiv f is the corresponding linear map from ⋀[R]^n M to N, and if g is a linear map from N to N', then the alternating map g.compAlternatingMap f from M to N' corresponds to the linear map g.comp (alternatingMapLinearEquiv f) on ⋀[R]^n M.