The closed subgroup scheme of GLₙ generated by a family of coordinate morphisms

Over a commutative ring R, fix a family of morphisms of commutative Hopf algebras

f i : O(GLₙ/R) ⟶ K i.

Contravariantly these are homomorphisms Spec (K i) ⟶ GLₙ of affine group schemes, and the smallest closed subgroup scheme of GLₙ through which all of them factor is cut out by the largest Hopf ideal contained in all their kernels. This file packages that common-kernel quotient as a closed subgroup scheme of GLₙ over R, together with its matrix-valued points.

The defining ideal is maximal among Hopf ideals killed by the f i over R itself. That maximality is what makes the scheme receive endomorphisms from generator equations, and it is the reason to form the scheme over the ring one works over rather than to base change a scheme generated over a subring: a Hopf ideal killed by the base-changed generators need not descend.

No reductivity, smoothness, flatness or root-datum statement is asserted, and nothing here identifies the points of the generated scheme with the abstract subgroup generated by the images of the K i-points; only the containment of the latter in the former is formal.

Main declarations

• TauCeti.GeneralLinear.generatedGroupScheme: the closed subgroup scheme of GLₙ generated by the family, presented as a Hopf-ideal quotient of O(GLₙ/R).
• TauCeti.GeneralLinear.generatedGroupSchemeι: its closed immersion into GLₙ.
• TauCeti.GeneralLinear.generatorToGeneratedGroupScheme: the morphism Spec (K i) ⟶ the generated scheme through which the ith generator factors.
• TauCeti.GeneralLinear.generatedPointsSubgroup: its matrix-valued points over an R-algebra.
• TauCeti.GeneralLinear.pointsMulEquiv_mapPointsFunctor_mem_generatedPointsSubgroup: every matrix coming from a point of some K i is a point of the generated scheme.

References

The construction is the scheme-theoretic subgroup generated by a family of homomorphisms; see J. E. Humphreys, Linear Algebraic Groups, §7.5, and W. C. Waterhouse, Introduction to Affine Group Schemes, §15.1. In the Chevalley--Demazure setting the family consists of the root subgroups and a split torus.

noncomputable def TauCeti.GeneralLinear.generatedGroupScheme {R : Type u} [CommRing R] (n : ℕ) {ι : Type v} {K : ι → CommHopfAlgCat R} (f : (i : ι) → coordinateHopfAlgebra R n ⟶ K i) : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))

The affine group scheme generated inside GLₙ by a family of coordinate morphisms, presented as the quotient of O(GLₙ/R) by the largest Hopf ideal killed by all of them.

Equations

• TauCeti.GeneralLinear.generatedGroupScheme n f = TauCeti.CommHopfAlgCat.quotientSpec (TauCeti.GeneralLinear.coordinateHopfAlgebra R n) (TauCeti.CommHopfAlgCat.commonKernelHopfIdeal f)

theorem TauCeti.GeneralLinear.generatedGroupScheme_def {R : Type u} [CommRing R] (n : ℕ) {ι : Type v} {K : ι → CommHopfAlgCat R} (f : (i : ι) → coordinateHopfAlgebra R n ⟶ K i) : generatedGroupScheme n f = CommHopfAlgCat.quotientSpec (coordinateHopfAlgebra R n) (CommHopfAlgCat.commonKernelHopfIdeal f)

The generated group scheme is the spectrum of the common-kernel Hopf quotient.

noncomputable def TauCeti.GeneralLinear.generatedGroupSchemeι {R : Type u} [CommRing R] (n : ℕ) {ι : Type v} {K : ι → CommHopfAlgCat R} (f : (i : ι) → coordinateHopfAlgebra R n ⟶ K i) : generatedGroupScheme n f ⟶ groupScheme R n

The canonical morphism from the generated subgroup scheme to GLₙ.

Equations

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

theorem TauCeti.GeneralLinear.generatedGroupSchemeι_def {R : Type u} [CommRing R] (n : ℕ) {ι : Type v} {K : ι → CommHopfAlgCat R} (f : (i : ι) → coordinateHopfAlgebra R n ⟶ K i) : generatedGroupSchemeι n f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.quotientSpecι (coordinateHopfAlgebra R n) (CommHopfAlgCat.commonKernelHopfIdeal f)) (CategoryTheory.eqToHom ⋯))

The inclusion of the generated subgroup scheme is the quotient-spectrum inclusion, read through the named presentation of GLₙ.

theorem TauCeti.GeneralLinear.isClosedImmersion_generatedGroupSchemeι_iff {R : Type u} [CommRing R] (n : ℕ) {ι : Type v} {K : ι → CommHopfAlgCat R} (f : (i : ι) → coordinateHopfAlgebra R n ⟶ K i) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (generatedGroupSchemeι n f).hom.hom) ↔ AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (hopfIdealInclusion R n (CommHopfAlgCat.commonKernelHopfIdeal f)).hom.hom)

Closed immersion of the generated-subgroup inclusion reduces to closed immersion of the common-kernel quotient inclusion. This records the definitional transport through generatedGroupScheme_def explicitly for downstream proofs.

instance TauCeti.GeneralLinear.isClosedImmersion_generatedGroupSchemeι {R : Type u} [CommRing R] (n : ℕ) {ι : Type v} {K : ι → CommHopfAlgCat R} (f : (i : ι) → coordinateHopfAlgebra R n ⟶ K i) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (generatedGroupSchemeι n f).hom.hom)

The generated subgroup scheme is a closed subgroup scheme of GLₙ.

noncomputable def TauCeti.GeneralLinear.generatorToGeneratedGroupScheme {R : Type u} [CommRing R] (n : ℕ) {ι : Type v} {K : ι → CommHopfAlgCat R} (f : (i : ι) → coordinateHopfAlgebra R n ⟶ K i) (i : ι) : (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op (K i)) ⟶ generatedGroupScheme n f

The ith generator, factored through the subgroup scheme it generates.

Equations

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

theorem TauCeti.GeneralLinear.generatorToGeneratedGroupScheme_def {R : Type u} [CommRing R] (n : ℕ) {ι : Type v} {K : ι → CommHopfAlgCat R} (f : (i : ι) → coordinateHopfAlgebra R n ⟶ K i) (i : ι) : generatorToGeneratedGroupScheme n f i = CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec ↧R).map (CommHopfAlgCat.commonKernelLift f i).op) (CategoryTheory.eqToHom ⋯)

The generator morphism is induced by the common-kernel factorization.

theorem TauCeti.GeneralLinear.isClosedImmersion_generatorToGeneratedGroupScheme_iff {R : Type u} [CommRing R] (n : ℕ) {ι : Type v} {K : ι → CommHopfAlgCat R} (f : (i : ι) → coordinateHopfAlgebra R n ⟶ K i) (i : ι) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (generatorToGeneratedGroupScheme n f i).hom.hom) ↔ AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left ((AlgebraicGeometry.hopfSpec ↧R).map (CommHopfAlgCat.commonKernelLift f i).op).hom.hom)

Closed immersion of a factored generator reduces to closed immersion of the spectrum map of its common-kernel lift. This records the definitional transport through generatedGroupScheme_def explicitly for downstream proofs.

@[simp]

theorem TauCeti.GeneralLinear.generatorToGeneratedGroupScheme_comp_ι {R : Type u} [CommRing R] (n : ℕ) {ι : Type v} {K : ι → CommHopfAlgCat R} (f : (i : ι) → coordinateHopfAlgebra R n ⟶ K i) (i : ι) : CategoryTheory.CategoryStruct.comp (generatorToGeneratedGroupScheme n f i) (generatedGroupSchemeι n f) = CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec ↧R).map (f i).op) (CategoryTheory.eqToHom ⋯)

Factoring the ith generator through the generated subgroup scheme and then including into GLₙ recovers that generator.

theorem TauCeti.GeneralLinear.isClosedImmersion_generatorToGeneratedGroupScheme_of_surjective {R : Type u} [CommRing R] (n : ℕ) {ι : Type v} {K : ι → CommHopfAlgCat R} (f : (i : ι) → coordinateHopfAlgebra R n ⟶ K i) (i : ι) (hi : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (f i))) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (generatorToGeneratedGroupScheme n f i).hom.hom)

The ith generator is a closed immersion into the generated subgroup scheme whenever its coordinate morphism is surjective.

Matrix-valued points

noncomputable def TauCeti.GeneralLinear.generatedPointsSubgroup {R : Type u} [CommRing R] (n : ℕ) {ι : Type v} {K : ι → CommHopfAlgCat R} (f : (i : ι) → coordinateHopfAlgebra R n ⟶ K i) (A : Type w) [CommRing A] [Algebra R A] : Subgroup (GL (Fin n) A)

The matrix-valued points of the subgroup scheme of GLₙ generated by a family of coordinate morphisms.

Equations

• TauCeti.GeneralLinear.generatedPointsSubgroup n f A = TauCeti.GeneralLinear.hopfIdealPointsSubgroup n (TauCeti.CommHopfAlgCat.commonKernelHopfIdeal f) A

theorem TauCeti.GeneralLinear.generatedPointsSubgroup_def {R : Type u} [CommRing R] (n : ℕ) {ι : Type v} {K : ι → CommHopfAlgCat R} (f : (i : ι) → coordinateHopfAlgebra R n ⟶ K i) (A : Type w) [CommRing A] [Algebra R A] : generatedPointsSubgroup n f A = hopfIdealPointsSubgroup n (CommHopfAlgCat.commonKernelHopfIdeal f) A

The points of the generated subgroup scheme are the matrix points cut out by its defining Hopf ideal.

@[simp]

theorem TauCeti.GeneralLinear.mem_generatedPointsSubgroup_iff {R : Type u} [CommRing R] (n : ℕ) {ι : Type v} {K : ι → CommHopfAlgCat R} (f : (i : ι) → coordinateHopfAlgebra R n ⟶ K i) (A : Type w) [CommRing A] [Algebra R A] (g : GL (Fin n) A) : g ∈ generatedPointsSubgroup n f A ↔ ∀ x ∈ CommHopfAlgCat.commonKernelHopfIdeal f, ((pointsMulEquiv n).symm g).ofConv x = 0

A matrix is a point of the generated subgroup scheme exactly when the corresponding point of O(GLₙ/R) vanishes on the defining Hopf ideal.

theorem TauCeti.GeneralLinear.pointsMulEquiv_mapPointsFunctor_mem_generatedPointsSubgroup {R : Type u} [CommRing R] (n : ℕ) {ι : Type v} {K : ι → CommHopfAlgCat R} (f : (i : ι) → coordinateHopfAlgebra R n ⟶ K i) (i : ι) (A : Type w) [CommRing A] [Algebra R A] (p : ↑(HopfAlgebra.points ↧A)) : (pointsMulEquiv n) ((CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (f i)).app ↧A)) p) ∈ generatedPointsSubgroup n f A

Every matrix coming from a point of one of the generators is a point of the generated subgroup scheme.

theorem TauCeti.GeneralLinear.generatedPointsSubgroup_le_hopfIdealPointsSubgroup {R : Type u} [CommRing R] (n : ℕ) {ι : Type v} {K : ι → CommHopfAlgCat R} (f : (i : ι) → coordinateHopfAlgebra R n ⟶ K i) {J : HopfIdeal R ↑(coordinateHopfAlgebra R n)} (hJ : ∀ (i : ι), J.toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (f i))).toRingHom) (A : Type w) [CommRing A] [Algebra R A] : generatedPointsSubgroup n f A ≤ hopfIdealPointsSubgroup n J A

A Hopf ideal killed by every generator cuts out a point subgroup containing the points of the generated subgroup scheme.