The orthogonal subgroup scheme of GLₙ

For a commutative ring R and n : ℕ, the orthogonal subgroup scheme Oₙ of GL n is the subgroup scheme preserving the constant form 1: the specialization of TauCeti.ConstantForm at C = 1, cut out of GL n by the entries of

X Xᵀ - 1

for X the localized generic matrix. On every commutative R-algebra A, its group of points is Mathlib's existing group Matrix.orthogonalGroup (Fin n) A of matrices with M * Mᵀ = 1, and that identification is what this file adds to the general construction.

This is the orthogonal group of the standard symmetric bilinear form, the scheme of the functor A ↦ {M | M Mᵀ = 1} over every commutative ring. It is the classical worked example in every characteristic except two, where the bilinear-form and quadratic-form orthogonal groups differ and smoothness becomes sensitive to the rank and regularity of the form; no smoothness is claimed here, so the construction is stated over an arbitrary commutative ring without restriction. This is the ambient stage of the SOₙ worked example of the ReductiveGroups roadmap, built at the same boundary as the symplectic example (TauCeti.Symplectic): construction and points identification, with no smoothness or reductivity claim. The determinant-one cut SOₙ itself is built on top of this file in TauCeti.SpecialOrthogonal.

The Hopf-ideal closure conditions, the quotient, the group scheme with its closed immersion into GLₙ, and the ambient membership criterion M C Mᵀ = C all come from TauCeti.ConstantForm, which proves them for an arbitrary constant matrix C (local finite type is the generic instance for Hopf-ideal quotients of the GLₙ coordinate algebra); the specializations below fix C = 1 and the constant form becomes the identity matrix in every value algebra. The construction includes n = 0 and the zero ring.

Main declarations

• TauCeti.Orthogonal.relationMatrix: the matrix of defining relations X Xᵀ - 1.
• TauCeti.Orthogonal.definingHopfIdeal: the Hopf ideal its entries generate.
• TauCeti.Orthogonal.coordinateHopfAlgebra: the orthogonal coordinate Hopf algebra, the quotient by the defining Hopf ideal.
• TauCeti.Orthogonal.groupScheme and TauCeti.Orthogonal.inclusion: the orthogonal subgroup scheme and its closed immersion into the general linear group scheme.
• TauCeti.Orthogonal.pointsMulEquiv: the group of algebra-valued points of the orthogonal coordinate Hopf algebra is Matrix.orthogonalGroup (Fin n) A.

References

• J. S. Milne, Algebraic Groups (2017), §2.3, where Oₙ is introduced among the basic examples of algebraic groups as the subgroup of GLₙ cut out by the entries of the standard form relation.
• W. C. Waterhouse, Introduction to Affine Group Schemes (1979), Chapter 1, for the orthogonal group as a representable functor on commutative rings.
• The Stacks Project, Tag 022W, for the ambient general linear group scheme.

The orthogonal specialization of the constant-form construction

@[reducible, inline]

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

The matrix of defining relations of the orthogonal subgroup scheme: X Xᵀ - 1 over the coordinate Hopf algebra of GL n, the constant-form relation matrix at C = 1.

Equations

• TauCeti.Orthogonal.relationMatrix R n = TauCeti.ConstantForm.relationMatrix R n 1

@[reducible, inline]

abbrev TauCeti.Orthogonal.relationSet (R : Type u) [CommRing R] (n : ℕ) : Set ↑(GeneralLinear.coordinateHopfAlgebra R n)

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

Equations

• TauCeti.Orthogonal.relationSet R n = TauCeti.ConstantForm.relationSet R n 1

@[reducible, inline]

noncomputable abbrev TauCeti.Orthogonal.definingHopfIdeal (R : Type u) [CommRing R] (n : ℕ) : HopfIdeal R ↑(GeneralLinear.coordinateHopfAlgebra R n)

The orthogonal Hopf ideal: the ideal of the coordinate Hopf algebra of GL n generated by the entries of X Xᵀ - 1.

Equations

• TauCeti.Orthogonal.definingHopfIdeal R n = TauCeti.ConstantForm.definingHopfIdeal R n 1

@[reducible, inline]

noncomputable abbrev TauCeti.Orthogonal.coordinateHopfAlgebra (R : Type u) [CommRing R] (n : ℕ) : CommHopfAlgCat R

The coordinate Hopf algebra of the orthogonal subgroup scheme of GL n.

Equations

• TauCeti.Orthogonal.coordinateHopfAlgebra R n = TauCeti.ConstantForm.coordinateHopfAlgebra R n 1

@[reducible, inline]

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

The orthogonal subgroup scheme of GL n.

Equations

• TauCeti.Orthogonal.groupScheme R n = TauCeti.ConstantForm.groupScheme R n 1

@[reducible, inline]

noncomputable abbrev TauCeti.Orthogonal.inclusion (R : Type u) [CommRing R] (n : ℕ) : groupScheme R n ⟶ GeneralLinear.groupScheme R n

The closed-subgroup inclusion from the orthogonal subgroup scheme into the named general linear group scheme.

Equations

• TauCeti.Orthogonal.inclusion R n = TauCeti.ConstantForm.inclusion R n 1

Algebra-valued points

@[simp]

theorem TauCeti.Orthogonal.mem_definingPointsSubgroup_iff (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] (g : ↑(HopfAlgebra.points ↧A)) : g ∈ CommHopfAlgCat.quotientPointsSubgroup (GeneralLinear.coordinateHopfAlgebra R n) (definingHopfIdeal R n) ↧A ↔ ↑((GeneralLinear.pointsMulEquiv n) g) ∈ Matrix.orthogonalGroup (Fin n) A

An ambient point belongs to the subgroup cut out by the orthogonal Hopf ideal exactly when its matrix is orthogonal. This is the ambient membership criterion that further cuts consume; the determinant-one cut (TauCeti.SpecialOrthogonal) combines it with the special-linear one.

theorem TauCeti.Orthogonal.toUnits_mk (n : ℕ) {A : Type w} [CommRing A] (M : GL (Fin n) A) (h : ↑M ∈ Matrix.orthogonalGroup (Fin n) A) : Unitary.toUnits ⟨↑M, h⟩ = M

The unit attached to an orthogonal matrix wrapped from a general linear element is that element: both have the same underlying matrix.

noncomputable def TauCeti.Orthogonal.pointsMulEquiv (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] : ↑(HopfAlgebra.points ↧A) ≃* ↥(Matrix.orthogonalGroup (Fin n) A)

The points identification: the group of algebra-valued points of the orthogonal coordinate Hopf algebra is the orthogonal group of the value algebra.

Equations

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

theorem TauCeti.Orthogonal.pointsMulEquiv_coe (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] (f : ↑(HopfAlgebra.points ↧A)) : ↑((GeneralLinear.pointsMulEquiv n) ((CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra R n) (definingHopfIdeal R n) ↧A)) f)) = ↑((pointsMulEquiv R n) f)

Under the orthogonal and general-linear point equivalences, the quotient-point inclusion is the ordinary inclusion of orthogonal matrices into GL n.

@[simp]

theorem TauCeti.Orthogonal.quotientPointsHom_pointsMulEquiv_symm (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] (g : ↥(Matrix.orthogonalGroup (Fin n) A)) : (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra R n) (definingHopfIdeal R n) ↧A)) ((pointsMulEquiv R n).symm g) = (GeneralLinear.pointsMulEquiv n).symm (Unitary.toUnits g)

The ambient point attached to an orthogonal matrix is the general-linear point attached to its unit.