Coordinate compatibility of affine-group-scheme base change

Let H be a commutative Hopf algebra over a commutative ring R, and let S be a commutative R-algebra. There are two constructions of the base-changed affine group scheme: pull back Spec H from Spec R to Spec S, or first extend scalars on coordinates to S ⊗[R] H and then take its Hopf spectrum. This file identifies the two constructions.

The underlying scheme isomorphism is Mathlib's AlgebraicGeometry.pullbackSpecIso', preceded by pullback symmetry so that the new base ring is the left tensor factor. Mathlib also proves that this isomorphism preserves the monoid-object structure. Here it is bundled as an isomorphism of affine group schemes and composed with the established Hopf-spectrum anti-equivalence.

Main declarations

• TauCeti.AffineGroupSchemeCat.hopfSpecBaseChangeIso: pullback of a Hopf spectrum is the Hopf spectrum of the scalar-extended coordinate Hopf algebra.
• TauCeti.AffineGroupSchemeCat.hopfSpecBaseChangeGrpIso_hom_naturality: the underlying group-object comparison intertwines pullback and coordinate scalar extension on morphisms.
• TauCeti.AffineGroupSchemeCat.hopfSpecBaseChangeNatIso: the comparison is natural in the coordinate Hopf algebra.

References

This is the base-change compatibility in the Hopf-algebra/affine-group-scheme dictionary; see J. S. Milne, Algebraic Groups (2017), Section 1.f.

Roadmap

This synchronizes the coordinate and scheme models in the base-change part of Layer 0 of the ReductiveGroups roadmap. In particular, it lets later scheme-side constructions, including the Layer 4 dictionary for groups of multiplicative type, reuse coordinate scalar extension.

theorem TauCeti.AffineGroupSchemeCat.hopfSpecBaseChangeGrpIso_hom_naturality {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] {H K : CommHopfAlgCat R} (f : H ⟶ K) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))).mapGrp.map ((AlgebraicGeometry.hopfSpec ↧R).map f.op)) (hopfSpecBaseChangeGrpIso H).hom = CategoryTheory.CategoryStruct.comp (hopfSpecBaseChangeGrpIso K).hom ((AlgebraicGeometry.hopfSpec ↧S).map (CommHopfAlgCat.baseChangeMap f).op)

The group-object comparison between pullback of Hopf spectra and Hopf spectra of scalar extensions intertwines the pullback of a coordinate morphism with its scalar extension.

noncomputable def TauCeti.AffineGroupSchemeCat.hopfSpecBaseChangeNatIso {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] : (commHopfAlgCatOpEquivAffineGroupSchemeCat ↧R).functor.comp (baseChangeFunctor (CommRingCat.ofHom (algebraMap R S))) ≅ CommHopfAlgCat.baseChangeFunctor.op.comp (commHopfAlgCatOpEquivAffineGroupSchemeCat ↧S).functor

Scheme-theoretic pullback of affine group schemes corresponds naturally, under the Hopf-spectrum anti-equivalence, to scalar extension of their coordinate Hopf algebras.

Equations

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

@[simp]

theorem TauCeti.AffineGroupSchemeCat.hopfSpecBaseChangeNatIso_hom_app {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (H : (CommHopfAlgCat R)ᵒᵖ) : hopfSpecBaseChangeNatIso.hom.app H = (hopfSpecBaseChangeIso (Opposite.unop H)).hom

The forward component of hopfSpecBaseChangeNatIso is hopfSpecBaseChangeIso.

@[simp]

theorem TauCeti.AffineGroupSchemeCat.hopfSpecBaseChangeNatIso_inv_app {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (H : (CommHopfAlgCat R)ᵒᵖ) : hopfSpecBaseChangeNatIso.inv.app H = (hopfSpecBaseChangeIso (Opposite.unop H)).inv

The inverse component of hopfSpecBaseChangeNatIso is the inverse of hopfSpecBaseChangeIso.