Base change of affine group schemes

Pullback along Spec S ⟶ Spec R carries an affine group scheme over Spec R to an affine group scheme over Spec S. This file bundles that construction on objects and morphisms as TauCeti.AffineGroupSchemeCat.baseChangeFunctor, and records comparison isomorphisms for base change along the identity ring map and along a composite ring map. The mutual coherence conditions of those two comparisons — the unit and associativity constraints that would make R ↦ AffineGroupSchemeCat R a pseudofunctor — are not proved here.

The group structure is transported by Mathlib's left-exact pullback functor on Over categories. Affineness is preserved because the base Spec R is itself affine: a fibre product of affine schemes over an affine base is again affine, so the fibre product of G with Spec S over Spec R is affine. (Over a general base scheme this argument is unavailable, and a fibre product of affine schemes need not be affine.) Thus the construction applies over general commutative rings; no field or finite-type hypothesis is needed.

Main declarations

• TauCeti.AffineGroupSchemeCat.baseChange: base change of one affine group scheme.
• TauCeti.AffineGroupSchemeCat.baseChangeMap: base change of a morphism.
• TauCeti.AffineGroupSchemeCat.baseChangeFunctor: functorial base change.
• TauCeti.AffineGroupSchemeCat.baseChangeFunctorIdIso, TauCeti.AffineGroupSchemeCat.baseChangeFunctorCompIso: base change along the identity ring map is the identity, and base change along a composite is the composite of base changes. Their components are computed by simp lemmas in terms of the underlying comparisons TauCeti.AlgebraicGeometry.Over.pullbackSpecMapId and TauCeti.AlgebraicGeometry.Over.pullbackSpecMapComp of pullback functors.
• TauCeti.AffineGroupSchemeCat.hopfSpecBaseChangeGrpIso and TauCeti.AffineGroupSchemeCat.hopfSpecBaseChangeIso: base change of a Hopf spectrum agrees with scalar extension of its coordinate Hopf algebra, first for group objects and then through the affine-group-scheme anti-equivalence.

The comparison with base change of coordinate Hopf algebras is developed in TauCeti.AlgebraicGeometry.AffineGroupScheme.BaseChange.Coordinate.

References

The coordinate-algebra counterpart of this construction, base change of commutative Hopf algebras, is TauCeti.CommHopfAlgCat.baseChangeFunctor; the two sides are related by the anti-equivalence TauCeti.commHopfAlgCatOpEquivAffineGroupSchemeCat. hopfSpecBaseChangeIso identifies their values on each Hopf algebra. Their natural compatibility is developed in TauCeti.AlgebraicGeometry.AffineGroupScheme.BaseChange.Coordinate as TauCeti.AffineGroupSchemeCat.hopfSpecBaseChangeNatIso.

Roadmap

This supplies the scheme-side base-change operation required by Layer 9 of the ReductiveGroups roadmap. The CFSGStatement roadmap's milestone L0 uses it to evaluate a pinned Chevalley--Demazure group scheme over ℤ after extension to an algebraic closure of a finite prime field.

@[reducible, inline]

noncomputable abbrev TauCeti.AffineGroupSchemeCat.baseChange {R S : CommRingCat} (f : R ⟶ S) (G : AffineGroupSchemeCat R) : AffineGroupSchemeCat S

Base change of an affine group scheme along a morphism f : R ⟶ S of commutative rings.

Its underlying scheme is the fibre product with Spec S over Spec R, and its group-object structure is the one transported by pullback.

Equations

• TauCeti.AffineGroupSchemeCat.baseChange f G = { obj := (CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map f)).mapGrp.obj G.obj, property := ⋯ }

@[simp]

theorem TauCeti.AffineGroupSchemeCat.baseChange_obj {R S : CommRingCat} (f : R ⟶ S) (G : AffineGroupSchemeCat R) : (baseChange f G).obj = (CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map f)).mapGrp.obj G.obj

The underlying group object of a base-changed affine group scheme is obtained by applying pullback to the original group object.

theorem TauCeti.AffineGroupSchemeCat.baseChange_obj_X {R S : CommRingCat} (f : R ⟶ S) (G : AffineGroupSchemeCat R) : (baseChange f G).obj.X = (CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map f)).obj G.obj.X

The underlying object over Spec S of a base-changed affine group scheme is the pullback of the original object over Spec R.

theorem TauCeti.AffineGroupSchemeCat.baseChange_obj_X_left {R S : CommRingCat} (f : R ⟶ S) (G : AffineGroupSchemeCat R) : (baseChange f G).obj.X.left = CategoryTheory.Limits.pullback G.obj.X.hom (AlgebraicGeometry.Spec.map f)

The underlying scheme of a base-changed affine group scheme is the corresponding fibre product.

@[reducible, inline]

noncomputable abbrev TauCeti.AffineGroupSchemeCat.baseChangeMap {R S : CommRingCat} (f : R ⟶ S) {G H : AffineGroupSchemeCat R} (g : G ⟶ H) : baseChange f G ⟶ baseChange f H

Base change of a morphism of affine group schemes.

Equations

• TauCeti.AffineGroupSchemeCat.baseChangeMap f g = CategoryTheory.ObjectProperty.homMk ((CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map f)).mapGrp.map g.hom)

@[simp]

theorem TauCeti.AffineGroupSchemeCat.hom_baseChangeMap {R S : CommRingCat} (f : R ⟶ S) {G H : AffineGroupSchemeCat R} (g : G ⟶ H) : (baseChangeMap f g).hom = (CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map f)).mapGrp.map g.hom

The underlying group-object morphism of baseChangeMap is obtained by applying pullback.

noncomputable def TauCeti.AffineGroupSchemeCat.baseChangeFunctor {R S : CommRingCat} (f : R ⟶ S) : CategoryTheory.Functor (AffineGroupSchemeCat R) (AffineGroupSchemeCat S)

Pullback along Spec S ⟶ Spec R defines a functor from affine group schemes over Spec R to affine group schemes over Spec S.

Equations

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

@[simp]

theorem TauCeti.AffineGroupSchemeCat.baseChangeFunctor_obj {R S : CommRingCat} (f : R ⟶ S) (G : AffineGroupSchemeCat R) : (baseChangeFunctor f).obj G = baseChange f G

The object part of baseChangeFunctor is base change of affine group schemes.

@[simp]

theorem TauCeti.AffineGroupSchemeCat.baseChangeFunctor_map {R S : CommRingCat} (f : R ⟶ S) {G H : AffineGroupSchemeCat R} (g : G ⟶ H) : (baseChangeFunctor f).map g = baseChangeMap f g

The morphism part of baseChangeFunctor is base change of affine-group-scheme morphisms.

noncomputable def TauCeti.AffineGroupSchemeCat.baseChangeFunctorIdIso {R : CommRingCat} : baseChangeFunctor (CategoryTheory.CategoryStruct.id R) ≅ CategoryTheory.Functor.id (AffineGroupSchemeCat R)

Base change along the identity of R is the identity functor on affine group schemes over Spec R.

Equations

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

@[simp]

theorem TauCeti.AffineGroupSchemeCat.baseChangeFunctorIdIso_hom_app_hom_hom_hom {R : CommRingCat} (G : AffineGroupSchemeCat R) : (baseChangeFunctorIdIso.hom.app G).hom.hom.hom = AlgebraicGeometry.Over.pullbackSpecMapId.hom.app G.obj.X

The morphism of objects over Spec R underlying baseChangeFunctorIdIso.hom.

@[simp]

theorem TauCeti.AffineGroupSchemeCat.baseChangeFunctorIdIso_inv_app_hom_hom_hom {R : CommRingCat} (G : AffineGroupSchemeCat R) : (baseChangeFunctorIdIso.inv.app G).hom.hom.hom = AlgebraicGeometry.Over.pullbackSpecMapId.inv.app G.obj.X

The morphism of objects over Spec R underlying baseChangeFunctorIdIso.inv.

noncomputable def TauCeti.AffineGroupSchemeCat.baseChangeFunctorCompIso {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) : baseChangeFunctor (CategoryTheory.CategoryStruct.comp f g) ≅ (baseChangeFunctor f).comp (baseChangeFunctor g)

Base change along a composite f ≫ g of ring maps is base change along f followed by base change along g.

Equations

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

@[simp]

theorem TauCeti.AffineGroupSchemeCat.baseChangeFunctorCompIso_hom_app_hom_hom_hom {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) (G : AffineGroupSchemeCat R) : ((baseChangeFunctorCompIso f g).hom.app G).hom.hom.hom = (AlgebraicGeometry.Over.pullbackSpecMapComp f g).hom.app G.obj.X

The morphism of objects over Spec T underlying (baseChangeFunctorCompIso f g).hom.

@[simp]

theorem TauCeti.AffineGroupSchemeCat.baseChangeFunctorCompIso_inv_app_hom_hom_hom {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) (G : AffineGroupSchemeCat R) : ((baseChangeFunctorCompIso f g).inv.app G).hom.hom.hom = (AlgebraicGeometry.Over.pullbackSpecMapComp f g).inv.app G.obj.X

The morphism of objects over Spec T underlying (baseChangeFunctorCompIso f g).inv.

noncomputable def TauCeti.AffineGroupSchemeCat.hopfSpecBaseChangeGrpIso {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (H : CommHopfAlgCat R) : (CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))).mapGrp.obj ((AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op H)) ≅ (AlgebraicGeometry.hopfSpec ↧S).obj (Opposite.op (CommHopfAlgCat.baseChange H))

Pulling the Hopf spectrum of H from Spec R to Spec S gives the Hopf spectrum of the scalar extension S ⊗[R] H, as group objects over Spec S.

The underlying scheme isomorphism first exchanges the two legs of the pullback and then applies the affine comparison pullbackSpecIso'. Mathlib proves that this map preserves the unit and multiplication of the Hopf spectra.

Equations

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

@[simp]

theorem TauCeti.AffineGroupSchemeCat.hopfSpecBaseChangeGrpIso_hom_hom_hom_left {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (H : CommHopfAlgCat R) : CategoryTheory.Over.Hom.left (hopfSpecBaseChangeGrpIso H).hom.hom.hom = (CategoryTheory.Limits.pullbackSymmetry (AlgebraicGeometry.Spec ↧↑H ↘ AlgebraicGeometry.Spec ↧R) (AlgebraicGeometry.Spec ↧S ↘ AlgebraicGeometry.Spec ↧R) ≪≫ AlgebraicGeometry.pullbackSpecIso' R S ↑H).hom

The underlying scheme map of hopfSpecBaseChangeGrpIso is the standard affine pullback comparison, after exchanging the two pullback legs.

@[simp]

theorem TauCeti.AffineGroupSchemeCat.hopfSpecBaseChangeGrpIso_inv_hom_hom_left {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (H : CommHopfAlgCat R) : CategoryTheory.Over.Hom.left (hopfSpecBaseChangeGrpIso H).inv.hom.hom = (CategoryTheory.Limits.pullbackSymmetry (AlgebraicGeometry.Spec ↧↑H ↘ AlgebraicGeometry.Spec ↧R) (AlgebraicGeometry.Spec ↧S ↘ AlgebraicGeometry.Spec ↧R) ≪≫ AlgebraicGeometry.pullbackSpecIso' R S ↑H).inv

The inverse underlying scheme map of hopfSpecBaseChangeGrpIso is the inverse of the standard affine pullback comparison.

noncomputable def TauCeti.AffineGroupSchemeCat.hopfSpecBaseChangeIso {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (H : CommHopfAlgCat R) : baseChange (CommRingCat.ofHom (algebraMap R S)) ((commHopfAlgCatOpEquivAffineGroupSchemeCat ↧R).functor.obj (Opposite.op H)) ≅ (commHopfAlgCatOpEquivAffineGroupSchemeCat ↧S).functor.obj (Opposite.op (CommHopfAlgCat.baseChange H))

Base change of an affine group scheme represented by a commutative Hopf algebra is represented by the scalar extension of that Hopf algebra.

Equations

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

@[simp]

theorem TauCeti.AffineGroupSchemeCat.hopfSpecBaseChangeIso_hom_hom {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (H : CommHopfAlgCat R) : (hopfSpecBaseChangeIso H).hom.hom = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))).mapGrp.map ((commHopfAlgCatOpEquivAffineGroupSchemeCat.functorCompιIso ↧R).hom.app (Opposite.op H))) (CategoryTheory.CategoryStruct.comp (hopfSpecBaseChangeGrpIso H).hom ((commHopfAlgCatOpEquivAffineGroupSchemeCat.functorCompιIso ↧S).inv.app (Opposite.op (CommHopfAlgCat.baseChange H))))

The underlying group-scheme morphism of hopfSpecBaseChangeIso is the composite of the anti-equivalence comparison at R, the direct Hopf-spectrum base-change comparison, and the inverse anti-equivalence comparison at S.

@[simp]

theorem TauCeti.AffineGroupSchemeCat.hopfSpecBaseChangeIso_inv_hom {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (H : CommHopfAlgCat R) : (hopfSpecBaseChangeIso H).inv.hom = CategoryTheory.CategoryStruct.comp ((commHopfAlgCatOpEquivAffineGroupSchemeCat.functorCompιIso ↧S).hom.app (Opposite.op (CommHopfAlgCat.baseChange H))) (CategoryTheory.CategoryStruct.comp (hopfSpecBaseChangeGrpIso H).inv ((CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))).mapGrp.map ((commHopfAlgCatOpEquivAffineGroupSchemeCat.functorCompιIso ↧R).inv.app (Opposite.op H))))

The inverse underlying group-scheme morphism of hopfSpecBaseChangeIso is the reverse composite of the three comparison isomorphisms.