Pullback of schemes along Spec.map

Mathlib's CategoryTheory.Over.pullbackId and CategoryTheory.Over.pullbackComp compare the pullback functors on Over categories along an identity morphism and along a composite. This file reads those comparisons through Spec: Spec.map takes an identity ring map to an identity morphism of schemes and a composite f ≫ g to Spec.map g ≫ Spec.map f, so pullback along Spec.map (𝟙 R) is the identity functor on schemes over Spec R, and pullback along Spec.map (f ≫ g) is the composite of pullback along Spec.map f with pullback along Spec.map g.

Nothing here mentions affineness or group objects: these are statements about arbitrary schemes over an affine base, and they are the underlying comparisons of the base-change functors on affine group schemes in TauCeti/AlgebraicGeometry/AffineGroupScheme/BaseChange/Basic.lean.

Main declarations

• TauCeti.AlgebraicGeometry.Over.pullbackSpecMapId: pullback along Spec.map (𝟙 R) is the identity functor.
• TauCeti.AlgebraicGeometry.Over.pullbackSpecMapComp: pullback along Spec.map (f ≫ g) is a composite of pullbacks.

noncomputable def TauCeti.AlgebraicGeometry.Over.pullbackSpecMapId {R : CommRingCat} : CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CategoryTheory.CategoryStruct.id R)) ≅ CategoryTheory.Functor.id (CategoryTheory.Over (AlgebraicGeometry.Spec R))

Pullback along Spec.map (𝟙 R) is the identity functor on schemes over Spec R.

Equations

• TauCeti.AlgebraicGeometry.Over.pullbackSpecMapId = CategoryTheory.eqToIso ⋯ ≪≫ CategoryTheory.Over.pullbackId

noncomputable def TauCeti.AlgebraicGeometry.Over.pullbackSpecMapComp {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) : CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CategoryTheory.CategoryStruct.comp f g)) ≅ (CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map f)).comp (CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map g))

Pullback along Spec.map (f ≫ g) is pullback along Spec.map f followed by pullback along Spec.map g.

Equations

• TauCeti.AlgebraicGeometry.Over.pullbackSpecMapComp f g = CategoryTheory.eqToIso ⋯ ≪≫ CategoryTheory.Over.pullbackComp (AlgebraicGeometry.Spec.map g) (AlgebraicGeometry.Spec.map f)