A generated subgroup scheme of GLₙ inside a constant-multiplication or constant-form subgroup

Fix a commutative ring R, a family of coordinate morphisms f i : O(GLₙ/R) ⟶ K i, and the closed subgroup scheme of GLₙ they generate. Two closed conditions on GLₙ are cut out by an explicit Hopf ideal: preserving a bilinear multiplication with constant structure matrices C : Fin n → Matrix (Fin n) (Fin n) R, and fixing a constant matrix C by the congruence M C Mᵀ = C.

Because the defining ideal of the generated subgroup scheme is the largest Hopf ideal killed by all the f i, each containment is tested on the generators alone: it suffices that the generic matrix of every f i satisfies the relation. On matrix-valued points the containment says that every point of the generated subgroup scheme satisfies the relation, over every R-algebra.

Only the containments are proved. Nothing here asserts that the generated subgroup scheme exhausts the points of the ambient constant-multiplication or constant-form subgroup scheme, nor is any relation asserted between the congruence M C Mᵀ = C and the transposed congruence Mᵀ C M = C, which is a different closed condition.

Main results

In the namespace TauCeti.GeneralLinear:

• constantMultiplicationDefiningHopfIdeal_le_commonKernelHopfIdeal and preserves_of_mem_generatedPointsSubgroup: the containment of Hopf ideals for a constant multiplication and its consequence on matrix points.
• constantFormDefiningHopfIdeal_le_commonKernelHopfIdeal and mul_mul_transpose_of_mem_generatedPointsSubgroup: the same pair for a constant form.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes (1979), §15.1, for a subgroup scheme generated by a family of homomorphisms.
• J. S. Milne, Algebraic Groups (2017), §2.3, for subgroups of GLₙ cut out by matrix relations.

A constant multiplication

theorem TauCeti.GeneralLinear.constantMultiplicationDefiningHopfIdeal_le_commonKernelHopfIdeal {R : Type u} [CommRing R] (n : ℕ) {ι : Type v} {K : ι → CommHopfAlgCat R} (f : (i : ι) → coordinateHopfAlgebra R n ⟶ K i) (C : Fin n → Matrix (Fin n) (Fin n) R) (hf : ∀ (i : ι), ConstantMultiplication.Preserves R n C ((genericMatrix R n).map ⇑↑(CommHopfAlgCat.Hom.hom (f i)))) : ConstantMultiplication.definingHopfIdeal R n C ≤ CommHopfAlgCat.commonKernelHopfIdeal f

The generators of a generated subgroup scheme cut out a multiplication they preserve. If the generic matrix of every generating coordinate morphism preserves the multiplication with structure matrices C, then the Hopf ideal cutting out the subgroup scheme preserving that multiplication is contained in the defining ideal of the generated subgroup scheme.

theorem TauCeti.GeneralLinear.preserves_of_mem_generatedPointsSubgroup {R : Type u} [CommRing R] (n : ℕ) {ι : Type v} {K : ι → CommHopfAlgCat R} (f : (i : ι) → coordinateHopfAlgebra R n ⟶ K i) (C : Fin n → Matrix (Fin n) (Fin n) R) (hf : ∀ (i : ι), ConstantMultiplication.Preserves R n C ((genericMatrix R n).map ⇑↑(CommHopfAlgCat.Hom.hom (f i)))) (A : Type w) [CommRing A] [Algebra R A] {g : GL (Fin n) A} (hg : g ∈ generatedPointsSubgroup n f A) : ConstantMultiplication.Preserves R n C ↑g

Every matrix point of a generated subgroup scheme preserves a multiplication preserved by the generic matrices of its generators.

A constant form

theorem TauCeti.GeneralLinear.constantFormDefiningHopfIdeal_le_commonKernelHopfIdeal {R : Type u} [CommRing R] (n : ℕ) {ι : Type v} {K : ι → CommHopfAlgCat R} (f : (i : ι) → coordinateHopfAlgebra R n ⟶ K i) (C : Matrix (Fin n) (Fin n) R) (hf : ∀ (i : ι), (genericMatrix R n).map ⇑↑(CommHopfAlgCat.Hom.hom (f i)) * C.map ⇑(algebraMap R ↑(K i)) * ((genericMatrix R n).map ⇑↑(CommHopfAlgCat.Hom.hom (f i))).transpose = C.map ⇑(algebraMap R ↑(K i))) : ConstantForm.definingHopfIdeal R n C ≤ CommHopfAlgCat.commonKernelHopfIdeal f

The generators of a generated subgroup scheme cut out a form they fix. If the generic matrix X of every generating coordinate morphism satisfies X C Xᵀ = C, then the Hopf ideal cutting out the subgroup scheme fixing C by congruence is contained in the defining ideal of the generated subgroup scheme.

theorem TauCeti.GeneralLinear.mul_mul_transpose_of_mem_generatedPointsSubgroup {R : Type u} [CommRing R] (n : ℕ) {ι : Type v} {K : ι → CommHopfAlgCat R} (f : (i : ι) → coordinateHopfAlgebra R n ⟶ K i) (C : Matrix (Fin n) (Fin n) R) (hf : ∀ (i : ι), (genericMatrix R n).map ⇑↑(CommHopfAlgCat.Hom.hom (f i)) * C.map ⇑(algebraMap R ↑(K i)) * ((genericMatrix R n).map ⇑↑(CommHopfAlgCat.Hom.hom (f i))).transpose = C.map ⇑(algebraMap R ↑(K i))) (A : Type w) [CommRing A] [Algebra R A] {g : GL (Fin n) A} (hg : g ∈ generatedPointsSubgroup n f A) : ↑g * C.map ⇑(algebraMap R A) * (↑g).transpose = C.map ⇑(algebraMap R A)

Every matrix point of a generated subgroup scheme fixes by congruence a form fixed by the generic matrices of its generators.