Top exterior powers

This file records the ordinary linear-algebra models for top exterior powers used by determinant constructions.

@[reducible, inline]

abbrev Module.topExteriorPower (R : Type u) [CommRing R] (n : ℕ) : Submodule R (ExteriorAlgebra R (Fin n → R))

The algebraic local model for the determinant of a free rank-n module.

Equations

• Module.topExteriorPower R n = ⋀[R]^n (Fin n → R)

theorem Module.finrank_topExteriorPower (R : Type u) [CommRing R] [Nontrivial R] (n : ℕ) : finrank R ↥(topExteriorPower R n) = 1

The top exterior power of a free rank-n module has rank one.

def Module.topPowerset (n : ℕ) : ↑(Set.powersetCard (ULift.{u, 0} (Fin n)) n)

The unique n-element powerset of ULift (Fin n) used by the free-module model.

Equations

• Module.topPowerset n = ⟨Finset.univ, ⋯⟩

noncomputable def Module.topExteriorFreeEquiv (R : Type u) [CommRing R] (n : ℕ) : ↥(⋀[R]^n (ULift.{u, 0} (Fin n) →₀ R)) ≃ₗ[R] R

The top exterior power of a free rank-n module is the coefficient ring.

Equations

• Module.topExteriorFreeEquiv R n = (Module.Basis.exteriorPower n Finsupp.basisSingleOne).repr.trans (Finsupp.uniqueLinearEquiv R R default)

theorem Module.topExteriorFreeEquiv_ιMulti (R : Type u) [CommRing R] (n : ℕ) (x : Fin n → ULift.{u, 0} (Fin n) →₀ R) : (topExteriorFreeEquiv R n) ((exteriorPower.ιMulti R n) x) = (Matrix.of fun (i j : Fin n) => (x i) ((Set.powersetCard.ofFinEmbEquiv.symm (topPowerset n)) j)).det