Rigidity of the toral Kostant carrier

The toral Kostant carrier is the smallest closed subgroup scheme of GLₙ containing both the represented root subgroups and the represented weight torus. Consequently, a homomorphism out of that carrier is determined by its restrictions to those generators.

This file proves that statement first on coordinate Hopf algebras and then for affine group schemes. It complements TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedGroupScheme_hom_ext, which applies to the carrier generated by root subgroups alone. For the toral carrier, agreement on the root subgroups does not by itself account for the adjoined torus, so in general the torus restriction is an essential second hypothesis.

A variant gives the equivalent interface in which agreement on all root subgroups is replaced by agreement on the closed immersion of the root-generated carrier. This is the form used when an endomorphism has already been constructed on the root-generated part. When that closed immersion is an isomorphism, the torus hypothesis can be dropped altogether.

Main results

• TauCeti.UniversalEnvelopingAlgebra.kostantToralCoordinate_hom_ext: coordinate morphisms into the toral quotient are determined by every root coordinate and the weight-torus coordinate.
• TauCeti.UniversalEnvelopingAlgebra.kostantToralGroupScheme_hom_ext: group-scheme morphisms out of the toral carrier are determined by every root subgroup and the weight torus.
• TauCeti.UniversalEnvelopingAlgebra.kostantToralGroupScheme_hom_ext_of_generated: it is enough to agree on the root-generated carrier and the weight torus.
• kostantToralGroupScheme_hom_ext_of_isIso_kostantGeneratedToToral: when the root-generated carrier is the whole toral carrier, agreement on the root subgroups suffices.

Roadmap

This is the uniqueness step for the explicit carrier in Layer 9, “the isomorphism theorem for pinned groups”, of TauCetiRoadmap/ReductiveGroups/README.md. The full pinned isomorphism theorem must additionally construct the morphism from a root-datum isomorphism and reduce its determining data to the pinned simple root subgroups. Milestone L1 of TauCetiRoadmap/CFSGStatement/README.md consumes that theorem to turn a Dynkin-diagram symmetry into the graph automorphism in a Steinberg endomorphism.

References

• J. E. Humphreys, Linear Algebraic Groups, §27.
• R. W. Carter, Simple Groups of Lie Type, §§7.1 and 12.2.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralCoordinate_hom_ext {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Finite κ] {V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) {Y : CommHopfAlgCat ℤ} (u v : Y ⟶ CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ n) (kostantToralDefiningIdeal e h ρ M hM hnil b wt)) (hroot : ∀ (i : I), CategoryTheory.CategoryStruct.comp u (kostantRootSubgroupToralCoordinateMap e h ρ M hM hnil b wt i) = CategoryTheory.CategoryStruct.comp v (kostantRootSubgroupToralCoordinateMap e h ρ M hM hnil b wt i)) (htorus : CategoryTheory.CategoryStruct.comp u (kostantWeightTorusToralCoordinateMap e h ρ M hM hnil b wt) = CategoryTheory.CategoryStruct.comp v (kostantWeightTorusToralCoordinateMap e h ρ M hM hnil b wt)) : u = v

Coordinate rigidity of the toral carrier. Two morphisms of commutative Hopf algebras into the coordinate algebra of the toral Kostant carrier are equal when they agree after composition with every root-subgroup coordinate and with the weight-torus coordinate.

Contravariantly, a homomorphism out of the closed group scheme generated by the root subgroups and the torus is determined on those generators.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralGroupScheme_hom_ext {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Finite κ] {V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) {Y : CommHopfAlgCat ℤ} (φ ψ : kostantToralGroupScheme e h ρ M hM hnil b wt ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op Y)) (hroot : ∀ (i : I), CategoryTheory.CategoryStruct.comp (kostantRootSubgroupToToral e h ρ M hM hnil b wt i) φ = CategoryTheory.CategoryStruct.comp (kostantRootSubgroupToToral e h ρ M hM hnil b wt i) ψ) (htorus : CategoryTheory.CategoryStruct.comp (kostantWeightTorusToToral e h ρ M hM hnil b wt) φ = CategoryTheory.CategoryStruct.comp (kostantWeightTorusToToral e h ρ M hM hnil b wt) ψ) : φ = ψ

Rigidity of the toral Kostant group scheme. Two homomorphisms out of the toral carrier are equal when they agree on every represented root subgroup and on the represented weight torus.

This is the scheme-theoretic form of kostantToralCoordinate_hom_ext.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralGroupScheme_hom_ext_of_generated {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Finite κ] {V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) {Y : CommHopfAlgCat ℤ} (φ ψ : kostantToralGroupScheme e h ρ M hM hnil b wt ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op Y)) (hgenerated : CategoryTheory.CategoryStruct.comp (kostantGeneratedToToral e h ρ M hM hnil b wt) φ = CategoryTheory.CategoryStruct.comp (kostantGeneratedToToral e h ρ M hM hnil b wt) ψ) (htorus : CategoryTheory.CategoryStruct.comp (kostantWeightTorusToToral e h ρ M hM hnil b wt) φ = CategoryTheory.CategoryStruct.comp (kostantWeightTorusToToral e h ρ M hM hnil b wt) ψ) : φ = ψ

It is enough to compare homomorphisms out of the toral carrier on the root-generated closed subgroup scheme and on the weight torus. This packages all root-subgroup hypotheses of kostantToralGroupScheme_hom_ext through kostantGeneratedToToral.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralGroupScheme_hom_ext_of_isIso_kostantGeneratedToToral {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Finite κ] {V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) [CategoryTheory.IsIso (kostantGeneratedToToral e h ρ M hM hnil b wt)] {Y : CommHopfAlgCat ℤ} (φ ψ : kostantToralGroupScheme e h ρ M hM hnil b wt ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op Y)) (hroot : ∀ (i : I), CategoryTheory.CategoryStruct.comp (kostantRootSubgroupToToral e h ρ M hM hnil b wt i) φ = CategoryTheory.CategoryStruct.comp (kostantRootSubgroupToToral e h ρ M hM hnil b wt i) ψ) : φ = ψ

If the canonical comparison from the root-generated carrier is an isomorphism, then two homomorphisms out of the toral carrier are equal as soon as they agree on every represented root subgroup; the weight-torus hypothesis of kostantToralGroupScheme_hom_ext becomes redundant.