Pullback of quasicoherent algebras

A quasicoherent commutative algebra on a scheme can be viewed as a commutative monoid object in the symmetric monoidal category of quasicoherent sheaves. This description makes pullback of algebras functorial: the strong symmetric monoidal pullback of quasicoherent sheaves carries commutative monoid objects to commutative monoid objects.

This is the algebraic side of base change for relative spectra. The characteristic equations in this file identify the carrier, unit, multiplication, and morphisms of an algebra pullback with the already established pullback of the underlying quasicoherent sheaves and its monoidal comparisons.

The construction is Mathlib's CategoryTheory.Functor.mapCommMon, which carries commutative monoid objects along a lax braided functor, applied to the strong symmetric monoidal structure on TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pullback.

Pullback of algebras is left adjoint to pushforward of algebras: for f : X ⟶ Y, a quasicoherent algebra A on Y and any commutative algebra B on X, algebra maps f^* A ⟶ B correspond to algebra maps A ⟶ f_* B. The bijection is transposition along the pullback–pushforward adjunction of modules. It preserves algebra maps because that adjunction is monoidal (CategoryTheory.Adjunction.isMonHom_homEquiv_iff), and the multiplication of f^* A is that of A transported along the tensor comparison of pullback, which is invertible as A is quasicoherent. The algebra B need not be quasicoherent, so that B can be the structure sheaf of an arbitrary scheme.

Pullback of algebras is pseudofunctorial: the identity and composition isomorphisms 𝟙^* A ≅ A and f^* g^* A ≅ (f ≫ g)^* A are those of the underlying modules, and the bijection above is compatible with them and with the corresponding isomorphisms of pushforward. These are the inputs for the compatibility of base change of relative spectra with composition.

Main declarations

• TauCeti.AlgebraicGeometry.QuasicoherentAlgebra.pullback: pullback of quasicoherent algebras along a morphism of schemes;
• TauCeti.AlgebraicGeometry.QuasicoherentAlgebra.pullbackId and TauCeti.AlgebraicGeometry.QuasicoherentAlgebra.pullbackComp: its identity and composition isomorphisms, given on underlying modules by Mathlib's Scheme.Modules.pullbackId and Scheme.Modules.pullbackComp;
• TauCeti.AlgebraicGeometry.QuasicoherentAlgebra.pullbackHomEquiv: the bijection between algebra maps f^* A ⟶ B and A ⟶ f_* B, natural in A and B, and compatible with composition (pullbackHomEquiv_comp) and identities (pullbackHomEquiv_id_hom_hom).

References

• The Stacks Project, Tag 01LQ (relative spectrum as a functor), where this adjunction for quasicoherent algebras gives the universal property of relative Spec in terms of pullbacks.

@[instance_reducible]

noncomputable def TauCeti.AlgebraicGeometry.pullbackAlgebraSymmetricCategorySheafOfModules (X : AlgebraicGeometry.Scheme) : CategoryTheory.SymmetricCategory (SheafOfModules X.ringCatSheaf)

The symmetry of modules on a scheme, stated for the unfolded sheaf category used by the quasicoherent full subcategory.

noncomputable def TauCeti.AlgebraicGeometry.QuasicoherentAlgebra.pullback {X Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) : CategoryTheory.Functor (QuasicoherentAlgebra X) (QuasicoherentAlgebra Y)

Pullback of quasicoherent commutative algebras along a morphism of schemes.

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentAlgebra.pullback_obj_X {X Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) (A : QuasicoherentAlgebra X) : ((pullback f).obj A).obj.X = (AlgebraicGeometry.Scheme.Modules.pullback f).obj A.obj.X

The carrier of a pulled-back algebra is the pullback of its underlying module.

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentAlgebra.pullback_obj_one {X Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) (A : QuasicoherentAlgebra X) : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.pullbackObjUnitIso f).inv (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback f).map CategoryTheory.MonObj.one) (CategoryTheory.eqToHom ⋯))

The unit of a pulled-back algebra is the pullback of its unit, preceded by the identification of the pulled-back structure sheaf.

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentAlgebra.pullback_obj_mul {X Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) (A : QuasicoherentAlgebra X) : CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Functor.OplaxMonoidal.δ (AlgebraicGeometry.Scheme.Modules.pullback f) A.obj.X A.obj.X)) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback f).map CategoryTheory.MonObj.mul) (CategoryTheory.eqToHom ⋯)))

The multiplication of a pulled-back algebra is the pullback of its multiplication, preceded by the inverse tensor comparison of module pullback.

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentAlgebra.pullback_map_hom_hom_hom {X Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) {A B : QuasicoherentAlgebra X} (g : A ⟶ B) : ((pullback f).map g).hom.hom.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback f).map g.hom.hom.hom) (CategoryTheory.eqToHom ⋯))

Pullback of algebra morphisms has the underlying map given by pullback of module morphisms, transported along the canonical carrier identifications.

noncomputable def TauCeti.AlgebraicGeometry.QuasicoherentAlgebra.pullbackId (X : AlgebraicGeometry.Scheme) : pullback (CategoryTheory.CategoryStruct.id X) ≅ CategoryTheory.Functor.id (QuasicoherentAlgebra X)

Pullback of quasicoherent algebras along the identity is naturally the identity.

noncomputable def TauCeti.AlgebraicGeometry.QuasicoherentAlgebra.pullbackComp {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) : (pullback g).comp (pullback f) ≅ pullback (CategoryTheory.CategoryStruct.comp f g)

Pullback of quasicoherent algebras respects composition.

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentAlgebra.pullbackId_hom_app_hom_hom_hom {X : AlgebraicGeometry.Scheme} (A : QuasicoherentAlgebra X) : ((pullbackId X).hom.app A).hom.hom.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((AlgebraicGeometry.Scheme.Modules.pullbackId X).hom.app A.obj.X)

The identity comparison of algebra pullback is Mathlib's identity comparison of module pullback on underlying modules.

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentAlgebra.pullbackId_inv_app_hom_hom_hom {X : AlgebraicGeometry.Scheme} (A : QuasicoherentAlgebra X) : ((pullbackId X).inv.app A).hom.hom.hom = CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackId X).inv.app A.obj.X) (CategoryTheory.eqToHom ⋯)

The inverse identity comparison of algebra pullback is Mathlib's inverse identity comparison of module pullback on underlying modules.

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentAlgebra.pullbackComp_hom_app_hom_hom_hom {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (A : QuasicoherentAlgebra Z) : ((pullbackComp f g).hom.app A).hom.hom.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackComp f g).hom.app A.obj.X) (CategoryTheory.eqToHom ⋯))

The composition comparison of algebra pullback is Mathlib's composition comparison of module pullback on underlying modules.

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentAlgebra.pullbackComp_inv_app_hom_hom_hom {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (A : QuasicoherentAlgebra Z) : ((pullbackComp f g).inv.app A).hom.hom.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackComp f g).inv.app A.obj.X) (CategoryTheory.eqToHom ⋯))

The inverse composition comparison of algebra pullback is Mathlib's inverse composition comparison of module pullback on underlying modules.

noncomputable def TauCeti.AlgebraicGeometry.QuasicoherentAlgebra.pullbackHomEquiv {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (A : QuasicoherentAlgebra Y) (B : CategoryTheory.CommMon X.Modules) : (((pullback f).obj A).obj ⟶ B) ≃ (A.obj ⟶ (AlgebraicGeometry.Scheme.Modules.pushforward f).mapCommMon.obj B)

Pullback of quasicoherent algebras is left adjoint to pushforward of algebras. For a morphism of schemes f : X ⟶ Y, a quasicoherent algebra A on Y and a commutative algebra B on X, algebra maps f^* A ⟶ B correspond to algebra maps A ⟶ f_* B. On underlying modules this is transposition along the pullback–pushforward adjunction (pullbackHomEquiv_apply_hom_hom).

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentAlgebra.pullbackHomEquiv_apply_hom_hom {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (A : QuasicoherentAlgebra Y) (B : CategoryTheory.CommMon X.Modules) (g : ((pullback f).obj A).obj ⟶ B) : ((pullbackHomEquiv f A B) g).hom.hom = ((AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction f).homEquiv A.obj.X B.toMon.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) g.hom.hom)

On underlying modules, the algebra map A ⟶ f_* B corresponding to g : f^* A ⟶ B is the transpose of g along the pullback–pushforward adjunction.

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentAlgebra.pullbackHomEquiv_symm_apply_hom_hom {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (A : QuasicoherentAlgebra Y) (B : CategoryTheory.CommMon X.Modules) (ψ : A.obj ⟶ (AlgebraicGeometry.Scheme.Modules.pushforward f).mapCommMon.obj B) : ((pullbackHomEquiv f A B).symm ψ).hom.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (((AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction f).homEquiv A.obj.X B.toMon.X).symm ψ.hom.hom)

On underlying modules, the algebra map f^* A ⟶ B corresponding to ψ : A ⟶ f_* B is the inverse transpose of ψ along the pullback–pushforward adjunction.

theorem TauCeti.AlgebraicGeometry.QuasicoherentAlgebra.pullbackHomEquiv_naturality_left {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {A' A : QuasicoherentAlgebra Y} (a : A' ⟶ A) (B : CategoryTheory.CommMon X.Modules) (g : ((pullback f).obj A).obj ⟶ B) : (pullbackHomEquiv f A' B) (CategoryTheory.CategoryStruct.comp ((pullback f).map a).hom g) = CategoryTheory.CategoryStruct.comp a.hom ((pullbackHomEquiv f A B) g)

The bijection pullbackHomEquiv is natural in the algebra on the base: precomposing with the pullback of a : A' ⟶ A corresponds to precomposing with a.

theorem TauCeti.AlgebraicGeometry.QuasicoherentAlgebra.pullbackHomEquiv_naturality_right {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (A : QuasicoherentAlgebra Y) {B B' : CategoryTheory.CommMon X.Modules} (g : ((pullback f).obj A).obj ⟶ B) (b : B ⟶ B') : (pullbackHomEquiv f A B') (CategoryTheory.CategoryStruct.comp g b) = CategoryTheory.CategoryStruct.comp ((pullbackHomEquiv f A B) g) ((AlgebraicGeometry.Scheme.Modules.pushforward f).mapCommMon.map b)

The bijection pullbackHomEquiv is natural in the algebra on the source: postcomposing with b : B ⟶ B' corresponds to postcomposing with its pushforward.

theorem TauCeti.AlgebraicGeometry.QuasicoherentAlgebra.pullbackHomEquiv_comp {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {Z : AlgebraicGeometry.Scheme} (g : Y ⟶ Z) (A : QuasicoherentAlgebra Z) (B : CategoryTheory.CommMon X.Modules) (φ : ((pullback f).obj ((pullback g).obj A)).obj ⟶ B) : (pullbackHomEquiv (CategoryTheory.CategoryStruct.comp f g) A B) (CategoryTheory.CategoryStruct.comp ((pullbackComp f g).inv.app A).hom φ) = CategoryTheory.CategoryStruct.comp ((pullbackHomEquiv g A ((AlgebraicGeometry.Scheme.Modules.pushforward f).mapCommMon.obj B)) ((pullbackHomEquiv f ((pullback g).obj A) B) φ)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.mapCommMonCompIso.inv.app B) ((CategoryTheory.Functor.mapCommMonNatIso (AlgebraicGeometry.Scheme.Modules.pushforwardComp f g)).hom.app B))

Transposition along pullback of algebras is compatible with composition of scheme morphisms: transposing along f ≫ g, after the composition isomorphism (f ≫ g)^* A ≅ f^* g^* A, is transposing along f and then along g, followed by the composition isomorphism g_* f_* B ≅ (f ≫ g)_* B of pushforward.

theorem TauCeti.AlgebraicGeometry.QuasicoherentAlgebra.pullbackHomEquiv_id_hom_hom {X : AlgebraicGeometry.Scheme} (A : QuasicoherentAlgebra X) (B : CategoryTheory.CommMon X.Modules) (φ : A.obj ⟶ B) : ((pullbackHomEquiv (CategoryTheory.CategoryStruct.id X) A B) (CategoryTheory.CategoryStruct.comp ((pullbackId X).hom.app A).hom φ)).hom.hom = CategoryTheory.CategoryStruct.comp φ.hom.hom ((AlgebraicGeometry.Scheme.Modules.pushforwardId X).inv.app B.X)

Transposition along pullback of algebras by the identity is the identity, through the identity isomorphisms 𝟙^* A ≅ A and B ≅ 𝟙_* B of pullback and pushforward.