Relative Spec recovers its algebra

For a quasi-coherent commutative algebra A on a scheme X, with structure morphism p : Spec_X A ⟶ X, the algebra of regular functions p_* 𝒪 of the relative spectrum is canonically isomorphic to A. Above an affine open U of X, the inverse image of U is the chart Spec Γ(A.X, U), and the comparison is the usual identification of the global functions on this spectrum with Γ(A.X, U). These comparisons are natural in U, so they extend uniquely from affine opens to an isomorphism of sheaves of rings; it respects the structure maps from 𝒪ₓ, hence is an isomorphism of algebras. It is natural in A, which gives the algebra-side unit of the correspondence between quasi-coherent algebras and affine schemes over X.

Main declarations

• CategoryTheory.CommMon.relativeSpecCoverFunctionAlgebraSectionsRingEquiv: over an affine open, the sections of p_* 𝒪 are the sections of A;
• CategoryTheory.CommMon.relativeSpecPushforwardIso: the isomorphism of algebras p_* 𝒪 ≅ A, and its naturality relativeSpecPushforwardIso_hom_naturality;
• TauCeti.AlgebraicGeometry.relativeSpecUnit: the natural isomorphism 𝟭 ≅ relativeSpec X ⋙ affineFunctions X.

References

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

theorem CategoryTheory.CommMon.top_le_preimage_relativeSpecToBase {X : AlgebraicGeometry.Scheme} (A : CommMon X.Modules) [SheafOfModules.IsQuasicoherent A.X] (U : X.AffineZariskiSite) : ⊤ ≤ (TopologicalSpace.Opens.map (A.relativeSpecCover.f U).base).obj ((TopologicalSpace.Opens.map A.relativeSpecToBase.base).obj U.toOpens)

The chart of the relative spectrum over an affine open U lies over U.

noncomputable def CategoryTheory.CommMon.relativeSpecCoverFunctionAlgebraSectionsRingEquiv {X : AlgebraicGeometry.Scheme} (A : CommMon X.Modules) [SheafOfModules.IsQuasicoherent A.X] (U : X.AffineZariskiSite) : ↑((AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebra A.relativeSpecToBase).X.presheaf.obj (Opposite.op ↑U)) ≃+* ↑(A.X.presheaf.obj (Opposite.op ↑U))

Sections of the function algebra of Spec_X A above an affine open are the sections of A.

The isomorphism identifies the inverse image of the affine open U with the chart Spec Γ(A.X, U), then uses the ordinary identification of the global functions on a spectrum.

theorem CategoryTheory.CommMon.relativeSpecCoverFunctionAlgebraSectionsRingEquiv_apply {X : AlgebraicGeometry.Scheme} (A : CommMon X.Modules) [SheafOfModules.IsQuasicoherent A.X] (U : X.AffineZariskiSite) (x : ↑((AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebra A.relativeSpecToBase).X.presheaf.obj (Opposite.op ↑U))) : (A.relativeSpecCoverFunctionAlgebraSectionsRingEquiv U) x = (ConcreteCategory.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧↑(A.X.presheaf.obj (Opposite.op ↑U))).hom) ((ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appLE (A.relativeSpecCover.f U) ((TopologicalSpace.Opens.map A.relativeSpecToBase.base).obj U.toOpens) ⊤ ⋯)) ((AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebraSectionsRingEquiv A.relativeSpecToBase ↑U) x))

Over an affine open U, the section comparison pulls a function back along the chart Spec Γ(A.X, U) and evaluates it through Scheme.ΓSpecIso.

noncomputable def CategoryTheory.CommMon.relativeSpecPushforwardIso {X : AlgebraicGeometry.Scheme} (A : CommMon X.Modules) [SheafOfModules.IsQuasicoherent A.X] : AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebra A.relativeSpecToBase ≅ A

The algebra-side unit of relative Spec: the function algebra p_* 𝒪 of the relative spectrum p : Spec_X A ⟶ X is isomorphic to A. Over each affine open U, it is the identification of the functions on the chart Spec Γ(A.X, U) with Γ(A.X, U) (CategoryTheory.CommMon.sectionsAlgHom_relativeSpecPushforwardIso_hom_apply).

theorem CategoryTheory.CommMon.sectionsAlgHom_relativeSpecPushforwardIso_hom_apply {X : AlgebraicGeometry.Scheme} (A : CommMon X.Modules) [SheafOfModules.IsQuasicoherent A.X] (U : X.AffineZariskiSite) (x : ↑((AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebra A.relativeSpecToBase).X.presheaf.obj (Opposite.op ↑U))) : (sectionsAlgHom A.relativeSpecPushforwardIso.hom ↑U) x = (A.relativeSpecCoverFunctionAlgebraSectionsRingEquiv U) x

Over an affine open, the isomorphism p_* 𝒪 ≅ A is the section comparison relativeSpecCoverFunctionAlgebraSectionsRingEquiv.

theorem CategoryTheory.CommMon.relativeSpecPushforwardIso_hom_naturality {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} [SheafOfModules.IsQuasicoherent A.X] {B : CommMon X.Modules} [SheafOfModules.IsQuasicoherent B.X] (f : A ⟶ B) : CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebraMap (relativeSpecMap f) ⋯) B.relativeSpecPushforwardIso.hom = CategoryStruct.comp A.relativeSpecPushforwardIso.hom f

The isomorphism p_* 𝒪 ≅ A is natural in the algebra: pulling back functions along Spec_X B ⟶ Spec_X A corresponds to the algebra morphism A ⟶ B.

theorem CategoryTheory.CommMon.relativeSpecPushforwardIso_hom_naturality_assoc {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} [SheafOfModules.IsQuasicoherent A.X] {B : CommMon X.Modules} [SheafOfModules.IsQuasicoherent B.X] (f : A ⟶ B) {Z : CommMon X.Modules} (h : B ⟶ Z) : CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebraMap (relativeSpecMap f) ⋯) (CategoryStruct.comp B.relativeSpecPushforwardIso.hom h) = CategoryStruct.comp A.relativeSpecPushforwardIso.hom (CategoryStruct.comp f h)

The isomorphism p_* 𝒪 ≅ A is natural in the algebra: pulling back functions along Spec_X B ⟶ Spec_X A corresponds to the algebra morphism A ⟶ B.

noncomputable def TauCeti.AlgebraicGeometry.relativeSpecUnit (X : AlgebraicGeometry.Scheme) : CategoryTheory.Functor.id (QuasicoherentAlgebra X)ᵒᵖ ≅ (relativeSpec X).comp (affineFunctions X)

The algebra-side unit of relative Spec: a quasi-coherent algebra is naturally the function algebra of its relative spectrum.

@[simp]

theorem TauCeti.AlgebraicGeometry.relativeSpecUnit_hom_app_unop_hom {X : AlgebraicGeometry.Scheme} (A : (QuasicoherentAlgebra X)ᵒᵖ) : ((relativeSpecUnit X).hom.app A).unop.hom = (Opposite.unop A).obj.relativeSpecPushforwardIso.hom

The unit on underlying algebras is the isomorphism p_* 𝒪 ≅ A.

@[simp]

theorem TauCeti.AlgebraicGeometry.relativeSpecUnit_inv_app_unop_hom {X : AlgebraicGeometry.Scheme} (A : (QuasicoherentAlgebra X)ᵒᵖ) : ((relativeSpecUnit X).inv.app A).unop.hom = (Opposite.unop A).obj.relativeSpecPushforwardIso.inv

The inverse unit on underlying algebras is the inverse of the isomorphism p_* 𝒪 ≅ A.