Base change of relative spectra

An affine morphism remains affine after arbitrary base change. Consequently, pulling back a scheme affine over X along f : Y ⟶ X gives a scheme affine over Y. This file packages that construction as the functor baseChangeAffineSchemeOver.

Relative Spec commutes with this base change: for a quasicoherent algebra A on X, the relative spectrum over Y of the pullback algebra f^* A is the fibre product Y ×_X Spec_X A. The projection Spec_Y (f^* A) ⟶ Spec_X A is the morphism over X corresponding to the algebra map A ⟶ f_* (p_* 𝒪) adjoint to the identification of f^* A with the functions on Spec_Y (f^* A). The square is cartesian because, for every scheme q : T ⟶ Y, the universal property of relative Spec, the adjunction between pullback and pushforward of algebras, and the identification f_* q_* 𝒪_T ≅ (q ≫ f)_* 𝒪_T give a bijection between morphisms T ⟶ Spec_Y (f^* A) over Y and morphisms T ⟶ Spec_X A over X, and this bijection is composition with the projection. The resulting isomorphism is natural in A.

Base change of relative spectra is compatible with identities and composition of base morphisms, through the identity and composition isomorphisms of algebra pullback. Along the identity, the projection Spec_X (𝟙^* A) ⟶ Spec_X A is induced by A ≅ 𝟙^* A. For g : Z ⟶ Y and f : Y ⟶ X, the projection Spec_Z ((g ≫ f)^* A) ⟶ Spec_X A is the identification Spec_Z ((g ≫ f)^* A) ≅ Spec_Z (g^* f^* A) followed by the projections Spec_Z (g^* f^* A) ⟶ Spec_Y (f^* A) ⟶ Spec_X A. Correspondingly, the isomorphism for g ≫ f is the composite of those for g and f with Mathlib's MorphismProperty.Over.pullbackComp.

The base-change functor specializes Mathlib's pullback functor on morphism-property over-categories to the property IsAffineHom; no new choice of fibre product is made.

Main declarations

• TauCeti.AlgebraicGeometry.baseChangeAffineSchemeOver: base change of affine schemes over a fixed base;
• TauCeti.AlgebraicGeometry.relativeSpecPullbackFst: the projection Spec_Y (f^* A) ⟶ Spec_X A;
• TauCeti.AlgebraicGeometry.isPullback_relativeSpecPullbackFst: the square formed by this projection and the structure morphisms over f is cartesian;
• TauCeti.AlgebraicGeometry.relativeSpecPullbackIso: the isomorphism of affine schemes over Y between Spec_Y (f^* A) and the base change of Spec_X A;
• TauCeti.AlgebraicGeometry.relativeSpecBaseChangeIso: the same isomorphism, natural in A;
• TauCeti.AlgebraicGeometry.relativeSpecPullbackFst_id, TauCeti.AlgebraicGeometry.relativeSpecPullbackFst_comp and TauCeti.AlgebraicGeometry.relativeSpecPullbackIso_comp: compatibility of base change with identities and composition of base morphisms.

References

• The Stacks Project, Tag 01SD (affine morphisms are stable under base change).
• The Stacks Project, Tag 01LQ (relative spectrum as a functor), where the relative spectrum of a pulled-back algebra is identified with the base change of the relative spectrum.

theorem TauCeti.AlgebraicGeometry.instHasPullbacksAlongSchemeIsAffineHom_tauCeti {X Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) : CategoryTheory.MorphismProperty.HasPullbacksAlong (@AlgebraicGeometry.IsAffineHom) f

Every morphism of schemes has pullbacks along f, in particular the affine ones.

theorem TauCeti.AlgebraicGeometry.instIsStableUnderBaseChangeAlongSchemeIsAffineHom_tauCeti {X Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) : CategoryTheory.MorphismProperty.IsStableUnderBaseChangeAlong (@AlgebraicGeometry.IsAffineHom) f

Affine morphisms are stable under base change along f.

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.baseChangeAffineSchemeOver {X Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) : CategoryTheory.Functor (AffineSchemeOver X) (AffineSchemeOver Y)

Pullback of schemes affine over X along an arbitrary morphism f : Y ⟶ X.

The underlying scheme is the chosen fibre product, and its structure morphism is the second projection to Y.

@[simp]

theorem TauCeti.AlgebraicGeometry.baseChangeAffineSchemeOver_map_left_fst {X Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) {V W : AffineSchemeOver X} (g : V ⟶ W) : CategoryTheory.CategoryStruct.comp ((baseChangeAffineSchemeOver f).map g).left (CategoryTheory.Limits.pullback.fst W.hom f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst V.hom f) g.left

The induced map between base changes commutes with projection to the original total spaces.

@[simp]

theorem TauCeti.AlgebraicGeometry.baseChangeAffineSchemeOver_map_left_snd {X Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) {V W : AffineSchemeOver X} (g : V ⟶ W) : CategoryTheory.CategoryStruct.comp ((baseChangeAffineSchemeOver f).map g).left (CategoryTheory.Limits.pullback.snd W.hom f) = CategoryTheory.Limits.pullback.snd V.hom f

The induced map between base changes lies over the identity of the new base.

noncomputable def TauCeti.AlgebraicGeometry.relativeSpecPullbackFst {X Y : AlgebraicGeometry.Scheme} (A : QuasicoherentAlgebra X) (f : Y ⟶ X) : ((QuasicoherentAlgebra.pullback f).obj A).obj.relativeSpec ⟶ A.obj.relativeSpec

The projection Spec_Y (f^* A) ⟶ Spec_X A from the relative spectrum of a pulled-back algebra. It is the morphism over X whose algebra map A ⟶ f_* (p_* 𝒪) is adjoint to the identification of f^* A with the functions on Spec_Y (f^* A) (relativeSpecPullbackFst_eq_relativeSpecLift).

theorem TauCeti.AlgebraicGeometry.relativeSpecPullbackFst_eq_relativeSpecLift {X Y : AlgebraicGeometry.Scheme} (A : QuasicoherentAlgebra X) (f : Y ⟶ X) : relativeSpecPullbackFst A f = CategoryTheory.CommMon.relativeSpecLift (CategoryTheory.CategoryStruct.comp ((QuasicoherentAlgebra.pullbackHomEquiv f A (AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebra ((QuasicoherentAlgebra.pullback f).obj A).obj.relativeSpecToBase)) ((QuasicoherentAlgebra.pullback f).obj A).obj.relativeSpecPushforwardIso.inv) (AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebraCompIso ((QuasicoherentAlgebra.pullback f).obj A).obj.relativeSpecToBase f).hom)

The projection Spec_Y (f^* A) ⟶ Spec_X A is the lift of the algebra map adjoint to the identification of f^* A with the functions on its relative spectrum, followed by the identification f_* p_* 𝒪 ≅ (p ≫ f)_* 𝒪.

@[simp]

theorem TauCeti.AlgebraicGeometry.relativeSpecPullbackFst_relativeSpecToBase {X Y : AlgebraicGeometry.Scheme} (A : QuasicoherentAlgebra X) (f : Y ⟶ X) : CategoryTheory.CategoryStruct.comp (relativeSpecPullbackFst A f) A.obj.relativeSpecToBase = CategoryTheory.CategoryStruct.comp ((QuasicoherentAlgebra.pullback f).obj A).obj.relativeSpecToBase f

The projection Spec_Y (f^* A) ⟶ Spec_X A lies over f.

@[simp]

theorem TauCeti.AlgebraicGeometry.relativeSpecPullbackFst_relativeSpecToBase_assoc {X Y : AlgebraicGeometry.Scheme} (A : QuasicoherentAlgebra X) (f : Y ⟶ X) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (relativeSpecPullbackFst A f) (CategoryTheory.CategoryStruct.comp A.obj.relativeSpecToBase h) = CategoryTheory.CategoryStruct.comp ((QuasicoherentAlgebra.pullback f).obj A).obj.relativeSpecToBase (CategoryTheory.CategoryStruct.comp f h)

The projection Spec_Y (f^* A) ⟶ Spec_X A lies over f.

theorem TauCeti.AlgebraicGeometry.isPullback_relativeSpecPullbackFst {X Y : AlgebraicGeometry.Scheme} (A : QuasicoherentAlgebra X) (f : Y ⟶ X) : CategoryTheory.IsPullback (relativeSpecPullbackFst A f) ((QuasicoherentAlgebra.pullback f).obj A).obj.relativeSpecToBase A.obj.relativeSpecToBase f

Relative Spec commutes with base change. For a quasicoherent algebra A on X and any morphism f : Y ⟶ X, the relative spectrum of the pullback algebra f^* A is the fibre product Y ×_X Spec_X A, with projections relativeSpecPullbackFst A f and the structure morphism.

theorem TauCeti.AlgebraicGeometry.relativeSpecMap_pullback_map_relativeSpecPullbackFst {X Y : AlgebraicGeometry.Scheme} (A : QuasicoherentAlgebra X) (f : Y ⟶ X) {A' : QuasicoherentAlgebra X} (b : A' ⟶ A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CommMon.relativeSpecMap ((QuasicoherentAlgebra.pullback f).map b).hom) (relativeSpecPullbackFst A' f) = CategoryTheory.CategoryStruct.comp (relativeSpecPullbackFst A f) (CategoryTheory.CommMon.relativeSpecMap b.hom)

The projection Spec_Y (f^* A) ⟶ Spec_X A is natural in the algebra A.

theorem TauCeti.AlgebraicGeometry.relativeSpecMap_pullback_map_relativeSpecPullbackFst_assoc {X Y : AlgebraicGeometry.Scheme} (A : QuasicoherentAlgebra X) (f : Y ⟶ X) {A' : QuasicoherentAlgebra X} (b : A' ⟶ A) {Z : AlgebraicGeometry.Scheme} (h : A'.obj.relativeSpec ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CommMon.relativeSpecMap ((QuasicoherentAlgebra.pullback f).map b).hom) (CategoryTheory.CategoryStruct.comp (relativeSpecPullbackFst A' f) h) = CategoryTheory.CategoryStruct.comp (relativeSpecPullbackFst A f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CommMon.relativeSpecMap b.hom) h)

The projection Spec_Y (f^* A) ⟶ Spec_X A is natural in the algebra A.

noncomputable def TauCeti.AlgebraicGeometry.relativeSpecPullbackIso {X Y : AlgebraicGeometry.Scheme} (A : QuasicoherentAlgebra X) (f : Y ⟶ X) : (relativeSpec Y).obj (Opposite.op ((QuasicoherentAlgebra.pullback f).obj A)) ≅ (baseChangeAffineSchemeOver f).obj ((relativeSpec X).obj (Opposite.op A))

The relative spectrum of f^* A over Y is the base change along f of the relative spectrum of A, as affine schemes over Y.

@[simp]

theorem TauCeti.AlgebraicGeometry.relativeSpecPullbackIso_hom_left_fst {X Y : AlgebraicGeometry.Scheme} (A : QuasicoherentAlgebra X) (f : Y ⟶ X) : CategoryTheory.CategoryStruct.comp (relativeSpecPullbackIso A f).hom.left (CategoryTheory.Limits.pullback.fst A.obj.relativeSpecToBase f) = relativeSpecPullbackFst A f

The isomorphism relativeSpecPullbackIso followed by the first projection of the fibre product is the projection Spec_Y (f^* A) ⟶ Spec_X A.

theorem TauCeti.AlgebraicGeometry.relativeSpecPullbackIso_hom_left_fst_assoc {X Y : AlgebraicGeometry.Scheme} (A : QuasicoherentAlgebra X) (f : Y ⟶ X) {Z : AlgebraicGeometry.Scheme} (h : A.obj.relativeSpec ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (relativeSpecPullbackIso A f).hom.left (CategoryTheory.Limits.pullback.fst A.obj.relativeSpecToBase f)) h = CategoryTheory.CategoryStruct.comp (relativeSpecPullbackFst A f) h

The isomorphism relativeSpecPullbackIso followed by the first projection of the fibre product is the projection Spec_Y (f^* A) ⟶ Spec_X A.

@[simp]

theorem TauCeti.AlgebraicGeometry.relativeSpecPullbackIso_hom_left_snd {X Y : AlgebraicGeometry.Scheme} (A : QuasicoherentAlgebra X) (f : Y ⟶ X) : CategoryTheory.CategoryStruct.comp (relativeSpecPullbackIso A f).hom.left (CategoryTheory.Limits.pullback.snd A.obj.relativeSpecToBase f) = ((QuasicoherentAlgebra.pullback f).obj A).obj.relativeSpecToBase

The isomorphism relativeSpecPullbackIso followed by the second projection of the fibre product is the structure morphism of Spec_Y (f^* A).

theorem TauCeti.AlgebraicGeometry.relativeSpecPullbackIso_hom_left_snd_assoc {X Y : AlgebraicGeometry.Scheme} (A : QuasicoherentAlgebra X) (f : Y ⟶ X) {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (relativeSpecPullbackIso A f).hom.left (CategoryTheory.Limits.pullback.snd A.obj.relativeSpecToBase f)) h = CategoryTheory.CategoryStruct.comp ((QuasicoherentAlgebra.pullback f).obj A).obj.relativeSpecToBase h

The isomorphism relativeSpecPullbackIso followed by the second projection of the fibre product is the structure morphism of Spec_Y (f^* A).

@[simp]

theorem TauCeti.AlgebraicGeometry.relativeSpecPullbackIso_inv_left_relativeSpecPullbackFst {X Y : AlgebraicGeometry.Scheme} (A : QuasicoherentAlgebra X) (f : Y ⟶ X) : CategoryTheory.CategoryStruct.comp (relativeSpecPullbackIso A f).inv.left (relativeSpecPullbackFst A f) = CategoryTheory.Limits.pullback.fst A.obj.relativeSpecToBase f

The inverse of relativeSpecPullbackIso, followed by the projection Spec_Y (f^* A) ⟶ Spec_X A, is the first projection of the fibre product.

theorem TauCeti.AlgebraicGeometry.relativeSpecPullbackIso_inv_left_relativeSpecPullbackFst_assoc {X Y : AlgebraicGeometry.Scheme} (A : QuasicoherentAlgebra X) (f : Y ⟶ X) {Z : AlgebraicGeometry.Scheme} (h : A.obj.relativeSpec ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (relativeSpecPullbackIso A f).inv.left (relativeSpecPullbackFst A f)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst A.obj.relativeSpecToBase f) h

The inverse of relativeSpecPullbackIso, followed by the projection Spec_Y (f^* A) ⟶ Spec_X A, is the first projection of the fibre product.

@[simp]

theorem TauCeti.AlgebraicGeometry.relativeSpecPullbackIso_inv_left_relativeSpecToBase {X Y : AlgebraicGeometry.Scheme} (A : QuasicoherentAlgebra X) (f : Y ⟶ X) : CategoryTheory.CategoryStruct.comp (relativeSpecPullbackIso A f).inv.left ((QuasicoherentAlgebra.pullback f).obj A).obj.relativeSpecToBase = CategoryTheory.Limits.pullback.snd A.obj.relativeSpecToBase f

The inverse of relativeSpecPullbackIso, followed by the structure morphism of Spec_Y (f^* A), is the second projection of the fibre product.

theorem TauCeti.AlgebraicGeometry.relativeSpecPullbackIso_inv_left_relativeSpecToBase_assoc {X Y : AlgebraicGeometry.Scheme} (A : QuasicoherentAlgebra X) (f : Y ⟶ X) {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (relativeSpecPullbackIso A f).inv.left ((QuasicoherentAlgebra.pullback f).obj A).obj.relativeSpecToBase) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd A.obj.relativeSpecToBase f) h

The inverse of relativeSpecPullbackIso, followed by the structure morphism of Spec_Y (f^* A), is the second projection of the fibre product.

noncomputable def TauCeti.AlgebraicGeometry.relativeSpecBaseChangeIso {X Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) : (QuasicoherentAlgebra.pullback f).op.comp (relativeSpec Y) ≅ (relativeSpec X).comp (baseChangeAffineSchemeOver f)

Relative Spec commutes with base change, naturally in the algebra. For f : Y ⟶ X, taking the relative spectrum of the pullback of a quasicoherent algebra is naturally isomorphic to base changing its relative spectrum along f.

@[simp]

theorem TauCeti.AlgebraicGeometry.relativeSpecBaseChangeIso_app {X Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) (A : (QuasicoherentAlgebra X)ᵒᵖ) : (relativeSpecBaseChangeIso f).app A = relativeSpecPullbackIso (Opposite.unop A) f

The components of relativeSpecBaseChangeIso are relativeSpecPullbackIso.

theorem TauCeti.AlgebraicGeometry.relativeSpecHomEquiv_comp_relativeSpecPullbackFst {X Y : AlgebraicGeometry.Scheme} (A : QuasicoherentAlgebra X) (f : Y ⟶ X) {T : AlgebraicGeometry.Scheme} {q : T ⟶ Y} (t : { t : T ⟶ ((QuasicoherentAlgebra.pullback f).obj A).obj.relativeSpec // CategoryTheory.CategoryStruct.comp t ((QuasicoherentAlgebra.pullback f).obj A).obj.relativeSpecToBase = q }) : (A.obj.relativeSpecHomEquiv (CategoryTheory.CategoryStruct.comp q f)) ⟨CategoryTheory.CategoryStruct.comp (↑t) (relativeSpecPullbackFst A f), ⋯⟩ = CategoryTheory.CategoryStruct.comp ((QuasicoherentAlgebra.pullbackHomEquiv f A (AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebra q)) ((((QuasicoherentAlgebra.pullback f).obj A).obj.relativeSpecHomEquiv q) t)) (AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebraCompIso q f).hom

The algebra map of a morphism t : T ⟶ Spec_Y (f^* A) over q : T ⟶ Y, followed by the projection to Spec_X A, is the transpose along f of the algebra map of t, followed by the identification f_* q_* 𝒪_T ≅ (q ≫ f)_* 𝒪_T.

theorem TauCeti.AlgebraicGeometry.relativeSpecPullbackFst_comp {X Y : AlgebraicGeometry.Scheme} (A : QuasicoherentAlgebra X) (f : Y ⟶ X) {Z : AlgebraicGeometry.Scheme} (g : Z ⟶ Y) : relativeSpecPullbackFst A (CategoryTheory.CategoryStruct.comp g f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CommMon.relativeSpecMap ((QuasicoherentAlgebra.pullbackComp g f).hom.app A).hom) (CategoryTheory.CategoryStruct.comp (relativeSpecPullbackFst ((QuasicoherentAlgebra.pullback f).obj A) g) (relativeSpecPullbackFst A f))

Base change of relative spectra is compatible with composition. For g : Z ⟶ Y and f : Y ⟶ X, the projection Spec_Z ((g ≫ f)^* A) ⟶ Spec_X A is the composite of the identification Spec_Z ((g ≫ f)^* A) ≅ Spec_Z (g^* f^* A) induced by the composition isomorphism of pullback with the projections Spec_Z (g^* f^* A) ⟶ Spec_Y (f^* A) ⟶ Spec_X A.

@[simp]

theorem TauCeti.AlgebraicGeometry.relativeSpecPullbackFst_id {X : AlgebraicGeometry.Scheme} (A : QuasicoherentAlgebra X) : relativeSpecPullbackFst A (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CommMon.relativeSpecMap ((QuasicoherentAlgebra.pullbackId X).inv.app A).hom

Base change of relative spectra along the identity. The projection Spec_X (𝟙^* A) ⟶ Spec_X A is the identification induced by the identity isomorphism A ≅ 𝟙^* A of pullback.

theorem TauCeti.AlgebraicGeometry.relativeSpecPullbackIso_comp {X Y : AlgebraicGeometry.Scheme} (A : QuasicoherentAlgebra X) (f : Y ⟶ X) {Z : AlgebraicGeometry.Scheme} (g : Z ⟶ Y) : (relativeSpecPullbackIso A (CategoryTheory.CategoryStruct.comp g f)).hom = CategoryTheory.CategoryStruct.comp ((relativeSpec Z).map ((QuasicoherentAlgebra.pullbackComp g f).hom.app A).op) (CategoryTheory.CategoryStruct.comp (relativeSpecPullbackIso ((QuasicoherentAlgebra.pullback f).obj A) g).hom (CategoryTheory.CategoryStruct.comp ((baseChangeAffineSchemeOver g).map (relativeSpecPullbackIso A f).hom) ((CategoryTheory.MorphismProperty.Over.pullbackComp g f (CategoryTheory.CategoryStruct.comp g f) ⋯).inv.app ((relativeSpec X).obj (Opposite.op A)))))

Relative Spec commutes with base change, compatibly with composition. For g : Z ⟶ Y and f : Y ⟶ X, the isomorphism Spec_Z ((g ≫ f)^* A) ≅ Z ×_X Spec_X A is the composite of the identification Spec_Z ((g ≫ f)^* A) ≅ Spec_Z (g^* f^* A), the isomorphisms for g and for f, and the canonical isomorphism Z ×_Y (Y ×_X Spec_X A) ≅ Z ×_X Spec_X A.