Base change of the special orthogonal group

For a morphism of commutative rings R → K, scalar extension of the coordinate Hopf algebra of the standard special orthogonal group SOₙ is canonically the coordinate Hopf algebra constructed directly over K.

The defining ideal is generated by the entries of X Xᵀ - 1 together with det X - 1. The general-linear base-change isomorphism carries both families of generators to their counterparts over K, so the general base-change theorem for Hopf-ideal quotients applies.

Main declarations

• TauCeti.SpecialOrthogonal.coordinateHopfAlgebraBaseChangeIso: base change of the coordinate Hopf algebra of SOₙ.
• baseChangeMap_coordinateMap_comp_coordinateHopfAlgebraBaseChangeIso_hom: compatibility with the quotient coordinate morphisms from O(GLₙ).
• TauCeti.SpecialOrthogonal.finiteTypeCoordinateHopfAlgebraBaseChangeIso: the finite-type form of the same isomorphism.

References

• J. S. Milne, Basic Theory of Affine Group Schemes, Chapter IV, §1.8.
• The Stacks Project, Tags 01JO and 022W.

The quotient-transport construction follows TauCeti.Symplectic.coordinateHopfAlgebraBaseChangeIso, with the orthogonality relations and the determinant-one relation transported together. This is the scalar-extension compatibility needed to formulate geometric connectedness and reductivity of the SOₙ worked example.

@[instance_reducible]

noncomputable def TauCeti.SpecialOrthogonal.instAlgebraXCoordinateHopfAlgebra (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) : Algebra R ↑(GeneralLinear.coordinateHopfAlgebra K n)

The R-algebra structure obtained by restricting the coordinate algebra over K.

Equations

• TauCeti.SpecialOrthogonal.instAlgebraXCoordinateHopfAlgebra R K n = Algebra.compHom (↑(TauCeti.GeneralLinear.coordinateHopfAlgebra K n)) (algebraMap R K)

theorem TauCeti.SpecialOrthogonal.instIsScalarTowerXCoordinateHopfAlgebra (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) : IsScalarTower R K ↑(GeneralLinear.coordinateHopfAlgebra K n)

The coordinate algebra over K is a scalar tower over R → K.

noncomputable def TauCeti.SpecialOrthogonal.coordinateHopfAlgebraBaseChangeIso (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) : CommHopfAlgCat.baseChange (coordinateHopfAlgebra R n) ≅ coordinateHopfAlgebra K n

Base change of the special-orthogonal coordinate Hopf algebra is canonically the special-orthogonal coordinate Hopf algebra over the new base.

Equations

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

@[simp]

theorem TauCeti.SpecialOrthogonal.baseChangeMap_coordinateMap_comp_coordinateHopfAlgebraBaseChangeIso_hom (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap (coordinateMap R n)) (coordinateHopfAlgebraBaseChangeIso R K n).hom = CategoryTheory.CategoryStruct.comp (GeneralLinear.coordinateHopfAlgebraBaseChangeIso R K n).hom (coordinateMap K n)

The special-orthogonal base-change isomorphism is compatible with the quotient coordinate morphisms from the corresponding general-linear coordinate Hopf algebras.

noncomputable def TauCeti.SpecialOrthogonal.finiteTypeCoordinateHopfAlgebraBaseChangeIso (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) : (finiteTypeCoordinateHopfAlgebra R n).baseChange ≅ finiteTypeCoordinateHopfAlgebra K n

The finite-type coordinate Hopf algebra of SOₙ commutes with base change.

Equations

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

@[simp]

theorem TauCeti.SpecialOrthogonal.finiteTypeCoordinateHopfAlgebraBaseChangeIso_hom (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) : (finiteTypeCoordinateHopfAlgebraBaseChangeIso R K n).hom.hom = (CategoryTheory.eqToIso ⋯ ≪≫ coordinateHopfAlgebraBaseChangeIso R K n ≪≫ CategoryTheory.eqToIso ⋯).hom

The underlying commutative-Hopf-algebra morphism of the finite-type base-change isomorphism is the coordinate-Hopf-algebra base-change isomorphism, with the object equalities made explicit.