The standard representation of a weight Levi

Restricting the standard representation of GL_N to the block-diagonal subgroup attached to an integer weight gives a faithful, completely reducible comodule over every field. Invariant subspaces are sums of whole weight blocks, and the remaining blocks give invariant complements. This supplies the representation-theoretic input to reductivity of weight Levis, including those with repeated weights.

The argument uses the localized polynomial presentation of the coordinate algebra: linear functionals extracting its surviving matrix entries recover the elementary matrix operators from the coaction. Thus the result also holds over finite fields, where rational points alone need not detect subcomodules.

References

• J. S. Milne, Algebraic Groups (2017), Chapters 4 and 13.
• J. C. Jantzen, Representations of Algebraic Groups, I.2.

The corestriction and faithfulness construction follows the standard SL_N comodule in TauCeti.Algebra.AlgebraicGroup.SpecialLinear.StandardComodule.

@[instance_reducible]

noncomputable def TauCeti.GeneralLinear.weightLeviStandardComodule (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) : Comodule R (↑(weightLeviCoordinateHopfAlgebra R w)) (Fin N → R)

The standard representation of a weight Levi, restricted from GL_N.

Equations

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

@[simp]

theorem TauCeti.GeneralLinear.weightLeviStandardComodule_coact (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) : Comodule.corestrictCoact (Bialgebra.Quotient.mkBialgHom (weightLeviDefiningHopfIdeal R w).toIdeal).toCoalgHom = TensorProduct.map LinearMap.id (Bialgebra.Quotient.mkBialgHom (weightLeviDefiningHopfIdeal R w).toIdeal).toLinearMap ∘ₗ standardCoact R N

The standard weight-Levi coaction is the standard GL_N coaction followed by the quotient map on the coordinate factor.

theorem TauCeti.GeneralLinear.weightLeviStandardComodule_coact_single (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) (j : Fin N) : Comodule.coact (Pi.single j 1) = ∑ i : Fin N, Pi.single i 1 ⊗ₜ[R] (Ideal.Quotient.mk (weightLeviDefiningHopfIdeal R w).toIdeal) (genericMatrix R N i j)

The standard weight-Levi coaction on a basis vector is its quotient generic column.

theorem TauCeti.GeneralLinear.isFaithful_weightLeviStandardComodule (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) : Comodule.IsFaithful

The standard representation of every weight Levi is faithful.

noncomputable def TauCeti.GeneralLinear.weightLeviCoordinateSubcomodule (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) (s : Set (Fin N)) (hs : ∀ (i j : Fin N), w i = w j → j ∈ s → i ∈ s) : Subcomodule R (↑(weightLeviCoordinateHopfAlgebra R w)) (Fin N → R)

A union of weight blocks spans a standard weight-Levi subcomodule.

Equations

• TauCeti.GeneralLinear.weightLeviCoordinateSubcomodule R w s hs = (Pi.basisFun R (Fin N)).coordinateSpanSubcomodule s ⋯

@[simp]

theorem TauCeti.GeneralLinear.weightLeviCoordinateSubcomodule_toSubmodule (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) (s : Set (Fin N)) (hs : ∀ (i j : Fin N), w i = w j → j ∈ s → i ∈ s) : (weightLeviCoordinateSubcomodule R w s hs).toSubmodule = Submodule.span R (⇑(Pi.basisFun R (Fin N)) '' s)

The coordinate subcomodule is the span of the selected standard basis vectors.

@[simp]

theorem TauCeti.GeneralLinear.mem_weightLeviCoordinateSubcomodule (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) (s : Set (Fin N)) (hs : ∀ (i j : Fin N), w i = w j → j ∈ s → i ∈ s) (v : Fin N → R) : v ∈ weightLeviCoordinateSubcomodule R w s hs ↔ ∀ i ∉ s, v i = 0

Membership in a coordinate subcomodule means vanishing outside its chosen weight blocks.

theorem TauCeti.GeneralLinear.single_mem_weightLeviStandardSubcomodule {N : ℕ} (w : Fin N → ℤ) (k : Type u) [Field k] (W : Subcomodule k (↑(weightLeviCoordinateHopfAlgebra k w)) (Fin N → k)) {v : Fin N → k} (hv : v ∈ W) (i j : Fin N) (hij : w i = w j) : Pi.single i (v j) ∈ W

An invariant subspace contains every elementary matrix translate within a weight block.

theorem TauCeti.GeneralLinear.weightLeviStandardSubcomodule_eq_span {N : ℕ} (w : Fin N → ℤ) (k : Type u) [Field k] (W : Subcomodule k (↑(weightLeviCoordinateHopfAlgebra k w)) (Fin N → k)) : W.toSubmodule = Submodule.span k (⇑(Pi.basisFun k (Fin N)) '' {i : Fin N | Pi.single i 1 ∈ W})

Every standard weight-Levi subcomodule is spanned by the coordinate vectors it contains.

theorem TauCeti.GeneralLinear.isCompletelyReducible_weightLeviStandardComodule {N : ℕ} (w : Fin N → ℤ) (k : Type u) [Field k] : Comodule.IsCompletelyReducible k (↑(weightLeviCoordinateHopfAlgebra k w)) (Fin N → k)

The standard representation of an arbitrary weight Levi is completely reducible.