The trace twist of a gl n-module, and every dominant weight as a highest weight

Dominance for gl n constrains only the consecutive differences of a weight (TauCeti.IsGlDominantIntegral), so the dominant weights are the antitone tuples of natural numbers translated along the central direction μ ↦ μ + c · (1, …, 1), with c a free scalar. TauCeti.exists_isGlHighestWeightVector_natCast realizes the natural-number weights as highest weights inside exterior powers; this file supplies the central direction and, with it, every dominant weight.

The twist

The trace is a Lie character of gl n: it is linear and kills every commutator (LieAlgebra.matrix_trace_commutator_zero). So for a scalar c and a gl n-module M the formula

⁅A, m⁆' = ⁅A, m⁆ + c · tr(A) · m

is again a gl n-module structure on the underlying R-module of M. It is carried by TauCeti.GlTraceTwist n c M, a copy of M with the same R-module structure and the displayed bracket; TauCeti.GlTraceTwist.linearEquiv is that identification of the underlying R-modules, and TauCeti.GlTraceTwist.ofTwist_lie is the defining equation of the bracket.

Since tr(Eᵢᵢ) = 1 and tr(Eᵢⱼ) = 0 for i ≠ j, twisting shifts the weight of a highest weight vector by c in every coordinate and changes nothing else (TauCeti.isGlHighestWeightVector_toTwist). No invertibility of the size of the matrices is needed: the shift is read off the diagonal matrix units, not off the identity matrix.

Every dominant weight is a highest weight

A dominant weight μ : Fin N → R is a + c for an antitone a : Fin N → ℕ and a scalar c, by TauCeti.IsGlDominantIntegral.exists_antitone_natCast_add_const in TauCeti/Algebra/Lie/GeneralLinear/HighestWeight.lean. Twisting the exterior-power realization of a by c then realizes μ, which is TauCeti.exists_isGlHighestWeightVector_of_isGlDominantIntegral. The realizing module TauCeti.glTraceTwistedYoungWedge is finite over R, hence finite-dimensional over a field.

Main definitions

• TauCeti.GlTraceTwist: a gl n-module twisted by the character c · tr.
• TauCeti.GlTraceTwist.linearEquiv: the underlying R-modules of a module and of its twist.
• TauCeti.glTraceTwistedYoungWedge: the trace twist by c of the exterior power in which TauCeti.exists_isGlHighestWeightVector_natCast realizes a tuple a of natural numbers; for an antitone a it carries a highest weight vector of the dominant weight a + c · (1, …, 1).
• TauCeti.glTraceTwistedYoungWedge.linearEquiv: the underlying R-module of that carrier is the exterior power it twists.

Main results

• TauCeti.GlTraceTwist.ofTwist_lie: the defining equation of the twisted bracket.
• TauCeti.isGlHighestWeightVector_toTwist_iff and its introduction half TauCeti.isGlHighestWeightVector_toTwist: twisting by c shifts the weight of a highest weight vector by c in every coordinate, and nothing else; TauCeti.glTraceTwistedYoungWedge.isGlHighestWeightVector_linearEquiv_symm is that introduction rule for the named carrier.
• TauCeti.exists_isGlHighestWeightVector_of_isGlDominantIntegral: every dominant weight of gl N is the highest weight of a highest weight vector in a module finite over R.

Implementation notes

Twisting by the trace loses no generality. A Lie character of gl ι in the sense of LieAlgebra.LieCharacter vanishes on the derived ideal (LieAlgebra.lieCharacter_apply_of_mem_derived), which is the trace-zero ideal (TauCeti.derivedSeries_one_eq_slIdeal); since a matrix differs from a multiple of a single diagonal matrix unit by a trace-zero matrix, every character of gl ι is c · tr for a nonempty ι. So the scalar c is a coordinate on the characters, and the twist below is the twist by an arbitrary one.

TauCeti.GlTraceTwist is a one-field structure rather than a bare type synonym, so that the twisting data ι and c are honest parameters of the carrier; the module structures are transported along the resulting equivalence. This is the pattern of Mathlib's WithLp, which carries a phantom exponent in the same way.

Roadmap context

Layer 9 of the highest weight roadmap asks for a finite-dimensional irreducible gl n-module for each dominant weight, the entries of a dominant weight being free scalars and only their differences constrained. The existence input for the weights with natural number entries is TauCeti.exists_isGlHighestWeightVector_natCast; this file supplies the remaining central direction, so that the existence half of that classification reaches every dominant weight. Cutting the realizing module down to an irreducible one, and naming the resulting carrier, is not done here.

References

• W. Fulton, J. Harris, Representation Theory: A First Course, Springer GTM 129 (1991), §15.5, where the rational representations of GL n are the determinant twists of the polynomial ones.

The carrier of the trace twist

structure TauCeti.GlTraceTwist (ι : Type u_1) {R : Type u} (c : R) (M : Type v) : Type v

The trace twist of a gl ι-module M by a scalar c: a copy of M with the same R-module structure and with the bracket ⁅A, m⁆ + c · tr(A) · m. It is again a gl ι-module because the trace is a Lie character, that is, a linear form killing every commutator.

TauCeti.GlTraceTwist.linearEquiv identifies the underlying R-modules and TauCeti.GlTraceTwist.ofTwist_lie computes the twisted bracket, so that the twist is used through its API rather than through the wrapper.

• toTwist :: (
• ofTwist : M

  Read a vector of the trace twist as a vector of M.

• )

def TauCeti.GlTraceTwist.equiv (ι : Type u_1) {R : Type u} (c : R) (M : Type v) : GlTraceTwist ι c M ≃ M

TauCeti.GlTraceTwist.ofTwist and TauCeti.GlTraceTwist.toTwist as an equivalence: the twist has the same underlying type.

Equations

• TauCeti.GlTraceTwist.equiv ι c M = { toFun := TauCeti.GlTraceTwist.ofTwist, invFun := TauCeti.GlTraceTwist.toTwist ι c, left_inv := ⋯, right_inv := ⋯ }

instance TauCeti.GlTraceTwist.instNontrivial {R : Type u} {ι : Type u_1} {c : R} {M : Type v} [Nontrivial M] : Nontrivial (GlTraceTwist ι c M)

@[instance_reducible]

instance TauCeti.GlTraceTwist.instAddCommGroup {R : Type u} {ι : Type u_1} {c : R} {M : Type v} [AddCommGroup M] : AddCommGroup (GlTraceTwist ι c M)

Equations

• TauCeti.GlTraceTwist.instAddCommGroup = (TauCeti.GlTraceTwist.equiv ι c M).addCommGroup

def TauCeti.GlTraceTwist.addEquiv {R : Type u} (ι : Type u_1) (c : R) (M : Type v) [AddCommGroup M] : GlTraceTwist ι c M ≃+ M

The additive groups of a module and of its trace twist agree.

Equations

• TauCeti.GlTraceTwist.addEquiv ι c M = { toEquiv := TauCeti.GlTraceTwist.equiv ι c M, map_add' := ⋯ }

@[instance_reducible]

instance TauCeti.GlTraceTwist.instModule {R : Type u} {ι : Type u_1} {c : R} {M : Type v} [Semiring R] [AddCommGroup M] [Module R M] : Module R (GlTraceTwist ι c M)

Equations

• TauCeti.GlTraceTwist.instModule = AddEquiv.module R (TauCeti.GlTraceTwist.addEquiv ι c M)

def TauCeti.GlTraceTwist.linearEquiv {R : Type u} (ι : Type u_1) (c : R) (M : Type v) [Semiring R] [AddCommGroup M] [Module R M] : GlTraceTwist ι c M ≃ₗ[R] M

A trace twist has the same underlying R-module. Every statement about the twisted bracket is made against this equivalence, so that the wrapper is never unfolded.

Equations

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

@[simp]

theorem TauCeti.GlTraceTwist.coe_linearEquiv {R : Type u} {ι : Type u_1} {c : R} {M : Type v} [Semiring R] [AddCommGroup M] [Module R M] : ⇑(GlTraceTwist.linearEquiv ι c M) = ofTwist

The underlying-module equivalence of a trace twist is the underlying-vector map.

instance TauCeti.GlTraceTwist.instFinite {R : Type u} {ι : Type u_1} {c : R} {M : Type v} [Semiring R] [AddCommGroup M] [Module R M] [Module.Finite R M] : Module.Finite R (GlTraceTwist ι c M)

theorem TauCeti.GlTraceTwist.ofTwist_injective {R : Type u} {ι : Type u_1} {c : R} {M : Type v} : Function.Injective ofTwist

Two vectors of a trace twist with the same underlying vector are equal.

@[simp]

theorem TauCeti.GlTraceTwist.ofTwist_toTwist {R : Type u} {ι : Type u_1} {c : R} {M : Type v} (m : M) : { ofTwist := m }.ofTwist = m

Reading a vector of M into the twist and back returns it.

@[simp]

theorem TauCeti.GlTraceTwist.toTwist_ofTwist {R : Type u} {ι : Type u_1} {c : R} {M : Type v} (m : GlTraceTwist ι c M) : { ofTwist := m.ofTwist } = m

Reading a vector of the twist into M and back returns it.

@[simp]

theorem TauCeti.GlTraceTwist.ofTwist_add {R : Type u} {ι : Type u_1} {c : R} {M : Type v} [AddCommGroup M] (m p : GlTraceTwist ι c M) : (m + p).ofTwist = m.ofTwist + p.ofTwist

The addition of a trace twist is the addition of the module it twists.

@[simp]

theorem TauCeti.GlTraceTwist.ofTwist_zero {R : Type u} {ι : Type u_1} {c : R} {M : Type v} [AddCommGroup M] : ofTwist 0 = 0

The zero of a trace twist is the zero of the module it twists.

@[simp]

theorem TauCeti.GlTraceTwist.ofTwist_smul {R : Type u} {ι : Type u_1} {c : R} {M : Type v} [Semiring R] [AddCommGroup M] [Module R M] (t : R) (m : GlTraceTwist ι c M) : (t • m).ofTwist = t • m.ofTwist

The scalar action on a trace twist is the scalar action on the module it twists.

The twisted bracket

@[instance_reducible]

instance TauCeti.GlTraceTwist.instLieRingModuleMatrix {R : Type u} [CommRing R] {ι : Type u_1} [DecidableEq ι] [Fintype ι] {c : R} {M : Type v} [AddCommGroup M] [Module R M] [LieRingModule (Matrix ι ι R) M] [LieModule R (Matrix ι ι R) M] : LieRingModule (Matrix ι ι R) (GlTraceTwist ι c M)

Equations

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

@[simp]

theorem TauCeti.GlTraceTwist.ofTwist_lie {R : Type u} [CommRing R] {ι : Type u_1} [DecidableEq ι] [Fintype ι] {c : R} {M : Type v} [AddCommGroup M] [Module R M] [LieRingModule (Matrix ι ι R) M] [LieModule R (Matrix ι ι R) M] (A : Matrix ι ι R) (m : GlTraceTwist ι c M) : ⁅A, m⁆.ofTwist = ⁅A, m.ofTwist⁆ + (c * A.trace) • m.ofTwist

The defining equation of the twisted bracket: it adds the scalar c · tr(A) to the untwisted action of A.

instance TauCeti.GlTraceTwist.instLieModuleMatrix {R : Type u} [CommRing R] {ι : Type u_1} [DecidableEq ι] [Fintype ι] {c : R} {M : Type v} [AddCommGroup M] [Module R M] [LieRingModule (Matrix ι ι R) M] [LieModule R (Matrix ι ι R) M] : LieModule R (Matrix ι ι R) (GlTraceTwist ι c M)

Twisting a highest weight vector

theorem TauCeti.isGlHighestWeightVector_toTwist_iff {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] [LinearOrder ι] {c : R} {M : Type v} [AddCommGroup M] [Module R M] [LieRingModule (Matrix ι ι R) M] [LieModule R (Matrix ι ι R) M] {mu : ι → R} {v : M} : IsGlHighestWeightVector (fun (i : ι) => mu i + c) { ofTwist := v } ↔ IsGlHighestWeightVector mu v

Twisting shifts a highest weight by the twisting scalar, and does nothing else. The diagonal matrix unit Eᵢᵢ has trace 1 and the raising matrix units have trace 0, so the twisted bracket adds c to every coordinate of the weight and still annihilates the vector along the raising directions; conversely a highest weight vector of the twist that comes from M has a weight of that shape, with c subtracted back off. This is how a twisted highest weight hypothesis is eliminated, without unfolding the bracket.

theorem TauCeti.isGlHighestWeightVector_toTwist {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] [LinearOrder ι] {c : R} {M : Type v} [AddCommGroup M] [Module R M] [LieRingModule (Matrix ι ι R) M] [LieModule R (Matrix ι ι R) M] {mu : ι → R} {v : M} (hv : IsGlHighestWeightVector mu v) : IsGlHighestWeightVector (fun (i : ι) => mu i + c) { ofTwist := v }

Twisting shifts a highest weight by the twisting scalar, the introduction half of TauCeti.isGlHighestWeightVector_toTwist_iff.

Every dominant weight is a highest weight

def TauCeti.glTraceTwistedYoungWedge (R : Type u) [CommRing R] {ι : Type u_1} [Fintype ι] (a : ι → ℕ) (c : R) : Type (max u u_1)

The trace twist by c of the exterior power realizing a tuple a of natural numbers: the exterior power in which TauCeti.exists_isGlHighestWeightVector_natCast realizes a, twisted by c. For an antitone a it carries a highest weight vector of the dominant weight a + c · (1, …, 1), which is TauCeti.exists_isGlHighestWeightVector_of_isGlDominantIntegral; for an unrestricted a it is just the twisted exterior power.

As with TauCeti.VermaModule, the carrier is a definition with its module structures declared one by one, so that statements about it are made against this name rather than against the exterior power it is built from; the roadmap will later cut that construction down to an irreducible quotient. TauCeti.glTraceTwistedYoungWedge.linearEquiv is the identification of the underlying R-modules and TauCeti.glTraceTwistedYoungWedge.isGlHighestWeightVector_linearEquiv_symm populates it. It is finite over R, hence finite-dimensional over a field.

Equations

• TauCeti.glTraceTwistedYoungWedge R a c = TauCeti.GlTraceTwist ι c ↥(⋀[R]^(∑ i : ι, a i) (ι × Fin (∑ i : ι, a i) → R))

@[instance_reducible]

instance TauCeti.instAddCommGroupGlTraceTwistedYoungWedge {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] (a : ι → ℕ) (c : R) : AddCommGroup (glTraceTwistedYoungWedge R a c)

Equations

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

@[instance_reducible]

instance TauCeti.instModuleGlTraceTwistedYoungWedge {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] (a : ι → ℕ) (c : R) : Module R (glTraceTwistedYoungWedge R a c)

Equations

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

@[instance_reducible]

noncomputable instance TauCeti.instLieRingModuleMatrixGlTraceTwistedYoungWedge {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] [LinearOrder ι] (a : ι → ℕ) (c : R) : LieRingModule (Matrix ι ι R) (glTraceTwistedYoungWedge R a c)

Equations

• TauCeti.instLieRingModuleMatrixGlTraceTwistedYoungWedge a c = { bracket := TauCeti.instLieRingModuleMatrixGlTraceTwistedYoungWedge._aux_1 a c, add_lie := ⋯, lie_add := ⋯, leibniz_lie := ⋯ }

instance TauCeti.instLieModuleMatrixGlTraceTwistedYoungWedge {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] [LinearOrder ι] (a : ι → ℕ) (c : R) : LieModule R (Matrix ι ι R) (glTraceTwistedYoungWedge R a c)

instance TauCeti.instFiniteGlTraceTwistedYoungWedge {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] (a : ι → ℕ) (c : R) : Module.Finite R (glTraceTwistedYoungWedge R a c)

def TauCeti.glTraceTwistedYoungWedge.linearEquiv (R : Type u) [CommRing R] {ι : Type u_1} [Fintype ι] (a : ι → ℕ) (c : R) : glTraceTwistedYoungWedge R a c ≃ₗ[R] ↥(⋀[R]^(∑ i : ι, a i) (ι × Fin (∑ i : ι, a i) → R))

A trace-twisted Young wedge has the exterior power as its underlying R-module. Every statement about the carrier is made against this equivalence, so that the definition is not unfolded.

Equations

• TauCeti.glTraceTwistedYoungWedge.linearEquiv R a c = TauCeti.GlTraceTwist.linearEquiv ι c ↥(⋀[R]^(∑ i : ι, a i) (ι × Fin (∑ i : ι, a i) → R))

theorem TauCeti.glTraceTwistedYoungWedge.isGlHighestWeightVector_linearEquiv_symm {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] [LinearOrder ι] {a : ι → ℕ} {c : R} {nu : ι → R} {w : ↥(⋀[R]^(∑ i : ι, a i) (ι × Fin (∑ i : ι, a i) → R))} (hw : IsGlHighestWeightVector nu w) : IsGlHighestWeightVector (fun (i : ι) => nu i + c) ((linearEquiv R a c).symm w)

A highest weight vector of the exterior power gives one of the trace-twisted Young wedge, of the weight shifted by c in every coordinate. This is the introduction rule for the carrier; the matching elimination rule is TauCeti.isGlHighestWeightVector_toTwist_iff.

theorem TauCeti.exists_isGlHighestWeightVector_glTraceTwistedYoungWedge {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] [LinearOrder ι] [Nontrivial R] {a : ι → ℕ} {c : R} {nu : ι → R} (ha : Antitone a) (hnu : nu = fun (i : ι) => ↑(a i) + c) : ∃ (v : glTraceTwistedYoungWedge R a c), IsGlHighestWeightVector nu v

An antitone tuple translated along the central direction is a highest weight, realized in the corresponding trace-twisted Young wedge.

theorem TauCeti.exists_isGlHighestWeightVector_of_isGlDominantIntegral {R : Type u} [CommRing R] [CharZero R] {N : ℕ} {mu : Fin N → R} (hmu : IsGlDominantIntegral mu) : ∃ (a : Fin N → ℕ) (c : R), Antitone a ∧ (mu = fun (i : Fin N) => ↑(a i) + c) ∧ ∃ (v : glTraceTwistedYoungWedge R a c), IsGlHighestWeightVector mu v

Every dominant weight of gl N is a highest weight, in a module finite over R: write the weight as an antitone tuple of natural numbers translated along the central direction (TauCeti.IsGlDominantIntegral.exists_antitone_natCast_add_const), realize the tuple in an exterior power, and twist by the translation.