Further results on exterior powers

This file records that the dth exterior power of a finite free module over a commutative ring vanishes as soon as d exceeds the rank of the module.

It then builds the surjection exteriorPower.fromTensorPower : ⨂[R]^n M →ₗ[R] ⋀[R]^n M that is left inverse, up to the factor n!, to Mathlib's antisymmetrization exteriorPower.toTensorPower: composing the antisymmetrization with it is n! • id on the exterior power, while composing the two the other way round is the antisymmetrization operator ∑_σ sgn(σ) σ on the tensor power. Consequently the antisymmetrization is injective once n! is a unit in the base ring, and its image is the image of that operator. That is the statement a Young symmetrizer of a one-column shape consumes.

Finally, it describes images of exterior powers under induced maps: inside the exterior algebra, the image of ⋀ⁿ M under f is the nth power of the degree-one image of f, and over a field an injective map embeds ⋀ⁿ V with its binomial dimension.

Main definitions

• exteriorPower.fromTensorPower is the canonical surjection of the tensor power onto the exterior power.

Main results

• exteriorPower.eq_zero_of_finrank_lt states that every element of ⋀[R]^d M is zero when Module.finrank R M < d.
• exteriorPower.fromTensorPower_comp_toTensorPower: antisymmetrizing and projecting back is multiplication by n!, whence exteriorPower.toTensorPower_injective.
• exteriorPower.toTensorPower_injective_of_free: antisymmetrization is injective for free modules in every characteristic, without factorial invertibility.
• exteriorPower.range_toTensorPower: the image of the antisymmetrization is the image of the antisymmetrization operator on the tensor power.
• exteriorPower.toTensorPower_comp_map and exteriorPower.map_comp_fromTensorPower: the antisymmetrization and the canonical surjection are natural in the module.
• TauCeti.ExteriorAlgebra.exteriorPower_map_map: the image of ⋀ⁿ M in the exterior algebra under the map induced by f is the nth power of the degree-one image of f.
• TauCeti.exteriorPower.finrank_range_map: over a field, the image of ⋀ⁿ V under the map induced by an injective linear map has dimension (dim V).choose n.

References

The results use Mathlib's exterior-power basis and dimension formula from Mathlib.LinearAlgebra.ExteriorPower.Basis, by Sophie Morel and Daniel Morrison.

theorem exteriorPower.eq_zero_of_finrank_lt {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (d : ℕ) (h : Module.finrank R M < d) (x : ↥(⋀[R]^d M)) : x = 0

An exterior power above the rank of a finite free module is zero.

Antisymmetrization of free modules

theorem exteriorPower.pairingDual_ιMulti_apply {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (g : Fin n → Module.Dual R M) (x : ↥(⋀[R]^n M)) : ((pairingDual R M n) ((ιMulti R n) g)) x = ((TensorPower.multilinearMapToDual R M n) g) ((toTensorPower R M n) x)

Pairing with a pure exterior product of linear forms factors through the antisymmetrization into the tensor power.

theorem exteriorPower.toTensorPower_injective_of_free {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] {n : ℕ} : Function.Injective ⇑(toTensorPower R M n)

Antisymmetrization embeds every exterior power of a free module into its tensor power, over any commutative ring, without requiring the factorial to be invertible.

The exterior power as a quotient of the tensor power

noncomputable def exteriorPower.fromTensorPower (R : Type u) (M : Type w) [CommRing R] [AddCommGroup M] [Module R M] (n : ℕ) : TensorPower R n M →ₗ[R] ↥(⋀[R]^n M)

The canonical surjection of the tensor power onto the exterior power, sending a pure tensor to the corresponding exterior product.

Mathlib's exteriorPower.toTensorPower runs the other way, by antisymmetrization; antisymmetrizing and then projecting back is n! on the exterior power, while projecting and then antisymmetrizing is the antisymmetrization operator ∑_σ sgn(σ) σ on the tensor power.

Equations

• exteriorPower.fromTensorPower R M n = PiTensorProduct.lift ↑(exteriorPower.ιMulti R n)

@[simp]

theorem exteriorPower.fromTensorPower_tprod {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (n : ℕ) (m : Fin n → M) : (fromTensorPower R M n) ((PiTensorProduct.tprod R) m) = (ιMulti R n) m

theorem exteriorPower.fromTensorPower_surjective {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (n : ℕ) : Function.Surjective ⇑(fromTensorPower R M n)

@[simp]

theorem exteriorPower.fromTensorPower_comp_toTensorPower {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (n : ℕ) : fromTensorPower R M n ∘ₗ toTensorPower R M n = n.factorial • LinearMap.id

Antisymmetrizing an exterior product and projecting it back multiplies by n!: each of the n! signed reorderings returns the same exterior product.

theorem exteriorPower.toTensorPower_injective {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (n : ℕ) (h : IsUnit ↑n.factorial) : Function.Injective ⇑(toTensorPower R M n)

The antisymmetrization is injective as soon as n! is a unit in the base ring, for instance over a ℚ-algebra.

theorem exteriorPower.toTensorPower_comp_fromTensorPower {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (n : ℕ) : toTensorPower R M n ∘ₗ fromTensorPower R M n = ∑ σ : Equiv.Perm (Fin n), ↑(Equiv.Perm.sign σ) • ↑(PiTensorProduct.reindex R (fun (x : Fin n) => M) σ)

Projecting a tensor to the exterior power and antisymmetrizing it back is the antisymmetrization operator ∑_σ sgn(σ) σ of the tensor power.

theorem exteriorPower.toTensorPower_comp_map {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (n : ℕ) {N : Type u_1} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) : toTensorPower R N n ∘ₗ map n f = (PiTensorProduct.map fun (x : Fin n) => f) ∘ₗ toTensorPower R M n

The antisymmetrization is natural in the module.

theorem exteriorPower.map_comp_fromTensorPower {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (n : ℕ) {N : Type u_1} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) : map n f ∘ₗ fromTensorPower R M n = fromTensorPower R N n ∘ₗ PiTensorProduct.map fun (x : Fin n) => f

The canonical surjection is natural in the module.

theorem exteriorPower.range_toTensorPower {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (n : ℕ) : (toTensorPower R M n).range = (∑ σ : Equiv.Perm (Fin n), ↑(Equiv.Perm.sign σ) • ↑(PiTensorProduct.reindex R (fun (x : Fin n) => M) σ)).range

The image of the antisymmetrization is the image of the antisymmetrization operator ∑_σ sgn(σ) σ on the tensor power.

theorem TauCeti.ExteriorAlgebra.exteriorPower_map_map {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {N : Type u_1} [AddCommGroup N] [Module R N] (n : ℕ) (f : M →ₗ[R] N) : Submodule.map (ExteriorAlgebra.map f).toLinearMap (⋀[R]^n M) = Submodule.map (ExteriorAlgebra.ι R) f.range ^ n

Inside the exterior algebra, the image of the nth exterior power under the map induced by f is the nth power of the degree-one image of the range of f.

theorem TauCeti.exteriorPower.finrank_range_map {K : Type u_1} [Field K] {V : Type u_2} {W : Type u_3} [AddCommGroup V] [Module K V] [Module.Finite K V] [AddCommGroup W] [Module K W] {f : V →ₗ[K] W} (hf : Function.Injective ⇑f) (n : ℕ) : Module.finrank K ↥(exteriorPower.map n f).range = (Module.finrank K V).choose n

Over a field, the image of the nth exterior power of a finite-dimensional space under the map induced by an injective linear map has dimension (dim V).choose n.