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.

• exteriorPower.map n f : ⋀[R]^n M →ₗ[R] ⋀[R]^n N is the linear map on nth exterior powers induced by a linear map f : M →ₗ[R] N. (See the file Algebra.Category.ModuleCat.ExteriorPower for the corresponding functor ModuleCat R ⥤ ModuleCat R.)

Theorems

• exteriorPower.ι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) : ↑((ιMulti R n) a) = (ExteriorAlgebra.ιMulti R n) a

noncomputable def exteriorPower.ιMulti_family (R : Type u) [CommRing R] (n : ℕ) {M : Type u_1} [AddCommGroup M] [Module R M] {I : Type u_4} [LinearOrder I] (v : I → M) (s : { s : Finset I // s.card = n }) : ↥(⋀[R]^n 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 nth exterior power.

Equations

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

@[simp]

theorem exteriorPower.ιMulti_family_apply_coe (R : Type u) [CommRing R] (n : ℕ) {M : Type u_1} [AddCommGroup M] [Module R M] {I : Type u_4} [LinearOrder I] (v : I → M) (s : { s : Finset I // s.card = n }) : ↑(ιMulti_family R n v s) = ExteriorAlgebra.ιMulti_family R n v s

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 ⇑(ι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) : Rels R ι M
• smul {R : Type u} {ι : Type u_4} {M : Type u_5} (m : ι → M) (i : ι) (r : R) (x : M) : 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) : 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] : (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] : (relations R ι M).R = 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] (x✝ : Rels R ι M) : (relations R ι M).relation x✝ = match x✝ with | 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 | Rels.smul m i r x => Finsupp.single (Function.update m i (r • x)) 1 - r • Finsupp.single (Function.update m i x) 1 | Rels.alt m i j hm hij => Finsupp.single m 1

noncomputable 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] : (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_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 : (relations R ι M).G) : (relationsSolutionEquiv.symm f).var m = f m

@[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 : (relations R ι M).Solution N) (m : ι → M) : (relationsSolutionEquiv s) m = s.var m

noncomputable def exteriorPower.presentation.isPresentationCore (R : Type u) [CommRing R] (n : ℕ) (M : Type u_1) [AddCommGroup M] [Module R M] : (relationsSolutionEquiv.symm (ι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_R (R : Type u) [CommRing R] (n : ℕ) (M : Type u_1) [AddCommGroup M] [Module R M] : (presentation R n M).R = presentation.Rels R (Fin n) M

@[simp]

theorem exteriorPower.presentation_G (R : Type u) [CommRing R] (n : ℕ) (M : Type u_1) [AddCommGroup M] [Module R M] : (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] (x✝ : presentation.Rels R (Fin n) M) : (presentation R n M).relation x✝ = match x✝ with | 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 | presentation.Rels.smul m i r x => Finsupp.single (Function.update m i (r • x)) 1 - Finsupp.single (Function.update m i x) r | presentation.Rels.alt m i j hm hij => Finsupp.single m 1

@[simp]

theorem exteriorPower.presentation_var (R : Type u) [CommRing R] (n : ℕ) (M : Type u_1) [AddCommGroup M] [Module R M] (m : (presentation.relations R (Fin n) M).G) : (presentation R n M).var m = (ι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 (ιMulti R n) = g.compAlternatingMap (ιMulti R n)) : f = g

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

theorem exteriorPower.linearMap_ext_iff {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} : f = g ↔ f.compAlternatingMap (ιMulti R n) = g.compAlternatingMap (ιMulti R n)

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) : (alternatingMapLinearEquiv f).compAlternatingMap (ι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) : (alternatingMapLinearEquiv f) ((ι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) : (alternatingMapLinearEquiv.symm F) m = (F.compAlternatingMap (ιMulti R n)) m

@[simp]

theorem exteriorPower.alternatingMapLinearEquiv_ιMulti {R : Type u} [CommRing R] {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module R M] : alternatingMapLinearEquiv (ι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) : alternatingMapLinearEquiv (g.compAlternatingMap f) = g ∘ₗ 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.

Functoriality of the exterior powers.

noncomputable def exteriorPower.map {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 →ₗ[R] N) : ↥(⋀[R]^n M) →ₗ[R] ↥(⋀[R]^n N)

The linear map between nth exterior powers induced by a linear map between the modules.

Equations

• exteriorPower.map n f = exteriorPower.alternatingMapLinearEquiv ((exteriorPower.ιMulti R n).compLinearMap f)

@[simp]

theorem exteriorPower.alternatingMapLinearEquiv_symm_map {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 →ₗ[R] N) : alternatingMapLinearEquiv.symm (map n f) = (ιMulti R n).compLinearMap f

@[simp]

theorem exteriorPower.map_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 →ₗ[R] N) : (map n f).compAlternatingMap (ιMulti R n) = (ιMulti R n).compLinearMap f

@[simp]

theorem exteriorPower.map_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 →ₗ[R] N) (m : Fin n → M) : (map n f) ((ιMulti R n) m) = (ιMulti R n) (⇑f ∘ m)

@[simp]

theorem exteriorPower.map_comp_ιMulti_family {R : Type u} [CommRing R] {n : ℕ} {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {I : Type u_4} [LinearOrder I] (v : I → M) (f : M →ₗ[R] N) : ⇑(map n f) ∘ ιMulti_family R n v = ιMulti_family R n (⇑f ∘ v)

@[simp]

theorem exteriorPower.map_apply_ιMulti_family {R : Type u} [CommRing R] {n : ℕ} {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {I : Type u_4} [LinearOrder I] (v : I → M) (f : M →ₗ[R] N) (s : { s : Finset I // s.card = n }) : (map n f) (ιMulti_family R n v s) = ιMulti_family R n (⇑f ∘ v) s

@[simp]

theorem exteriorPower.map_id {R : Type u} [CommRing R] {n : ℕ} {M : Type u_1} [AddCommGroup M] [Module R M] : map n LinearMap.id = LinearMap.id

@[simp]

theorem exteriorPower.map_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'] (f : M →ₗ[R] N) (g : N →ₗ[R] N') : map n (g ∘ₗ f) = map n g ∘ₗ map n f

Linear equivalences in degrees 0 and 1.

noncomputable def exteriorPower.zeroEquiv (R : Type u) [CommRing R] (M : Type u_1) [AddCommGroup M] [Module R M] : ↥(⋀[R]^0 M) ≃ₗ[R] R

The linear equivalence ⋀[R]^0 M ≃ₗ[R] R.

Equations

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

theorem exteriorPower.zeroEquiv_symm_apply (R : Type u) [CommRing R] (M : Type u_1) [AddCommGroup M] [Module R M] (a : R) : (zeroEquiv R M).symm a = a • (ιMulti R 0) fun (a : Fin 0) => ⋯.elim

@[simp]

theorem exteriorPower.zeroEquiv_ιMulti {R : Type u} [CommRing R] {M : Type u_1} [AddCommGroup M] [Module R M] (f : Fin 0 → M) : (zeroEquiv R M) ((ιMulti R 0) f) = 1

theorem exteriorPower.zeroEquiv_naturality {R : Type u} [CommRing R] {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) : ↑(zeroEquiv R N) ∘ₗ map 0 f = ↑(zeroEquiv R M)

noncomputable def exteriorPower.oneEquiv (R : Type u) [CommRing R] (M : Type u_1) [AddCommGroup M] [Module R M] : ↥(⋀[R]^1 M) ≃ₗ[R] M

The linear equivalence M ≃ₗ[R] ⋀[R]^1 M.

Equations

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

theorem exteriorPower.oneEquiv_symm_apply (R : Type u) [CommRing R] (M : Type u_1) [AddCommGroup M] [Module R M] (a : M) : (oneEquiv R M).symm a = (ιMulti R 1) fun (x : Fin 1) => a

@[simp]

theorem exteriorPower.oneEquiv_ιMulti {R : Type u} [CommRing R] {M : Type u_1} [AddCommGroup M] [Module R M] (f : Fin 1 → M) : (oneEquiv R M) ((ιMulti R 1) f) = f 0

theorem exteriorPower.oneEquiv_naturality {R : Type u} [CommRing R] {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) : ↑(oneEquiv R N) ∘ₗ map 1 f = f ∘ₗ ↑(oneEquiv R M)