Homomorphisms out of the generated Chevalley carrier are determined by the root subgroups

The closed subgroup scheme of GLₙ generated by the represented Kostant root subgroups is, by construction, the smallest one through which every xᵢ : 𝔾ₐ ⟶ GLₙ factors. This file records what that minimality buys: a homomorphism out of the generated group scheme is determined by its restrictions to the root subgroups.

The argument is the scheme-theoretic replacement for "a group is generated by a family of subgroups, so a homomorphism is determined on generators". Two homomorphisms agreeing on every root subgroup have an equalizer, which is a closed subgroup scheme containing all of them; minimality forces it to be everything. In coordinate terms the equalizer Hopf ideal is squeezed below the defining ideal, so it vanishes.

This supplies the generated-carrier universal property needed by Layer 9's explicit Chevalley--Demazure construction: the theorems below quantify over the whole family e : I → L of represented root subgroups used to define the carrier. They do not establish the separate isomorphism theorem for pinned groups, whose uniqueness statement only assumes agreement on the simple root subgroups.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedCoordinate_hom_ext: two coordinate morphisms into the generated Chevalley carrier agreeing on every root subgroup are equal.
• TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedGroupScheme_hom_ext: the same statement for morphisms of affine group schemes out of the generated group scheme.

References

The determination of a homomorphism by a generating family of root subgroups is standard in the Chevalley--Demazure construction; see J. E. Humphreys, Linear Algebraic Groups, §27, and R. W. Carter, Simple Groups of Lie Type, §12.2. It advances the explicit "Chevalley--Demazure construction" and "Root subgroup maps" targets in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedCoordinate_hom_ext {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type u_1} {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) {Y : CommHopfAlgCat ℤ} (u v : Y ⟶ CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ n) (kostantGeneratedDefiningIdeal e h ρ M hM hnil b)) (huv : ∀ (i : I), CategoryTheory.CategoryStruct.comp u (kostantRootSubgroupGeneratedCoordinateMap e h ρ M hM hnil b i) = CategoryTheory.CategoryStruct.comp v (kostantRootSubgroupGeneratedCoordinateMap e h ρ M hM hnil b i)) : u = v

Coordinate rigidity. Two morphisms of commutative Hopf algebras into the coordinate algebra of the generated Chevalley carrier that agree after composing with every root-subgroup coordinate map are equal.

Contravariantly: a homomorphism of affine group schemes out of the group scheme generated by the Kostant root subgroups is determined by its restrictions to those root subgroups.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedGroupScheme_hom_ext {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type u_1} {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) {Y : CommHopfAlgCat ℤ} (φ ψ : kostantGeneratedGroupScheme e h ρ M hM hnil b ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op Y)) (hφψ : ∀ (i : I), CategoryTheory.CategoryStruct.comp (kostantRootSubgroupToGenerated e h ρ M hM hnil b i) φ = CategoryTheory.CategoryStruct.comp (kostantRootSubgroupToGenerated e h ρ M hM hnil b i) ψ) : φ = ψ

Rigidity of the generated Chevalley carrier. Two homomorphisms of affine group schemes out of the group scheme generated by the represented Kostant root subgroups are equal as soon as they agree after composing with every root subgroup xᵢ : 𝔾ₐ ⟶ G.

In particular, there is at most one endomorphism of the carrier realizing a prescribed action on the whole generating family.