Weight tori in the general linear group scheme

Let wt : Fin N → κ → ℤ be a finite family of characters of the split torus 𝔾ₘ^κ. Each character gives a diagonal entry, and together they define a group-scheme morphism

𝔾ₘ^κ → GL_N,     s ↦ diag(∏_j s_j ^ wt(i,j)).

This file constructs the morphism by factoring it through the diagonal torus of GL_N. On character lattices, the factorization is the homomorphism sending the i-th coordinate character to wt i; contravariance of diagonalizable groups gives the required map of split tori. The scheme-valued point formula then follows from the existing point comparisons for diagonalizable groups and the diagonal torus. The file also computes the algebra-valued point map induced by the weight-torus coordinate morphism and specializes the construction to the rank-one cocharacter attached to an integer weight on each coordinate.

The construction is the scheme-level realization of TauCeti.basisWeightTorus. In particular, when wt is the weight function of a finite free admissible lattice, it supplies the split-torus morphism in the pinned Chevalley--Demazure construction of Layer 9 of the ReductiveGroups roadmap. No faithfulness is asserted: an arbitrary weight family may have a common kernel.

Main declarations

• TauCeti.GeneralLinear.weightCharacterMap: the homomorphism on character lattices.
• TauCeti.GeneralLinear.weightTorusCoordinateMap: the coordinate Hopf-algebra morphism of the represented weight torus.
• TauCeti.GeneralLinear.weightTorusCoordinateMap_surjective: spanning weights make the coordinate morphism surjective.
• TauCeti.GeneralLinear.weightTorusCoordinateBialgHom: its direct diagonal-representation form, allowing the base ring and torus index to live in different universes.
• TauCeti.GeneralLinear.corestrict_standardComodule_weightTorusCoordinateBialgHom_eq_ofWeights: restriction of the standard comodule to a weight torus is the corresponding weight comodule.
• TauCeti.GeneralLinear.weightTorusBaseChangeCoordinateMap: that morphism base changed along R → K and transported into the coordinate Hopf algebras built directly over K.
• TauCeti.GeneralLinear.hom_weightTorusBaseChangeCoordinateMap: the transported map's underlying bialgebra morphism is the direct construction over K.
• TauCeti.GeneralLinear.weightTorusBaseChangeCoordinateMap_eq: the transported map agrees with the categorical weight-torus coordinate morphism over K when all data share one universe.
• TauCeti.GeneralLinear.weightTorus: the represented morphism 𝔾ₘ^κ → GL_N.
• TauCeti.GeneralLinear.isClosedImmersion_weightTorus: spanning weights make the represented morphism a closed immersion.
• TauCeti.GeneralLinear.weightTorusClosedSubgroup: the resulting closed subgroup scheme.
• TauCeti.GeneralLinear.schemePointsMulEquiv_weightTorus: its diagonal matrix on scheme-valued points.
• TauCeti.GeneralLinear.mapPointsFunctor_weightTorusCoordinateMap_app: the induced map on algebra-valued points.
• TauCeti.GeneralLinear.diagonalTorusCoordinates_pointsMap_weightCharacterMap: the diagonal coordinates of that point map are the prescribed characters.
• TauCeti.GeneralLinear.weightTorusCoordinateMap_reindex: composing every weight with a permutation of the torus index relabels the weight-torus coordinate map.
• TauCeti.GeneralLinear.pointsMulEquiv_mapPointsFunctor_weightTorusCoordinateMap: the diagonal matrix the weight torus produces on algebra-valued points.
• TauCeti.GeneralLinear.weightCocharacter: the cocharacter attached to integer coordinate weights.
• TauCeti.GeneralLinear.mapDomain_weightCocharacter: its concrete action on algebra-valued points.

References

• J. S. Milne, Algebraic Groups (2017), §§12 and 21.
• R. W. Carter, Simple Groups of Lie Type (1972), §§4.4 and 7.1.

noncomputable def TauCeti.GeneralLinear.weightTorusCoordinateBialgHom {N : ℕ} {S : Type u} {sigma : Type v} [CommRing S] [Finite sigma] (wt : Fin N → sigma → ℤ) : ↑(coordinateHopfAlgebra S N) →ₐc[S] MonoidAlgebra S (Multiplicative (sigma →₀ ℤ))

The weight-torus coordinate bialgebra morphism constructed directly as a diagonal representation. Unlike the categorical factorization through diagonalTorusCoordinateMap, this construction permits the base ring and the torus index to live in different universes.

Equations

• TauCeti.GeneralLinear.weightTorusCoordinateBialgHom wt = TauCeti.DiagonalizableGroup.diagonalCoordinateMap (Pi.basisFun S (Fin N)) fun (i : Fin N) => TauCeti.SplitTorus.weightCharacter (wt i)

@[simp]

theorem TauCeti.GeneralLinear.weightTorusCoordinateBialgHom_X {N : ℕ} {S : Type u} {sigma : Type v} [CommRing S] [Finite sigma] (wt : Fin N → sigma → ℤ) (i j : Fin N) : (weightTorusCoordinateBialgHom wt) ((coordinateHopfAlgebraAlgEquiv S N) ((coordinateRingMap S N) (MvPolynomial.X (i, j)))) = if i = j then MonoidAlgebra.single (Multiplicative.ofAdd (Finsupp.equivFunOnFinite.symm (wt i))) 1 else 0

A generic matrix entry maps under the direct weight-torus bialgebra morphism to the prescribed character on the diagonal, and to zero off the diagonal.

theorem TauCeti.GeneralLinear.corestrict_standardComodule_weightTorusCoordinateBialgHom_eq_ofWeights {N : ℕ} {S : Type u} {sigma : Type v} [CommRing S] [Finite sigma] (wt : Fin N → sigma → ℤ) : have x := standardComodule S N; Comodule.Corestrict (weightTorusCoordinateBialgHom wt).toCoalgHom = Comodule.ofWeights (Pi.basisFun S (Fin N)) fun (a : Fin N) => Multiplicative.ofAdd (Finsupp.equivFunOnFinite.symm (wt a))

Corestricting the standard general-linear comodule along a weight-torus coordinate morphism is the direct sum of its prescribed one-dimensional weight comodules.

theorem TauCeti.GeneralLinear.corestrict_corestrict_standardComodule_eq_ofWeights {N : ℕ} {S : Type u} {sigma : Type v} [CommRing S] [Finite sigma] [Fintype sigma] {H : Type u_1} [CommRing H] [HopfAlgebra S H] (f : ↑(coordinateHopfAlgebra S N) →ₐc[S] H) (g : H →ₐc[S] MonoidAlgebra S (Multiplicative (sigma →₀ ℤ))) (wt : Fin N → sigma → ℤ) (hcomp : g.comp f = weightTorusCoordinateBialgHom wt) : have x := standardComodule S N; have x := Comodule.Corestrict f.toCoalgHom; Comodule.Corestrict g.toCoalgHom = Comodule.ofWeights (Pi.basisFun S (Fin N)) fun (a : Fin N) => SplitTorus.weightCharacter (wt a)

If a weight-torus morphism factors through another coordinate Hopf algebra, restricting the corestricted standard comodule along that factor gives the same prescribed weight comodule.

noncomputable def TauCeti.GeneralLinear.weightCharacterMap {κ : Type u} {N : ℕ} [Finite κ] (wt : Fin N → κ → ℤ) : Multiplicative (ULift.{u, 0} (Fin N) →₀ ℤ) →* Multiplicative (κ →₀ ℤ)

The character-lattice map associated to a family of weights. It sends the standard character at i : Fin N to the finitely supported function corresponding to wt i.

Contravariance turns this map into a morphism from the rank-κ split torus to the rank-N diagonal torus.

Equations

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

@[simp]

theorem TauCeti.GeneralLinear.weightCharacterMap_ofAdd_single {κ : Type u} {N : ℕ} [Finite κ] (wt : Fin N → κ → ℤ) (i : Fin N) : (weightCharacterMap wt) (Multiplicative.ofAdd (Finsupp.single { down := i } 1)) = Multiplicative.ofAdd (Finsupp.equivFunOnFinite.symm (wt i))

The weight character-lattice map takes a standard character to the corresponding weight.

noncomputable def TauCeti.GeneralLinear.weightTorusCoordinateMap {R κ : Type u} [CommRing R] {N : ℕ} [Finite κ] (wt : Fin N → κ → ℤ) : coordinateHopfAlgebra R N ⟶ (DiagonalizableGroup.coordinateRing R (SplitTorus.characterGroup κ)).obj

The coordinate Hopf-algebra morphism of the weight torus. It first restricts functions on GL_N to its diagonal torus, then applies the group-algebra map induced by the prescribed weights. Its direction is opposite to the represented group-scheme morphism.

Equations

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

theorem TauCeti.GeneralLinear.weightTorusCoordinateMap_apply {R κ : Type u} [CommRing R] {N : ℕ} [Finite κ] (wt : Fin N → κ → ℤ) (x : ↑(coordinateHopfAlgebra R N)) : (CommHopfAlgCat.Hom.hom (weightTorusCoordinateMap wt)) x = (MonoidAlgebra.mapDomainBialgHom R (weightCharacterMap wt)) ((CommHopfAlgCat.Hom.hom diagonalTorusCoordinateMap) x)

Applying the weight-torus coordinate map first restricts to the diagonal torus and then maps each diagonal character along weightCharacterMap.

@[simp]

theorem TauCeti.GeneralLinear.weightTorusCoordinateMap_X {R κ : Type u} [CommRing R] {N : ℕ} [Finite κ] (wt : Fin N → κ → ℤ) (i j : Fin N) : (CommHopfAlgCat.Hom.hom (weightTorusCoordinateMap wt)) ((coordinateHopfAlgebraAlgEquiv R N) ((coordinateRingMap R N) (MvPolynomial.X (i, j)))) = if i = j then MonoidAlgebra.single (Multiplicative.ofAdd (Finsupp.equivFunOnFinite.symm (wt i))) 1 else 0

A generic matrix entry restricts along the weight torus to the prescribed character on the diagonal, and to zero off the diagonal.

theorem TauCeti.GeneralLinear.hom_weightTorusCoordinateMap {R κ : Type u} [CommRing R] {N : ℕ} [Finite κ] (wt : Fin N → κ → ℤ) : CommHopfAlgCat.Hom.hom (weightTorusCoordinateMap wt) = weightTorusCoordinateBialgHom wt

The categorical weight-torus coordinate map is the direct diagonal-representation bialgebra morphism when the base ring and torus index live in the same universe.

theorem TauCeti.GeneralLinear.weightTorusCoordinateMap_surjective {R κ : Type u} [CommRing R] {N : ℕ} [Finite κ] (wt : Fin N → κ → ℤ) (hwt : Submodule.span ℤ (Set.range wt) = ⊤) : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (weightTorusCoordinateMap wt))

A spanning family of weights makes the weight-torus coordinate morphism surjective.

noncomputable def TauCeti.GeneralLinear.weightTorus {R κ : Type u} [CommRing R] {N : ℕ} [Finite κ] (wt : Fin N → κ → ℤ) : SplitTorus.groupScheme R κ ⟶ groupScheme R N

The group-scheme morphism from a split torus to GL_N prescribed by a family of weights. It factors through the diagonal torus: the i-th diagonal entry is the character wt i.

Equations

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

theorem TauCeti.GeneralLinear.weightTorus_def {R κ : Type u} [CommRing R] {N : ℕ} [Finite κ] (wt : Fin N → κ → ℤ) : weightTorus wt = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec ↧R).map (weightTorusCoordinateMap wt).op) (CategoryTheory.eqToHom ⋯))

The weight torus is relative spectrum applied contravariantly to its coordinate morphism, transported across the named presentations of the split torus and GL_N.

theorem TauCeti.GeneralLinear.weightTorus_eq_diagonalGroupSchemeHom {R κ : Type u} [CommRing R] {N : ℕ} [Finite κ] [Fintype κ] (wt : Fin N → κ → ℤ) : weightTorus wt = DiagonalizableGroup.diagonalGroupSchemeHom (SplitTorus.characterGroup κ) (Pi.basisFun R (Fin N)) fun (i : Fin N) => SplitTorus.weightCharacter (wt i)

The represented weight torus is the diagonalizable-group representation whose characters are the prescribed weights.

theorem TauCeti.GeneralLinear.isClosedImmersion_weightTorus {R κ : Type u} [CommRing R] {N : ℕ} [Finite κ] (wt : Fin N → κ → ℤ) (hwt : Submodule.span ℤ (Set.range wt) = ⊤) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (weightTorus wt).hom.hom)

A family of weights spanning the character lattice represents the split torus as a closed subgroup of GL_N.

noncomputable def TauCeti.GeneralLinear.weightTorusClosedSubgroup {R κ : Type u} [CommRing R] {N : ℕ} [Finite κ] (wt : Fin N → κ → ℤ) (hwt : Submodule.span ℤ (Set.range wt) = ⊤) : ClosedSubgroupScheme (groupScheme R N)

The split torus represented by a spanning family of weights, as a closed subgroup scheme of GL_N. This does not assert maximality in an ambient reductive group.

Equations

• TauCeti.GeneralLinear.weightTorusClosedSubgroup wt hwt = TauCeti.ClosedSubgroupScheme.mk (TauCeti.GeneralLinear.weightTorus wt)

@[simp]

theorem TauCeti.GeneralLinear.coe_weightTorusClosedSubgroup {R κ : Type u} [CommRing R] {N : ℕ} [Finite κ] (wt : Fin N → κ → ℤ) (hwt : Submodule.span ℤ (Set.range wt) = ⊤) : have x := ⋯; ↑(weightTorusClosedSubgroup wt hwt) = CategoryTheory.Subobject.mk (weightTorus wt)

The underlying subobject of a closed weight torus is represented by its defining weight-torus morphism.

noncomputable def TauCeti.GeneralLinear.weightTorusBaseChangeCoordinateMap {κ : Type u} {N : ℕ} [Finite κ] (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (wt : Fin N → κ → ℤ) : coordinateHopfAlgebra K N ⟶ (DiagonalizableGroup.coordinateRing K (SplitTorus.characterGroup κ)).obj

The base change along R → K of the weight-torus coordinate map, transported into the coordinate Hopf algebras built directly over K by coordinateHopfAlgebraBaseChangeIso and DiagonalizableGroup.baseChangeCoordinateHopfAlgebraIso.

This is a transport of the map over R, not a fresh construction over K. hom_weightTorusBaseChangeCoordinateMap identifies its underlying bialgebra morphism with the direct construction over K; weightTorusBaseChangeCoordinateMap_eq gives the categorical same-universe form.

Equations

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

theorem TauCeti.GeneralLinear.weightTorusBaseChangeCoordinateMap_def {κ : Type u} {N : ℕ} [Finite κ] (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (wt : Fin N → κ → ℤ) : weightTorusBaseChangeCoordinateMap R K wt = CategoryTheory.CategoryStruct.comp (coordinateHopfAlgebraBaseChangeIso R K N).inv (CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap (weightTorusCoordinateMap wt)) (DiagonalizableGroup.baseChangeCoordinateHopfAlgebraIso R K (SplitTorus.characterGroup κ)).hom)

The base-changed weight-torus coordinate map is the stated composite of the two coordinate base-change isomorphisms with the scalar extension of the map over R.

The module system does not expose a definition's body outside its own module, so this is the form in which downstream files can rewrite with the definition.

theorem TauCeti.GeneralLinear.hom_weightTorusBaseChangeCoordinateMap {κ : Type u} {N : ℕ} [Finite κ] (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (wt : Fin N → κ → ℤ) : CommHopfAlgCat.Hom.hom (weightTorusBaseChangeCoordinateMap R K wt) = weightTorusCoordinateBialgHom wt

Weight-torus coordinate morphisms commute with base change. The underlying bialgebra morphism of the transported scalar extension is the direct diagonal-representation morphism over K. This statement allows the extension ring to live in a larger universe.

theorem TauCeti.GeneralLinear.weightTorusBaseChangeCoordinateMap_eq {κ : Type u} {N : ℕ} [Finite κ] (R K : Type u) [CommRing R] [CommRing K] [Algebra R K] (wt : Fin N → κ → ℤ) : weightTorusBaseChangeCoordinateMap R K wt = weightTorusCoordinateMap wt

In one universe, base change of the categorical weight-torus coordinate map agrees with the categorical map constructed directly over the extension ring.

@[simp]

theorem TauCeti.GeneralLinear.mapPointsFunctor_weightTorusCoordinateMap_app {R κ : Type u} [CommRing R] {N : ℕ} [Finite κ] (wt : Fin N → κ → ℤ) (A : CommAlgCat R) (p : ↑(HopfAlgebra.points A)) : (CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (weightTorusCoordinateMap wt)).app A)) p = diagonalTorusPoints ((DiagonalizableGroup.pointsMap (weightCharacterMap wt)) p)

Precomposition by the weight-torus coordinate morphism first restricts a character along the weight map and then embeds the resulting diagonal-torus point into GL_N.

theorem TauCeti.GeneralLinear.diagonalTorusCoordinates_pointsMap_weightCharacterMap {R κ : Type u} [CommRing R] {N : ℕ} [Fintype κ] (wt : Fin N → κ → ℤ) (A : CommAlgCat R) (p : ↑(HopfAlgebra.points A)) (i : Fin N) : diagonalTorusCoordinates (SplitTorus.pointsMulEquiv ((DiagonalizableGroup.pointsMap (weightCharacterMap wt)) p)) i = torusCharacter (SplitTorus.pointsMulEquiv p) (wt i)

The diagonal coordinates obtained by restricting a split-torus point along a weight family are the corresponding torus characters.

theorem TauCeti.GeneralLinear.pointsMulEquiv_mapPointsFunctor_weightTorusCoordinateMap {R κ : Type u} [CommRing R] {N : ℕ} [Fintype κ] (wt : Fin N → κ → ℤ) (A : CommAlgCat R) (p : ↑(HopfAlgebra.points A)) : (pointsMulEquiv N) ((CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (weightTorusCoordinateMap wt)).app A)) p) = diagGL fun (i : Fin N) => torusCharacter (SplitTorus.pointsMulEquiv p) (wt i)

On algebra-valued points, the weight-torus coordinate morphism is the diagonal matrix whose i-th entry is the value of the character wt i.

theorem TauCeti.GeneralLinear.weightTorusCoordinateMap_determinantGroupLike {R κ : Type u} [CommRing R] {N : ℕ} [Finite κ] (wt : Fin N → κ → ℤ) (hwt : ∑ i : Fin N, wt i = 0) : (CommHopfAlgCat.Hom.hom (weightTorusCoordinateMap wt)) ↑(determinantGroupLike R N) = 1

A represented weight torus has determinant one when the sum of its weights is zero.

theorem TauCeti.GeneralLinear.hom_weightTorusCoordinateMap_reindex {R κ : Type u} [CommRing R] {N : ℕ} [Finite κ] (τ : Equiv.Perm κ) (wt : Fin N → κ → ℤ) : CommHopfAlgCat.Hom.hom (weightTorusCoordinateMap fun (i : Fin N) => wt i ∘ ⇑τ) = (MonoidAlgebra.mapDomainBialgHom R (SplitTorus.characterRelabel τ⁻¹).toMonoidHom).comp (CommHopfAlgCat.Hom.hom (weightTorusCoordinateMap wt))

Composing every weight with a permutation τ of the torus index relabels the underlying bialgebra morphism of the weight-torus coordinate map by τ⁻¹.

theorem TauCeti.GeneralLinear.weightTorusCoordinateMap_reindex {R κ : Type u} [CommRing R] {N : ℕ} [Finite κ] (τ : Equiv.Perm κ) (wt : Fin N → κ → ℤ) : (weightTorusCoordinateMap fun (i : Fin N) => wt i ∘ ⇑τ) = CategoryTheory.CategoryStruct.comp (weightTorusCoordinateMap wt) (SplitTorus.relabelCoordinateMap R τ⁻¹)

Composing every weight with a permutation τ of the torus index relabels the represented weight torus by τ⁻¹. The two weight families present the same subgroup of GL_N, differing only by the automorphism of the split torus which τ induces.

def TauCeti.GeneralLinear.weightDiagonalUnits {N : ℕ} {A : Type v} [CommMonoid A] (w : Fin N → ℤ) : Aˣ →* Fin N → Aˣ

The diagonal unit family i ↦ t ^ w i attached to integer weights.

Equations

• TauCeti.GeneralLinear.weightDiagonalUnits w = MonoidHom.pi fun (i : Fin N) => zpowGroupHom (w i)

@[simp]

theorem TauCeti.GeneralLinear.weightDiagonalUnits_apply {N : ℕ} {A : Type v} [CommMonoid A] (w : Fin N → ℤ) (t : Aˣ) (i : Fin N) : (weightDiagonalUnits w) t i = t ^ w i

The i-th diagonal coordinate of the weight cocharacter is t ^ w i.

noncomputable def TauCeti.GeneralLinear.weightCocharacter {R : Type u} [CommRing R] {N : ℕ} (w : Fin N → ℤ) : ↑(coordinateHopfAlgebra R N) →ₐc[R] LaurentPolynomial R

The cocharacter of GL_N acting on the i-th coordinate with integer weight w i.

Equations

• TauCeti.GeneralLinear.weightCocharacter w = CommHopfAlgCat.Hom.hom (TauCeti.GeneralLinear.weightCocharacterCoordinateMap✝ w)

noncomputable def TauCeti.GeneralLinear.weightCocharacterPoints {R : Type u} [CommRing R] {N : ℕ} {A : Type v} [CommRing A] [Algebra R A] (w : Fin N → ℤ) : WithConv (LaurentPolynomial R →ₐ[R] A) →* WithConv (↑(coordinateHopfAlgebra R N) →ₐ[R] A)

The weight cocharacter on algebra-valued points.

Equations

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

theorem TauCeti.GeneralLinear.pointsMulEquiv_weightCocharacterPoints {R : Type u} [CommRing R] {N : ℕ} {A : Type v} [CommRing A] [Algebra R A] (w : Fin N → ℤ) (f : WithConv (LaurentPolynomial R →ₐ[R] A)) : (pointsMulEquiv N) ((weightCocharacterPoints w) f) = diagGL ((weightDiagonalUnits w) (MultiplicativeGroup.pointsMulEquiv f))

Reading the weight cocharacter as a matrix gives diag(t ^ w i).

theorem TauCeti.GeneralLinear.mapDomain_weightCocharacter {R : Type u} [CommRing R] {N : ℕ} {A : Type v} [CommRing A] [Algebra R A] (w : Fin N → ℤ) (f : WithConv (LaurentPolynomial R →ₐ[R] A)) : (AlgHom.mapDomain (weightCocharacter w)) f = (weightCocharacterPoints w) f

Precomposition by the weight cocharacter sends a Laurent point to its concrete diagonal weight-cocharacter point.

@[simp]

theorem TauCeti.GeneralLinear.schemePointsMulEquiv_weightTorus {R κ : Type u} [CommRing R] {N : ℕ} {A : Type u} [CommRing A] [Algebra R A] [Fintype κ] (wt : Fin N → κ → ℤ) (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (SplitTorus.groupScheme R κ).X) : (schemePointsMulEquiv N A) (CategoryTheory.CategoryStruct.comp p (weightTorus wt).hom.hom) = diagGL fun (i : Fin N) => torusCharacter (SplitTorus.schemePointsMulEquiv p) (wt i)

On scheme-valued points, the weight torus is the diagonal matrix whose i-th diagonal entry is the value of the character wt i.