Exterior powers of the standard general-linear module

The infinitesimal exterior-power action restricts along the matrix-to-endomorphism equivalence to an action of a general linear Lie algebra. A matrix unit acts on the wedge of the standard basis vectors indexed by a finite set S of coordinates in a way read off from S: the diagonal unit Eᵢᵢ scales it by one or by zero according as i lies in S, and Eᵢⱼ with i ≠ j annihilates it whenever S contains i as soon as it contains j. Over a nontrivial ring, for d ≤ n, this makes the wedge of the first d standard basis vectors in Kⁿ a highest-weight vector.

Main definitions

• exteriorPower.glLieMap: the action of matrices on an exterior power.
• exteriorPower.basisWedge: the wedge of the standard basis vectors indexed by a finite set of coordinates.
• exteriorPower.firstBasisWedge: the wedge of the first standard basis vectors.
• exteriorPower.fundamentalWeight: the first-d coordinate-indicator weight.

Main results

• exteriorPower.lie_single_self_basisWedge and exteriorPower.lie_single_basisWedge_eq_zero_of_ne_of_mem_imp_mem: how a matrix unit acts on the wedge of a set of standard basis vectors.
• exteriorPower.isGlHighestWeightVector_firstBasisWedge: over a nontrivial ring, the first basis wedge is a highest-weight vector when d ≤ n.

Roadmap context

The highest-weight roadmap uses these exterior modules in two places: Layer 9 constructs the fundamental gl_n modules, while Layer 8 uses the sl₉ action on ⋀³(K⁹) in the Vinberg model of E₈.

noncomputable def exteriorPower.glLieMap {K : Type u_1} [CommRing K] (d : ℕ) {n : Type u_2} [DecidableEq n] [Fintype n] : Matrix n n K →ₗ⁅K⁆ Module.End K ↥(⋀[K]^d (n → K))

The natural matrix action on an exterior power of the standard module.

Equations

• exteriorPower.glLieMap d = (exteriorPower.lieMap d).comp lieEquivMatrix'.symm.toLieHom

@[simp]

theorem exteriorPower.glLieMap_apply_ιMulti {K : Type u_1} [CommRing K] (d : ℕ) {n : Type u_2} [DecidableEq n] [Fintype n] (A : Matrix n n K) (v : Fin d → n → K) : ((glLieMap d) A) ((ιMulti K d) v) = ∑ i : Fin d, (ιMulti K d) (Function.update v i (A.mulVec (v i)))

A matrix acts on a decomposable wedge by acting on one factor at a time.

@[instance_reducible]

noncomputable def exteriorPower.glLieRingModule {K : Type u_1} [CommRing K] (d : ℕ) {n : Type u_2} [DecidableEq n] [Fintype n] : LieRingModule (Matrix n n K) ↥(⋀[K]^d (n → K))

The Lie-ring module structure on an exterior power induced by the standard matrix action.

Equations

• exteriorPower.glLieRingModule d = LieRingModule.compLieHom (↥(⋀[K]^d (n → K))) (exteriorPower.glLieMap d)

theorem exteriorPower.glLieModule {K : Type u_1} [CommRing K] (d : ℕ) {n : Type u_2} [DecidableEq n] [Fintype n] : LieModule K (Matrix n n K) ↥(⋀[K]^d (n → K))

The Lie-module structure on an exterior power induced by the standard matrix action.

theorem exteriorPower.gl_lie_def {K : Type u_1} [CommRing K] (d : ℕ) {n : Type u_2} [DecidableEq n] [Fintype n] (A : Matrix n n K) (x : ↥(⋀[K]^d (n → K))) : ⁅A, x⁆ = ((glLieMap d) A) x

The scoped Lie action is the action represented by glLieMap.

noncomputable def exteriorPower.basisWedge (K : Type u_1) [CommRing K] {n : Type u_2} [Fintype n] [LinearOrder n] {N : ℕ} (S : Finset n) (h : S.card = N) : ↥(⋀[K]^N (n → K))

The wedge of the standard basis vectors of n → K indexed by a finite set S of coordinates, an element of the exterior power of degree the size of S. The factors are wedged together in the order S inherits from n.

Equations

• exteriorPower.basisWedge K S h = exteriorPower.ιMulti_family K N ⇑(Pi.basisFun K n) ⟨S, h⟩

theorem exteriorPower.basisWedge_eq_ιMulti_family {K : Type u_1} [CommRing K] {n : Type u_2} [Fintype n] [LinearOrder n] {N : ℕ} (S : Finset n) (h : S.card = N) : basisWedge K S h = ιMulti_family K N ⇑(Pi.basisFun K n) ⟨S, h⟩

The wedge of a set of basis vectors is the member of the standard basis of the exterior power that the set indexes.

theorem exteriorPower.basisWedge_eq_ιMulti {K : Type u_1} [CommRing K] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {N : ℕ} (S : Finset n) (h : S.card = N) : basisWedge K S h = (ιMulti K N) fun (k : Fin N) => Pi.single ((S.orderEmbOfFin h) k) 1

The wedge of a set of basis vectors, written as an exterior product.

theorem exteriorPower.basisWedge_ne_zero {K : Type u_1} [CommRing K] {n : Type u_2} [Fintype n] [LinearOrder n] {N : ℕ} [Nontrivial K] (S : Finset n) (h : S.card = N) : basisWedge K S h ≠ 0

The wedge of a set of basis vectors is nonzero.

@[simp]

theorem exteriorPower.lie_single_self_basisWedge {K : Type u_1} [CommRing K] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {N : ℕ} (S : Finset n) (h : S.card = N) (i : n) : ⁅Matrix.single i i 1, basisWedge K S h⁆ = (if i ∈ S then 1 else 0) • basisWedge K S h

The diagonal matrix unit Eᵢᵢ fixes the factors of a wedge of standard basis vectors that lie in direction i and kills the others, so it scales the wedge by one when i is one of its indices and annihilates it otherwise.

theorem exteriorPower.lie_single_basisWedge_eq_zero_of_ne_of_mem_imp_mem {K : Type u_1} [CommRing K] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {N : ℕ} (S : Finset n) (h : S.card = N) {i j : n} (hij : i ≠ j) (hS : j ∈ S → i ∈ S) : ⁅Matrix.single i j 1, basisWedge K S h⁆ = 0

A matrix unit Eᵢⱼ with i ≠ j annihilates the wedge of the standard basis vectors indexed by S, as soon as S contains i whenever it contains j: the j-th factor is carried to a factor already present, so every summand of the Leibniz expansion has a repeated factor.

noncomputable def exteriorPower.firstBasisWedge {K : Type u_1} [CommRing K] (d n : ℕ) (h : d ≤ n) : ↥(⋀[K]^d (Fin n → K))

The wedge of the first d standard basis vectors of K^n.

Equations

• exteriorPower.firstBasisWedge d n h = exteriorPower.ιMulti_family K d (⇑(Pi.basisFun K (Fin n))) (exteriorPower.firstBasisSet✝ d n h)

@[simp]

theorem exteriorPower.firstBasisWedge_eq_ιMulti {K : Type u_1} [CommRing K] (d n : ℕ) (h : d ≤ n) : firstBasisWedge d n h = (ιMulti K d) fun (i : Fin d) => Pi.single (Fin.castLE h i) 1

The first basis wedge written as an exterior product of standard basis vectors.

def exteriorPower.fundamentalWeight {K : Type u_1} [Zero K] [One K] (d n : ℕ) : Fin n → K

The tuple that is 1 on the first d coordinates and 0 afterward. When d ≤ n, this is the weight of the first basis wedge in the d-th exterior power of the standard gl_n module.

Equations

• exteriorPower.fundamentalWeight d n j = if ↑j < d then 1 else 0

@[simp]

theorem exteriorPower.fundamentalWeight_apply {K : Type u_1} [Zero K] [One K] (d n : ℕ) (j : Fin n) : fundamentalWeight d n j = if ↑j < d then 1 else 0

The fundamental exterior weight is 1 on the first d coordinates and 0 afterward.

theorem exteriorPower.isGlDominantIntegral_fundamentalWeight {K : Type u_1} [CommRing K] [CharZero K] (d n : ℕ) : TauCeti.IsGlDominantIntegral (fundamentalWeight d n)

The fundamental exterior weight is dominant integral in characteristic zero.

theorem exteriorPower.firstBasisWedge_ne_zero {K : Type u_1} [CommRing K] [Nontrivial K] (d n : ℕ) (h : d ≤ n) : firstBasisWedge d n h ≠ 0

The first basis wedge is nonzero.

theorem exteriorPower.isGlHighestWeightVector_firstBasisWedge {K : Type u_1} [CommRing K] [Nontrivial K] (d n : ℕ) (h : d ≤ n) : TauCeti.IsGlHighestWeightVector (fundamentalWeight d n) (firstBasisWedge d n h)

Over a nontrivial ring, the first basis wedge is a highest-weight vector for the exterior-power action when d ≤ n.