Base change of the matrix points cut out by a Hopf ideal

A closed subgroup scheme of GLₙ/A is often built over an extension A of k by a Hopf ideal J of O(GLₙ/A) together with an isomorphism identifying the quotient it cuts out with the scalar extension of the quotient by a Hopf ideal I of O(GLₙ/k). The points of such a presented quotient are already the points of the quotient over k on the value algebra with its scalars restricted to k, by CommHopfAlgCat.baseChangeIsoPointsMulEquiv. This file records that this identification preserves the ambient invertible matrix.

The only input is the commuting square relating the two quotient maps through the general-linear coordinate base-change isomorphism. Nothing here chooses either ideal, so any carrier presented this way — in particular an explicit pinned Chevalley carrier and its scalar extension — can instantiate the result below.

Main declarations

• TauCeti.GeneralLinear.pointsMulEquiv_quotientPointsHom_baseChangeIsoPointsMulEquiv: the presented base-change point equivalence preserves the ambient invertible matrix.

Roadmap

This advances the carrier-independent half of the base-change and points targets in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, whose consumer is milestone L0 of TauCetiRoadmap/CFSGStatement/README.md. It identifies no particular carrier with the pinned simply connected group.

theorem TauCeti.GeneralLinear.pointsMulEquiv_quotientPointsHom_baseChangeIsoPointsMulEquiv {k : Type u} [CommRing k] {A : Type (max u v)} [CommRing A] [Algebra k A] (n : ℕ) (I : HopfIdeal k ↑(coordinateHopfAlgebra k n)) (J : HopfIdeal A ↑(coordinateHopfAlgebra A n)) (e : CommHopfAlgCat.quotient (coordinateHopfAlgebra A n) J ≅ CommHopfAlgCat.baseChange (CommHopfAlgCat.quotient (coordinateHopfAlgebra k n) I)) (he : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (coordinateHopfAlgebra A n) J) e.hom = CategoryTheory.CategoryStruct.comp (coordinateHopfAlgebraBaseChangeIso k A n).inv (CommHopfAlgCat.baseChangeMap (CommHopfAlgCat.mkQuotient (coordinateHopfAlgebra k n) I))) (B : CommAlgCat A) (q : ↑(HopfAlgebra.points B)) : (pointsMulEquiv n) ((CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (coordinateHopfAlgebra k n) I (CommAlgCat.restrictScalarsObj (algebraMap k A) B))) ((CommHopfAlgCat.baseChangeIsoPointsMulEquiv e B) q)) = (pointsMulEquiv n) ((CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (coordinateHopfAlgebra A n) J B)) q)

The presented base-change point equivalence preserves the ambient invertible matrix. Both sides read the same matrix over the value algebra, one through the quotient over k and one through the quotient over A.