Base change of the general linear group scheme

The scheme-theoretic base change of GL_n along a morphism of commutative rings is canonically isomorphic to the general linear group scheme constructed directly over the target ring. This is the scheme-side form of GeneralLinear.coordinateHopfAlgebraBaseChangeIso.

Main declarations

• TauCeti.GeneralLinear.groupSchemeBaseChangeIso: the canonical base-change isomorphism for general linear group schemes.
• TauCeti.GeneralLinear.hopfIdealBaseChangeIso: the corresponding comparison for a closed subgroup presented by compatible Hopf ideals before and after base change.

noncomputable def TauCeti.GeneralLinear.groupSchemeBaseChangeIso (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] (n : ℕ) : (CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))).mapGrp.obj (groupScheme R n) ≅ groupScheme S n

The canonical identification of the base change of GL_n/R with GL_n/S.

Equations

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

Closed subgroups under base change

noncomputable def TauCeti.GeneralLinear.coordinateGroupSchemeBaseChangeIso (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] (n : ℕ) : (CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))).mapGrp.obj ((AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op (coordinateHopfAlgebra R n))) ≅ (AlgebraicGeometry.hopfSpec ↧S).obj (Opposite.op (coordinateHopfAlgebra S n))

The base change of the Hopf spectrum of the coordinate algebra of GL_n/R, expressed as the Hopf spectrum of the coordinate algebra constructed directly over S.

Equations

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

theorem TauCeti.GeneralLinear.groupSchemeBaseChangeIso_hom (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] (n : ℕ) : (groupSchemeBaseChangeIso R S n).hom = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))).mapGrp.map (CategoryTheory.eqToHom ⋯)) (CategoryTheory.CategoryStruct.comp (coordinateGroupSchemeBaseChangeIso R S n).hom (CategoryTheory.eqToHom ⋯))

The forward base-change comparison is the coordinate-presentation comparison, preceded and followed by the named presentations of the source and target general linear group schemes.

noncomputable def TauCeti.GeneralLinear.hopfIdealBaseChangeIso (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] (n : ℕ) (I : HopfIdeal R ↑(coordinateHopfAlgebra R n)) (I' : HopfIdeal S ↑(coordinateHopfAlgebra S n)) (e : CommHopfAlgCat.quotient (coordinateHopfAlgebra S n) I' ≅ CommHopfAlgCat.baseChange (CommHopfAlgCat.quotient (coordinateHopfAlgebra R n) I)) : (CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))).mapGrp.obj (CommHopfAlgCat.quotientSpec (coordinateHopfAlgebra R n) I) ≅ CommHopfAlgCat.quotientSpec (coordinateHopfAlgebra S n) I'

The base change of a closed subgroup presented by a Hopf ideal, transported to a compatible quotient presentation over the target ring.

Equations

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

theorem TauCeti.GeneralLinear.map_quotientSpecι_comp_coordinateGroupSchemeBaseChangeIso (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] (n : ℕ) (I : HopfIdeal R ↑(coordinateHopfAlgebra R n)) (I' : HopfIdeal S ↑(coordinateHopfAlgebra S n)) (e : CommHopfAlgCat.quotient (coordinateHopfAlgebra S n) I' ≅ CommHopfAlgCat.baseChange (CommHopfAlgCat.quotient (coordinateHopfAlgebra R n) I)) (he : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (coordinateHopfAlgebra S n) I') e.hom = CategoryTheory.CategoryStruct.comp (coordinateHopfAlgebraBaseChangeIso R S n).inv (CommHopfAlgCat.baseChangeMap (CommHopfAlgCat.mkQuotient (coordinateHopfAlgebra R n) I))) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))).mapGrp.map (CommHopfAlgCat.quotientSpecι (coordinateHopfAlgebra R n) I)) (coordinateGroupSchemeBaseChangeIso R S n).hom = CategoryTheory.CategoryStruct.comp (hopfIdealBaseChangeIso R S n I I' e).hom (CommHopfAlgCat.quotientSpecι (coordinateHopfAlgebra S n) I')

A compatible quotient presentation identifies the base change of a closed-subgroup inclusion with the closed-subgroup inclusion over the target ring.

theorem TauCeti.GeneralLinear.map_hopfIdealInclusion_comp_groupSchemeBaseChangeIso (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] (n : ℕ) (I : HopfIdeal R ↑(coordinateHopfAlgebra R n)) (I' : HopfIdeal S ↑(coordinateHopfAlgebra S n)) (e : CommHopfAlgCat.quotient (coordinateHopfAlgebra S n) I' ≅ CommHopfAlgCat.baseChange (CommHopfAlgCat.quotient (coordinateHopfAlgebra R n) I)) (he : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (coordinateHopfAlgebra S n) I') e.hom = CategoryTheory.CategoryStruct.comp (coordinateHopfAlgebraBaseChangeIso R S n).inv (CommHopfAlgCat.baseChangeMap (CommHopfAlgCat.mkQuotient (coordinateHopfAlgebra R n) I))) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))).mapGrp.map (hopfIdealInclusion R n I)) (groupSchemeBaseChangeIso R S n).hom = CategoryTheory.CategoryStruct.comp (hopfIdealBaseChangeIso R S n I I' e).hom (hopfIdealInclusion S n I')

Base change carries a Hopf-ideal closed immersion into GL_n/R to the compatible Hopf-ideal closed immersion into GL_n/S.