Functoriality of relative Spec

A morphism of quasi-coherent commutative algebras on a scheme induces a morphism of relative spectra in the opposite direction. On each affine open, this is the spectrum of the induced algebra homomorphism on sections. These chart maps determine the global morphism uniquely and commute with the structure morphisms to the base.

We package this construction as TauCeti.AlgebraicGeometry.relativeSpec, from the opposite category of quasi-coherent algebras to affine schemes over the base. The functor provides the geometric side of the correspondence between quasi-coherent commutative algebras and affine schemes over the base, and is an input to the natural universal property of relative Spec.

References

• The Stacks Project, Tag 01LL (relative spectrum).
• A. Grothendieck and J. Dieudonné, Éléments de géométrie algébrique II, §1.3.

noncomputable def CategoryTheory.CommMon.relativeSpecMap {X : AlgebraicGeometry.Scheme} {A B : CommMon X.Modules} [SheafOfModules.IsQuasicoherent A.X] [SheafOfModules.IsQuasicoherent B.X] (f : A ⟶ B) : B.relativeSpec ⟶ A.relativeSpec

The relative spectrum of an algebra morphism, contravariant in the algebra.

Equations

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

@[simp]

theorem CategoryTheory.CommMon.relativeSpecCover_f_relativeSpecMap {X : AlgebraicGeometry.Scheme} {A B : CommMon X.Modules} [SheafOfModules.IsQuasicoherent A.X] [SheafOfModules.IsQuasicoherent B.X] (f : A ⟶ B) (U : X.AffineZariskiSite) : CategoryStruct.comp (B.relativeSpecCover.f U) (relativeSpecMap f) = CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (sectionsAlgHom f ↑U).toRingHom)) (A.relativeSpecCover.f U)

On an affine chart, the relative-spectrum map is Spec of the algebra map on sections.

@[simp]

theorem CategoryTheory.CommMon.relativeSpecCover_f_relativeSpecMap_assoc {X : AlgebraicGeometry.Scheme} {A B : CommMon X.Modules} [SheafOfModules.IsQuasicoherent A.X] [SheafOfModules.IsQuasicoherent B.X] (f : A ⟶ B) (U : X.AffineZariskiSite) {Z : AlgebraicGeometry.Scheme} (h : A.relativeSpec ⟶ Z) : CategoryStruct.comp (B.relativeSpecCover.f U) (CategoryStruct.comp (relativeSpecMap f) h) = CategoryStruct.comp (CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (sectionsAlgHom f ↑U).toRingHom)) (A.relativeSpecCover.f U)) h

On an affine chart, the relative-spectrum map is Spec of the algebra map on sections.

theorem CategoryTheory.CommMon.relativeSpec_hom_ext {X : AlgebraicGeometry.Scheme} (A : CommMon X.Modules) [SheafOfModules.IsQuasicoherent A.X] {T : AlgebraicGeometry.Scheme} (f g : A.relativeSpec ⟶ T) (h : ∀ (U : X.AffineZariskiSite), CategoryStruct.comp (A.relativeSpecCover.f U) f = CategoryStruct.comp (A.relativeSpecCover.f U) g) : f = g

Maps out of a relative spectrum are determined on its affine charts.

theorem CategoryTheory.CommMon.relativeSpec_hom_ext_iff {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} [SheafOfModules.IsQuasicoherent A.X] {T : AlgebraicGeometry.Scheme} {f g : A.relativeSpec ⟶ T} : f = g ↔ ∀ (U : X.AffineZariskiSite), CategoryStruct.comp (A.relativeSpecCover.f U) f = CategoryStruct.comp (A.relativeSpecCover.f U) g

@[simp]

theorem CategoryTheory.CommMon.relativeSpecMap_relativeSpecToBase {X : AlgebraicGeometry.Scheme} {A B : CommMon X.Modules} [SheafOfModules.IsQuasicoherent A.X] [SheafOfModules.IsQuasicoherent B.X] (f : A ⟶ B) : CategoryStruct.comp (relativeSpecMap f) A.relativeSpecToBase = B.relativeSpecToBase

The relative-spectrum map commutes with the structure morphism to the base.

@[simp]

theorem CategoryTheory.CommMon.relativeSpecMap_relativeSpecToBase_assoc {X : AlgebraicGeometry.Scheme} {A B : CommMon X.Modules} [SheafOfModules.IsQuasicoherent A.X] [SheafOfModules.IsQuasicoherent B.X] (f : A ⟶ B) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryStruct.comp (relativeSpecMap f) (CategoryStruct.comp A.relativeSpecToBase h) = CategoryStruct.comp B.relativeSpecToBase h

The relative-spectrum map commutes with the structure morphism to the base.

@[simp]

theorem CategoryTheory.CommMon.relativeSpecMap_id {X : AlgebraicGeometry.Scheme} (A : CommMon X.Modules) [SheafOfModules.IsQuasicoherent A.X] : relativeSpecMap (CategoryStruct.id A) = CategoryStruct.id A.relativeSpec

@[simp]

theorem CategoryTheory.CommMon.relativeSpecMap_comp {X : AlgebraicGeometry.Scheme} {A B C : CommMon X.Modules} [SheafOfModules.IsQuasicoherent A.X] [SheafOfModules.IsQuasicoherent B.X] [SheafOfModules.IsQuasicoherent C.X] (f : A ⟶ B) (g : B ⟶ C) : relativeSpecMap (CategoryStruct.comp f g) = CategoryStruct.comp (relativeSpecMap g) (relativeSpecMap f)

@[reducible, inline]

abbrev TauCeti.AlgebraicGeometry.QuasicoherentAlgebra (X : AlgebraicGeometry.Scheme) : Type (u + 1)

Quasi-coherent commutative algebras on a scheme, with algebra morphisms.

Equations

• TauCeti.AlgebraicGeometry.QuasicoherentAlgebra X = (have this := fun (A : CategoryTheory.CommMon X.Modules) => SheafOfModules.IsQuasicoherent A.X; this).FullSubcategory

instance TauCeti.AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatXModulesObjCommMon_tauCeti {X : AlgebraicGeometry.Scheme} (A : QuasicoherentAlgebra X) : SheafOfModules.IsQuasicoherent A.obj.X

@[reducible, inline]

abbrev TauCeti.AlgebraicGeometry.AffineSchemeOver (X : AlgebraicGeometry.Scheme) : Type (u + 1)

Affine schemes over X: the structure morphism, not necessarily the scheme, is affine. Morphisms are arbitrary scheme morphisms over X.

Equations

• TauCeti.AlgebraicGeometry.AffineSchemeOver X = CategoryTheory.MorphismProperty.Over @AlgebraicGeometry.IsAffineHom ⊤ X

@[instance_reducible]

instance TauCeti.AlgebraicGeometry.instCategoryAffineSchemeOver {X : AlgebraicGeometry.Scheme} : CategoryTheory.Category.{u, u + 1} (AffineSchemeOver X)

Equations

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

instance TauCeti.AlgebraicGeometry.instIsAffineHomHomSchemeDiscretePUnit_tauCeti {X : AlgebraicGeometry.Scheme} (V : AffineSchemeOver X) : AlgebraicGeometry.IsAffineHom V.hom

noncomputable def TauCeti.AlgebraicGeometry.relativeSpec (X : AlgebraicGeometry.Scheme) : CategoryTheory.Functor (QuasicoherentAlgebra X)ᵒᵖ (AffineSchemeOver X)

Relative Spec as a contravariant functor from quasi-coherent commutative algebras to schemes affine over the base.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.relativeSpec_obj_left {X : AlgebraicGeometry.Scheme} (A : (QuasicoherentAlgebra X)ᵒᵖ) : ((relativeSpec X).obj A).left = (Opposite.unop A).obj.relativeSpec

@[simp]

theorem TauCeti.AlgebraicGeometry.relativeSpec_obj_hom {X : AlgebraicGeometry.Scheme} (A : (QuasicoherentAlgebra X)ᵒᵖ) : ((relativeSpec X).obj A).hom = (Opposite.unop A).obj.relativeSpecToBase

@[simp]

theorem TauCeti.AlgebraicGeometry.relativeSpec_map_left {X : AlgebraicGeometry.Scheme} {A B : (QuasicoherentAlgebra X)ᵒᵖ} (f : A ⟶ B) : ((relativeSpec X).map f).left = CategoryTheory.CommMon.relativeSpecMap f.unop.hom