The subgroup scheme of GLₙ preserving a constant matrix

For a commutative ring R, a natural number n, and a constant matrix C : Matrix (Fin n) (Fin n) R, the entries of the matrix relation

X C Xᵀ - C

— X the localized generic matrix of GL n, C read in the coordinate Hopf algebra through the structure morphism — generate a Hopf ideal in the coordinate Hopf algebra of GL n. Its quotient represents the closed subgroup scheme of GL n preserving C. On every commutative R-algebra A, its points are the invertible matrices M with M C Mᵀ = C.

Nothing is assumed of C: it is an arbitrary square matrix over the base, not required to be invertible, symmetric, alternating, or nondegenerate, and the construction includes n = 0 and the zero ring. The classical families are the specializations at a constant form: TauCeti.Orthogonal takes C = 1 and TauCeti.Symplectic takes C = Jₘ, each adding its own identification of the points with the corresponding matrix group. This file supplies everything those specializations share: the relation matrix, the Hopf ideal with its three closure conditions, the quotient, the group scheme with its closed immersion into GLₙ, and the ambient membership criterion M C Mᵀ = C; local finite type comes from the generic GeneralLinear.locallyOfFiniteType_hopfIdealQuotientSpec instance, which applies to the reducible groupScheme directly.

The three Hopf-ideal closure conditions are proved by matrix algebra rather than coordinate by coordinate. Writing f := X C Xᵀ - C for the matrix of generators and mapping it entrywise through the relevant algebra morphisms — each of which fixes C, being an R-algebra morphism:

• the counit sends X to the identity matrix, so it sends f to 1 C 1ᵀ - C = 0;

• the comultiplication sends X to Y Z, where Y and Z are the two tensor inclusions of X, and

  (Y Z) C (Y Z)ᵀ - C = Y (Z C Zᵀ - C) Yᵀ + (Y C Yᵀ - C),
  

  whose two summands are the right and left tensor inclusions of f framed by matrices, so every entry lies in the right or left tensor ideal;

• the antipode sends X to its inverse matrix, and

  X⁻¹ C (X⁻¹)ᵀ - C = -(X⁻¹ (X C Xᵀ - C) (X⁻¹)ᵀ),
  

  so every entry of the antipode image is a combination of the generators.

That each identity holds for an arbitrary constant C is what makes the classical examples specializations rather than separate constructions: no step inverts C, transposes it, or uses a relation between C and Cᵀ.

Main declarations

• TauCeti.ConstantForm.relationMatrix: the matrix of defining relations X C Xᵀ - C.
• TauCeti.ConstantForm.definingHopfIdeal_toIdeal_le_ker_of_map_genericMatrix_mul_mul_transpose: a coordinate morphism whose generic matrix X satisfies X C Xᵀ = C kills the defining ideal.
• TauCeti.ConstantForm.definingHopfIdeal: the Hopf ideal its entries generate.
• TauCeti.ConstantForm.coordinateHopfAlgebra and TauCeti.ConstantForm.coordinateMap: the quotient coordinate Hopf algebra and the quotient morphism onto it.
• TauCeti.ConstantForm.groupScheme and TauCeti.ConstantForm.inclusion: the subgroup scheme preserving C and its closed immersion into the general linear group scheme — the generic GeneralLinear.hopfIdealInclusion at the defining Hopf ideal — with groupScheme_def and inclusion_def exposing the quotient-spectrum presentations.
• TauCeti.ConstantForm.mem_definingPointsSubgroup_iff: an ambient point is cut out exactly when its matrix M satisfies M C Mᵀ = C.

References

• J. S. Milne, Algebraic Groups (2017), §2.3, where the orthogonal and symplectic groups are introduced as the subgroups of GLₙ cut out by the entries of a form relation.
• W. C. Waterhouse, Introduction to Affine Group Schemes (1979), Chapter 1, for such groups as representable functors on commutative rings.
• The Stacks Project, Tag 022W, for the ambient general linear group scheme.

The matrix form of the closure computations is standard, and the framing identities above are not adapted from either reference. The proofs themselves are those of the merged worked examples TauCeti.Symplectic (for C = Jₘ) and TauCeti.Orthogonal (for C = 1), generalized here to an arbitrary C: the declaration order and proof plan are theirs, and those two files now consume this one rather than repeating it. TauCeti.Symplectic recorded the generalization in its own module docstring — that the computations "apply verbatim to X C Xᵀ - C for any constant matrix C" — before it was carried out.

The defining relation matrix

noncomputable def TauCeti.ConstantForm.relationMatrix (R : Type u) [CommRing R] (n : ℕ) (C : Matrix (Fin n) (Fin n) R) : Matrix (Fin n) (Fin n) ↑(GeneralLinear.coordinateHopfAlgebra R n)

The matrix of defining relations of the subgroup scheme preserving C: X C Xᵀ - C over the coordinate Hopf algebra of GL n.

Equations

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

theorem TauCeti.ConstantForm.relationMatrix_def (R : Type u) [CommRing R] (n : ℕ) (C : Matrix (Fin n) (Fin n) R) : relationMatrix R n C = GeneralLinear.genericMatrix R n * C.map ⇑(algebraMap R ↑(GeneralLinear.coordinateHopfAlgebra R n)) * (GeneralLinear.genericMatrix R n).transpose - C.map ⇑(algebraMap R ↑(GeneralLinear.coordinateHopfAlgebra R n))

The relation matrix is the constant form transported by the generic matrix, minus the form: X C Xᵀ - C.

def TauCeti.ConstantForm.relationSet (R : Type u) [CommRing R] (n : ℕ) (C : Matrix (Fin n) (Fin n) R) : Set ↑(GeneralLinear.coordinateHopfAlgebra R n)

The set of defining relations: the entries of the relation matrix.

Equations

• TauCeti.ConstantForm.relationSet R n C = Set.range fun (ij : Fin n × Fin n) => TauCeti.ConstantForm.relationMatrix R n C ij.1 ij.2

theorem TauCeti.ConstantForm.relationMatrix_mem_relationSet (R : Type u) [CommRing R] (n : ℕ) (C : Matrix (Fin n) (Fin n) R) (i j : Fin n) : relationMatrix R n C i j ∈ relationSet R n C

Every entry of the relation matrix is a defining relation.

@[simp]

theorem TauCeti.ConstantForm.mem_relationSet_iff (R : Type u) [CommRing R] (n : ℕ) (C : Matrix (Fin n) (Fin n) R) {x : ↑(GeneralLinear.coordinateHopfAlgebra R n)} : x ∈ relationSet R n C ↔ ∃ (i : Fin n) (j : Fin n), relationMatrix R n C i j = x

An element is a defining relation exactly when it is an entry of the relation matrix.

@[simp]

theorem TauCeti.ConstantForm.relationMatrix_map (R : Type u) [CommRing R] (n : ℕ) (C : Matrix (Fin n) (Fin n) R) {T : Type u_1} [CommRing T] [Algebra R T] (phi : ↑(GeneralLinear.coordinateHopfAlgebra R n) →ₐ[R] T) : (relationMatrix R n C).map ⇑phi = (GeneralLinear.genericMatrix R n).map ⇑phi * C.map ⇑(algebraMap R T) * ((GeneralLinear.genericMatrix R n).map ⇑phi).transpose - C.map ⇑(algebraMap R T)

Mapping the relation matrix through an algebra morphism gives the relation of the images: the generic matrix maps entrywise, and the constant form maps to the constant form.

The three Hopf-ideal closure conditions

The defining Hopf ideal and quotient

noncomputable def TauCeti.ConstantForm.definingHopfIdeal (R : Type u) [CommRing R] (n : ℕ) (C : Matrix (Fin n) (Fin n) R) : HopfIdeal R ↑(GeneralLinear.coordinateHopfAlgebra R n)

The Hopf ideal preserving C: the ideal of the coordinate Hopf algebra of GL n generated by the entries of X C Xᵀ - C, with the three closure conditions extended from the generators across the span.

Equations

• TauCeti.ConstantForm.definingHopfIdeal R n C = TauCeti.HopfIdeal.ofSpan (TauCeti.ConstantForm.relationSet R n C) ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.ConstantForm.definingHopfIdeal_toIdeal (R : Type u) [CommRing R] (n : ℕ) (C : Matrix (Fin n) (Fin n) R) : (definingHopfIdeal R n C).toIdeal = Ideal.span (relationSet R n C)

The underlying ideal of the defining Hopf ideal is the span of the defining relations.

theorem TauCeti.ConstantForm.definingHopfIdeal_toIdeal_le_ker_of_map_genericMatrix_mul_mul_transpose (R : Type u) [CommRing R] (n : ℕ) (C : Matrix (Fin n) (Fin n) R) {T : Type u_1} [CommRing T] [Algebra R T] (phi : ↑(GeneralLinear.coordinateHopfAlgebra R n) →ₐ[R] T) (hphi : (GeneralLinear.genericMatrix R n).map ⇑phi * C.map ⇑(algebraMap R T) * ((GeneralLinear.genericMatrix R n).map ⇑phi).transpose = C.map ⇑(algebraMap R T)) : (definingHopfIdeal R n C).toIdeal ≤ RingHom.ker ↑phi

A coordinate morphism whose generic matrix X satisfies X C Xᵀ = C kills the defining ideal. This is the criterion by which a subgroup of GL n given by generating morphisms is shown to lie in the subgroup scheme preserving C: it suffices to evaluate the form relation on the generic matrix of each generator.

@[reducible, inline]

noncomputable abbrev TauCeti.ConstantForm.coordinateHopfAlgebra (R : Type u) [CommRing R] (n : ℕ) (C : Matrix (Fin n) (Fin n) R) : CommHopfAlgCat R

The coordinate Hopf algebra of the subgroup scheme of GL n preserving C.

Equations

• TauCeti.ConstantForm.coordinateHopfAlgebra R n C = TauCeti.CommHopfAlgCat.quotient (TauCeti.GeneralLinear.coordinateHopfAlgebra R n) (TauCeti.ConstantForm.definingHopfIdeal R n C)

noncomputable def TauCeti.ConstantForm.coordinateMap (R : Type u) [CommRing R] (n : ℕ) (C : Matrix (Fin n) (Fin n) R) : GeneralLinear.coordinateHopfAlgebra R n ⟶ coordinateHopfAlgebra R n C

The quotient coordinate morphism from O(GL n) to the coordinate Hopf algebra of the subgroup scheme preserving C.

Equations

• TauCeti.ConstantForm.coordinateMap R n C = TauCeti.CommHopfAlgCat.mkQuotient (TauCeti.GeneralLinear.coordinateHopfAlgebra R n) (TauCeti.ConstantForm.definingHopfIdeal R n C)

theorem TauCeti.ConstantForm.coordinateMap_def (R : Type u) [CommRing R] (n : ℕ) (C : Matrix (Fin n) (Fin n) R) : coordinateMap R n C = CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra R n) (definingHopfIdeal R n C)

The coordinate map is the canonical quotient morphism by the defining Hopf ideal.

theorem TauCeti.ConstantForm.coordinateMap_apply (R : Type u) [CommRing R] (n : ℕ) (C : Matrix (Fin n) (Fin n) R) (h : ↑(GeneralLinear.coordinateHopfAlgebra R n)) : (CommHopfAlgCat.Hom.hom (coordinateMap R n C)) h = (Ideal.Quotient.mkₐ R (definingHopfIdeal R n C).toIdeal) h

The coordinate morphism sends an ambient coordinate to its quotient class.

@[simp]

theorem TauCeti.ConstantForm.coordinateMap_relationMatrix (R : Type u) [CommRing R] (n : ℕ) (C : Matrix (Fin n) (Fin n) R) (i j : Fin n) : (CommHopfAlgCat.Hom.hom (coordinateMap R n C)) (relationMatrix R n C i j) = 0

Every defining relation vanishes in the quotient coordinate Hopf algebra.

The group scheme and its closed immersion

@[reducible, inline]

noncomputable abbrev TauCeti.ConstantForm.groupScheme (R : Type u) [CommRing R] (n : ℕ) (C : Matrix (Fin n) (Fin n) R) : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))

The subgroup scheme of GL n preserving C.

Equations

• TauCeti.ConstantForm.groupScheme R n C = TauCeti.CommHopfAlgCat.quotientSpec (TauCeti.GeneralLinear.coordinateHopfAlgebra R n) (TauCeti.ConstantForm.definingHopfIdeal R n C)

theorem TauCeti.ConstantForm.groupScheme_def (R : Type u) [CommRing R] (n : ℕ) (C : Matrix (Fin n) (Fin n) R) : groupScheme R n C = CommHopfAlgCat.quotientSpec (GeneralLinear.coordinateHopfAlgebra R n) (definingHopfIdeal R n C)

The subgroup scheme preserving C is the quotient spectrum of its coordinate Hopf algebra.

noncomputable def TauCeti.ConstantForm.inclusion (R : Type u) [CommRing R] (n : ℕ) (C : Matrix (Fin n) (Fin n) R) : groupScheme R n C ⟶ GeneralLinear.groupScheme R n

The closed-subgroup inclusion into the named general linear group scheme: the generic Hopf-ideal closed immersion GeneralLinear.hopfIdealInclusion at the defining Hopf ideal.

Equations

• TauCeti.ConstantForm.inclusion R n C = TauCeti.GeneralLinear.hopfIdealInclusion R n (TauCeti.ConstantForm.definingHopfIdeal R n C)

theorem TauCeti.ConstantForm.inclusion_def (R : Type u) [CommRing R] (n : ℕ) (C : Matrix (Fin n) (Fin n) R) : inclusion R n C = GeneralLinear.hopfIdealInclusion R n (definingHopfIdeal R n C)

The inclusion is the generic Hopf-ideal closed immersion at the defining Hopf ideal.

theorem TauCeti.ConstantForm.inclusion_eq_eqToHom_comp_hopfSpec_map (R : Type u) [CommRing R] (n : ℕ) (C : Matrix (Fin n) (Fin n) R) : inclusion R n C = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec ↧R).map (coordinateMap R n C).op) (CategoryTheory.eqToHom ⋯))

The constant-form inclusion expressed through the quotient-spectrum presentations of its source and the ambient general linear group.

instance TauCeti.ConstantForm.isClosedImmersion_inclusion (R : Type u) [CommRing R] (n : ℕ) (C : Matrix (Fin n) (Fin n) R) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (inclusion R n C).hom.hom)

The inclusion into the named general linear group scheme is a closed immersion.

noncomputable def TauCeti.ConstantForm.finiteTypeCoordinateHopfAlgebra (R : Type u) [CommRing R] (n : ℕ) (C : Matrix (Fin n) (Fin n) R) : FiniteTypeCommHopfAlgCat R

The quotient coordinate Hopf algebra, bundled with its finite-type property.

Equations

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

@[simp]

theorem TauCeti.ConstantForm.finiteTypeCoordinateHopfAlgebra_obj (R : Type u) [CommRing R] (n : ℕ) (C : Matrix (Fin n) (Fin n) R) : (finiteTypeCoordinateHopfAlgebra R n C).obj = coordinateHopfAlgebra R n C

The finite-type package has the quotient coordinate Hopf algebra as its underlying object.

Algebra-valued points

theorem TauCeti.ConstantForm.mapPointsFunctor_coordinateMap_app (R : Type u) [CommRing R] (n : ℕ) (C : Matrix (Fin n) (Fin n) R) {A : Type w} [CommRing A] [Algebra R A] (f : ↑(HopfAlgebra.points ↧A)) : (CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (coordinateMap R n C)).app ↧A)) f = (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra R n) (definingHopfIdeal R n C) ↧A)) f

Mapping a point along the quotient coordinate morphism gives its ambient general-linear point. CommHopfAlgCat.quotientPointsHom is by definition the points map induced by the quotient morphism, so this is coordinateMap_def read on points; it is stated here to glue the two applied forms at a value algebra.

theorem TauCeti.ConstantForm.mem_definingPointsSubgroup_iff (R : Type u) [CommRing R] (n : ℕ) (C : Matrix (Fin n) (Fin n) R) {A : Type w} [CommRing A] [Algebra R A] (g : ↑(HopfAlgebra.points ↧A)) : g ∈ CommHopfAlgCat.quotientPointsSubgroup (GeneralLinear.coordinateHopfAlgebra R n) (definingHopfIdeal R n C) ↧A ↔ ↑((GeneralLinear.pointsMulEquiv n) g) * C.map ⇑(algebraMap R A) * (↑((GeneralLinear.pointsMulEquiv n) g)).transpose = C.map ⇑(algebraMap R A)

The ambient membership criterion: an ambient point belongs to the subgroup cut out by the defining Hopf ideal exactly when its matrix M satisfies M C Mᵀ = C.

This is the criterion the classical specializations consume: TauCeti.Orthogonal restates it as membership in Matrix.orthogonalGroup (the simp normal form there), while TauCeti.Symplectic uses it internally to build its points identification. It is deliberately not a simp lemma — the orthogonal restatement is the normal form a user wants on that side, and the symplectic side rewrites with it explicitly.