Action and trace formulas in exterior-power bases

A basis of a module induces a basis of each exterior power, indexed by subsets of the basis indices. An endomorphism diagonal in the original basis acts diagonally in this exterior-power basis, with eigenvalues given by products over the indexing subsets. Their sum is the trace.

A basis indexed by Fin n identifies the degree-n exterior power with the scalars by sending an exterior product to its determinant against that basis. The induced endomorphism acts by its determinant in this degree. These formulas hold over every commutative ring, including the zero ring. When the ring is nontrivial, n is the module's rank and this is its top exterior power.

Main definitions

• Module.Basis.exteriorPowerTopEquiv identifies the degree-n exterior power with the scalars for a basis indexed by Fin n.

Main results

• Module.Basis.map_exteriorPower_of_apply gives the eigenvalues in the exterior-power basis.
• Module.Basis.trace_map_exteriorPower_of_apply sums those eigenvalues to compute the trace.
• Module.Basis.exteriorPower_ιMulti_eq_det_smul expands a degree-n exterior product in terms of the wedge of a basis indexed by Fin n.
• Module.Basis.map_exteriorPower_top_eq_det_smul gives the degree-n action as its determinant for a basis indexed by Fin n.
• LinearMap.map_exteriorPower_finrank_eq_det_smul gives the action in degree Module.finrank as its determinant.
• Module.Basis.trace_map_exteriorPower_top gives the degree-n trace as the determinant for a basis indexed by Fin n.

References

The results use Mathlib's exterior-power basis from Mathlib.LinearAlgebra.ExteriorPower.Basis, by Sophie Morel and Daniel Morrison, and the determinant of a family against a basis from Mathlib.LinearAlgebra.Determinant.

theorem Module.Basis.map_exteriorPower_of_apply {R : Type u} {M : Type w} [CommRing R] {I : Type u_1} [LinearOrder I] [AddCommGroup M] [Module R M] (b : Basis I R M) (f : M →ₗ[R] M) (a : I → R) (hf : ∀ (i : I), f (b i) = a i • b i) (d : ℕ) (s : ↑(Set.powersetCard I d)) : (exteriorPower.map d f) ((exteriorPower d b) s) = (∏ i ∈ ↑s, a i) • (exteriorPower d b) s

An endomorphism diagonal in a basis is diagonal in the induced basis of the exterior power: the basis vector indexed by the d-element subset s is an eigenvector, with eigenvalue the product of the eigenvalues indexed by s. Summing those eigenvalues over all s gives the trace, Module.Basis.trace_map_exteriorPower_of_apply.

theorem Module.Basis.trace_map_exteriorPower_of_apply {R : Type u} {M : Type w} [CommRing R] {I : Type u_1} [Fintype I] [AddCommGroup M] [Module R M] (b : Basis I R M) (f : M →ₗ[R] M) (a : I → R) (d : ℕ) (hf : ∀ (i : I), f (b i) = a i • b i) : (LinearMap.trace R ↥(⋀[R]^d M)) (exteriorPower.map d f) = ∑ s : ↑(Set.powersetCard I d), ∏ i ∈ ↑s, a i

If an endomorphism is diagonal in a finite basis, then its trace on the dth exterior power is the dth elementary symmetric sum of its eigenvalues.

theorem Module.Basis.exteriorPower_ιMulti_eq_det_smul {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (b : Basis (Fin n) R M) (v : Fin n → M) : (exteriorPower.ιMulti R n) v = b.det v • (exteriorPower.ιMulti R n) ⇑b

Given a basis indexed by Fin n, an exterior product of n vectors is the determinant of that family against the basis, times the exterior product of the basis.

theorem Module.Basis.map_exteriorPower_top_eq_det_smul {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (b : Basis (Fin n) R M) (f : M →ₗ[R] M) : exteriorPower.map n f = LinearMap.det f • LinearMap.id

For a basis indexed by Fin n, an endomorphism acts on the degree-n exterior power as multiplication by its determinant.

@[simp]

theorem LinearMap.map_exteriorPower_finrank_eq_det_smul {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] (f : M →ₗ[R] M) : exteriorPower.map (Module.finrank R M) f = LinearMap.det f • id

The basis-free form of Module.Basis.map_exteriorPower_top_eq_det_smul: an endomorphism of a free module acts on the exterior power in degree Module.finrank R M by its determinant. For a nonfinite module over a nontrivial ring, this is the identity in degree zero.

noncomputable def Module.Basis.exteriorPowerTopEquiv {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (b : Basis (Fin n) R M) : ↥(⋀[R]^n M) ≃ₗ[R] R

A basis indexed by Fin n identifies the degree-n exterior power with the scalars by sending an exterior product of vectors to their determinant against the basis.

Equations

• b.exteriorPowerTopEquiv = LinearEquiv.ofLinearMap (exteriorPower.alternatingMapLinearEquiv b.det) (LinearMap.toSpanSingleton R (↥(⋀[R]^n M)) ((exteriorPower.ιMulti R n) ⇑b)) ⋯ ⋯

@[simp]

theorem Module.Basis.exteriorPowerTopEquiv_apply_ιMulti {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (b : Basis (Fin n) R M) (v : Fin n → M) : b.exteriorPowerTopEquiv ((exteriorPower.ιMulti R n) v) = b.det v

The identification for a basis indexed by Fin n sends an exterior product to its determinant against the basis.

@[simp]

theorem Module.Basis.exteriorPowerTopEquiv_symm_apply {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (b : Basis (Fin n) R M) (r : R) : b.exteriorPowerTopEquiv.symm r = r • (exteriorPower.ιMulti R n) ⇑b

The inverse identification sends a scalar to that multiple of the basis wedge.

theorem Module.Basis.trace_map_exteriorPower_top {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (b : Basis (Fin n) R M) (f : M →ₗ[R] M) : (LinearMap.trace R ↥(⋀[R]^n M)) (exteriorPower.map n f) = LinearMap.det f

For a basis indexed by Fin n, the trace of the induced endomorphism on the degree-n exterior power is the determinant.