The special orthogonal subgroup scheme of GLₙ

For a commutative ring R and n : ℕ, the special orthogonal subgroup scheme SOₙ is cut out of GL n by the join of two Hopf ideals that already exist:

• the orthogonal Hopf ideal, generated by the entries of X Xᵀ - 1 (TauCeti.Orthogonal.definingHopfIdeal), and
• the determinant kernel, the principal ideal generated by det X - 1 (TauCeti.SpecialLinear.definingHopfIdeal).

No new closure computation is needed: the join of Hopf ideals is a Hopf ideal, and its quotient imposes both families of relations at once — on points, the intersection Oₙ ∩ SLₙ inside GL n. On every commutative R-algebra A, the group of points is Mathlib's group Matrix.specialOrthogonalGroup (Fin n) A of orthogonal matrices of determinant one, because a point vanishes on the join exactly when it vanishes on both joinands (TauCeti.CommHopfAlgCat.quotientPointsSubgroup_sup), and the two ambient membership criteria are already identified with orthogonality and determinant one.

As with the orthogonal construction, this is the special orthogonal group of the standard symmetric bilinear form: the scheme of the functor A ↦ {M | M Mᵀ = 1, det M = 1} over every commutative ring. In characteristic two the quadratic-form special orthogonal group (cut out by the Dickson invariant rather than the determinant) differs from this determinant-one cut, 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 completes the construction-and-points boundary of the SOₙ worked example of the ReductiveGroups roadmap, at the same stage as the symplectic example: construction and points identification, with no smoothness or reductivity claim.

Main declarations

• TauCeti.SpecialOrthogonal.definingHopfIdeal: the join of the orthogonal Hopf ideal and the determinant kernel.
• TauCeti.SpecialOrthogonal.coordinateHopfAlgebra: the special orthogonal coordinate Hopf algebra, the quotient by the defining Hopf ideal.
• TauCeti.SpecialOrthogonal.groupScheme and TauCeti.SpecialOrthogonal.inclusion: the special orthogonal subgroup scheme and its closed immersion into the general linear group scheme.
• TauCeti.SpecialOrthogonal.pointsMulEquiv: the group of algebra-valued points of the special orthogonal coordinate Hopf algebra is Matrix.specialOrthogonalGroup (Fin n) A.
• TauCeti.SpecialOrthogonal.pointsMulEquiv_mapValue: this points identification is natural in the value algebra.

References

• J. S. Milne, Algebraic Groups (2017), §2.3, where SOₙ appears among the basic examples of algebraic groups as the intersection of Oₙ with SLₙ inside GLₙ.
• The Stacks Project, Tag 022W, for the ambient general linear group scheme.

The construction is assembled entirely from the orthogonal and special-linear Hopf ideals of TauCeti.Orthogonal and TauCeti.SpecialLinear through the Hopf-ideal join.

The defining Hopf ideal and quotient

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

The special orthogonal Hopf ideal: the join of the orthogonal Hopf ideal and the determinant kernel in the coordinate Hopf algebra of GL n.

Equations

• TauCeti.SpecialOrthogonal.definingHopfIdeal R n = TauCeti.Orthogonal.definingHopfIdeal R n ⊔ TauCeti.SpecialLinear.definingHopfIdeal R n

@[simp]

theorem TauCeti.SpecialOrthogonal.definingHopfIdeal_toIdeal (R : Type u) [CommRing R] (n : ℕ) : (definingHopfIdeal R n).toIdeal = Ideal.span (Orthogonal.relationSet R n) ⊔ Ideal.span {↑(GeneralLinear.determinantGroupLike R n) - 1}

The underlying ideal of the special orthogonal Hopf ideal is generated by the orthogonality relations together with the localized generic determinant minus one.

@[reducible, inline]

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

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

Equations

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

noncomputable def TauCeti.SpecialOrthogonal.coordinateMap (R : Type u) [CommRing R] (n : ℕ) : GeneralLinear.coordinateHopfAlgebra R n ⟶ coordinateHopfAlgebra R n

The quotient coordinate morphism from O(GL n) to the special orthogonal coordinate Hopf algebra.

Equations

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

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

The special orthogonal coordinate morphism is the quotient by its defining Hopf ideal.

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

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

@[simp]

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

Every orthogonality relation vanishes in the special orthogonal coordinate Hopf algebra.

@[simp]

theorem TauCeti.SpecialOrthogonal.coordinateMap_determinantGroupLike (R : Type u) [CommRing R] (n : ℕ) : (CommHopfAlgCat.Hom.hom (coordinateMap R n)) ↑(GeneralLinear.determinantGroupLike R n) = 1

The generic determinant maps to one in the special orthogonal coordinate Hopf algebra.

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

The special orthogonal subgroup scheme of GL n.

Equations

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

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

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

Equations

• TauCeti.SpecialOrthogonal.inclusion R n = CategoryTheory.CategoryStruct.comp (TauCeti.SpecialOrthogonal.groupSchemeι✝ R n) (CategoryTheory.eqToIso ⋯).hom

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

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

noncomputable def TauCeti.SpecialOrthogonal.finiteTypeCoordinateHopfAlgebra (R : Type u) [CommRing R] (n : ℕ) : FiniteTypeCommHopfAlgCat R

The special orthogonal 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.SpecialOrthogonal.finiteTypeCoordinateHopfAlgebra_obj (R : Type u) [CommRing R] (n : ℕ) : (finiteTypeCoordinateHopfAlgebra R n).obj = coordinateHopfAlgebra R n

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

instance TauCeti.SpecialOrthogonal.locallyOfFiniteType_groupScheme (R : Type u) [CommRing R] (n : ℕ) : AlgebraicGeometry.LocallyOfFiniteType (groupScheme R n).X.hom

The structural morphism of the special orthogonal subgroup scheme is locally of finite type.

Algebra-valued points

@[simp]

theorem TauCeti.SpecialOrthogonal.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.specialOrthogonalGroup (Fin n) A

An ambient point belongs to the subgroup cut out by the special orthogonal Hopf ideal exactly when its matrix is orthogonal of determinant one.

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

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

Equations

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

theorem TauCeti.SpecialOrthogonal.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 special orthogonal and general-linear point equivalences, the quotient-point inclusion is the ordinary inclusion of special orthogonal matrices into GL n.

theorem TauCeti.SpecialOrthogonal.pointsMulEquiv_mapValue (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] {B : Type v} [CommRing B] [Algebra R B] (phi : A →ₐ[R] B) (f : WithConv (↑(coordinateHopfAlgebra R n) →ₐ[R] A)) : (pointsMulEquiv R n) ((AlgHom.mapValue phi) f) = (Matrix.SpecialOrthogonalGroup.map ↑phi) ((pointsMulEquiv R n) f)

The matrix description of special orthogonal points is natural under algebra maps.

theorem TauCeti.SpecialOrthogonal.mapValue_pointsMulEquiv_symm_apply (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] {B : Type v} [CommRing B] [Algebra R B] (phi : A →ₐ[R] B) (g : ↥(Matrix.specialOrthogonalGroup (Fin n) A)) : (AlgHom.mapValue phi) ((pointsMulEquiv R n).symm g) = (pointsMulEquiv R n).symm ((Matrix.SpecialOrthogonalGroup.map phi.toRingHom) g)

Naturality of the inverse pointwise equivalence in the value algebra.

@[simp]

theorem TauCeti.SpecialOrthogonal.quotientPointsHom_pointsMulEquiv_symm (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] (g : ↥(Matrix.specialOrthogonalGroup (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 a special orthogonal matrix is the general-linear point attached to the unit of its orthogonal part.