Redundant generators of a closed subgroup scheme of GLₙ

Let f j : O(GLₙ/R) ⟶ K j be a family of coordinate morphisms indexed by ι ⊕ κ, and write G for the closed subgroup scheme of GLₙ it generates and G' for the one generated by the subfamily indexed by ι. This file proves that the members indexed by κ may be dropped as soon as each of them kills the defining Hopf ideal of G': then G = G', and a homomorphism out of G is determined by its restrictions to the generators indexed by ι alone. The equality of defining ideals is TauCeti.CommHopfAlgCat.commonKernelHopfIdeal_eq_of_toIdeal_le_ker.

The kernel condition says exactly that the universal point of K (.inr k) is a point of G'. It is usually proved pointwise, as an identity among matrices showing that each point of an extra generator, typically a split torus, is a product of points of the remaining ones, typically root subgroups; commonKernelHopfIdeal_toIdeal_le_ker_of_mapPointsFunctor_mem converts that pointwise statement into the kernel condition.

The equality concerns the subgroup scheme generated over R itself, with the maximal defining ideal of TauCeti.GeneralLinear.generatedGroupScheme; no base change is involved.

Main results

• TauCeti.GeneralLinear.commonKernelHopfIdeal_toIdeal_le_ker_of_mapPointsFunctor_mem: a coordinate morphism all of whose points lie in a generated subgroup scheme kills its defining Hopf ideal.
• TauCeti.GeneralLinear.generatedGroupScheme_eq_of_toIdeal_le_ker: the two generated group schemes agree.
• TauCeti.GeneralLinear.generatedGroupScheme_hom_ext_of_toIdeal_le_ker: homomorphisms out of the generated group scheme agreeing on the generators indexed by ι are equal.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, §§1.4 and 15.1.
• R. Steinberg, Lectures on Chevalley Groups, §3.

The universal-point argument generalizes TauCeti.kostantGeneratedDefiningIdeal_toIdeal_le_torus_ker_of_universal_torus_mem_elementary in TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.RootSubgroup.Scheme.ToralClosure.Generation, which treats the weight torus of a Kostant toral closure over ℤ.

theorem TauCeti.GeneralLinear.commonKernelHopfIdeal_toIdeal_le_ker_of_mapPointsFunctor_mem {R : Type u} [CommRing R] (n : ℕ) {ι : Type v} {K : ι → CommHopfAlgCat R} (p : (i : ι) → coordinateHopfAlgebra R n ⟶ K i) {L : CommHopfAlgCat R} (g : coordinateHopfAlgebra R n ⟶ L) (hg : ∀ (A : Type u) [inst : CommRing A] [inst_1 : Algebra R A] (q : ↑(HopfAlgebra.points ↧A)), (pointsMulEquiv n) ((CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor g).app ↧A)) q) ∈ generatedPointsSubgroup n p A) : (CommHopfAlgCat.commonKernelHopfIdeal p).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom g)).toRingHom

A generator whose points are already generated kills the defining ideal. If every point of g lies in the points of the subgroup scheme generated by p, then g kills the defining Hopf ideal of that subgroup scheme. Only the universal point of L is used. The converse is TauCeti.GeneralLinear.pointsMulEquiv_mapPointsFunctor_mem_hopfIdealPointsSubgroup.

theorem TauCeti.GeneralLinear.generatedGroupScheme_eq_of_toIdeal_le_ker {R : Type u} [CommRing R] (n : ℕ) {ι : Type v} {κ : Type w} {K : ι ⊕ κ → CommHopfAlgCat R} (f : (j : ι ⊕ κ) → coordinateHopfAlgebra R n ⟶ K j) (hker : ∀ (k : κ), (CommHopfAlgCat.commonKernelHopfIdeal fun (i : ι) => f (Sum.inl i)).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (f (Sum.inr k)))).toRingHom) : generatedGroupScheme n f = generatedGroupScheme n fun (i : ι) => f (Sum.inl i)

Dropping redundant generators, for the generated group schemes: if every generator indexed by κ kills the defining ideal of the subgroup scheme generated by those indexed by ι, then the subgroup scheme of GLₙ generated by the whole family is the one generated by the members indexed by ι.

theorem TauCeti.GeneralLinear.generatedGroupScheme_hom_ext_of_toIdeal_le_ker {R : Type u} [CommRing R] (n : ℕ) {ι : Type v} {κ : Type w} {K : ι ⊕ κ → CommHopfAlgCat R} (f : (j : ι ⊕ κ) → coordinateHopfAlgebra R n ⟶ K j) (hker : ∀ (k : κ), (CommHopfAlgCat.commonKernelHopfIdeal fun (i : ι) => f (Sum.inl i)).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (f (Sum.inr k)))).toRingHom) {Y : CommHopfAlgCat R} (φ ψ : generatedGroupScheme n f ⟶ (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op Y)) (h : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (generatorToGeneratedGroupScheme n f (Sum.inl i)) φ = CategoryTheory.CategoryStruct.comp (generatorToGeneratedGroupScheme n f (Sum.inl i)) ψ) : φ = ψ

Rigidity with redundant generators dropped. Under the hypothesis of generatedGroupScheme_eq_of_toIdeal_le_ker, two homomorphisms from the subgroup scheme generated by the whole family to an affine group scheme presented as hopfSpec Y are equal as soon as they agree on the generators indexed by ι.