Relative Spec over an affine scheme

For a quasi-coherent commutative algebra A on an affine scheme X, the relative spectrum is canonically Spec Γ(A.X, ⊤). The inverse of this identification is the chart inclusion over the whole base. It respects the structure morphism to X and is natural in algebra morphisms, identifying relative Spec on an affine base with the usual contravariant spectrum of the algebra of global sections.

The construction uses CommMon.isPullback_relativeSpecCover: the chart over the whole base is an isomorphism because it is the pullback of the isomorphism X.topIso.hom.

References

• The Stacks Project, Tag 01LL, Lemma 27.3.4 (relative spectrum via gluing).

instance CategoryTheory.CommMon.isIso_relativeSpecCover_f_top {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] (A : CommMon X.Modules) [SheafOfModules.IsQuasicoherent A.X] : IsIso (A.relativeSpecCover.f ⟨⊤, ⋯⟩)

Over an affine base, the chart of relative Spec over the whole base is an isomorphism.

noncomputable def CategoryTheory.CommMon.relativeSpecIsoSpec {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] (A : CommMon X.Modules) [SheafOfModules.IsQuasicoherent A.X] : A.relativeSpec ≅ AlgebraicGeometry.Spec ↧↑(A.X.presheaf.obj (Opposite.op ⊤))

Relative Spec over an affine scheme is the spectrum of the algebra of global sections. The inverse is the chart inclusion over the whole base.

Equations

• A.relativeSpecIsoSpec = (CategoryTheory.asIso (A.relativeSpecCover.f ⟨⊤, ⋯⟩)).symm

@[simp]

theorem CategoryTheory.CommMon.relativeSpecIsoSpec_inv {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] (A : CommMon X.Modules) [SheafOfModules.IsQuasicoherent A.X] : A.relativeSpecIsoSpec.inv = A.relativeSpecCover.f ⟨⊤, ⋯⟩

The inverse affine normalization is the chart inclusion over the whole base.

theorem CategoryTheory.CommMon.relativeSpecIsoSpec_inv_relativeSpecToBase {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] (A : CommMon X.Modules) [SheafOfModules.IsQuasicoherent A.X] : CategoryStruct.comp A.relativeSpecIsoSpec.inv A.relativeSpecToBase = CategoryStruct.comp (AlgebraicGeometry.Spec.map (A.toSectionsPresheaf.app (Opposite.op ⊤))) X.isoSpec.inv

Affine normalization identifies the map to the base with Spec of the structure map on global sections, followed by the affine identification of the base.

theorem CategoryTheory.CommMon.relativeSpecIsoSpec_inv_relativeSpecToBase_assoc {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] (A : CommMon X.Modules) [SheafOfModules.IsQuasicoherent A.X] {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryStruct.comp A.relativeSpecIsoSpec.inv (CategoryStruct.comp A.relativeSpecToBase h) = CategoryStruct.comp (CategoryStruct.comp (AlgebraicGeometry.Spec.map (A.toSectionsPresheaf.app (Opposite.op ⊤))) X.isoSpec.inv) h

Affine normalization identifies the map to the base with Spec of the structure map on global sections, followed by the affine identification of the base.

@[simp]

theorem CategoryTheory.CommMon.relativeSpecIsoSpec_hom_toBase {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] (A : CommMon X.Modules) [SheafOfModules.IsQuasicoherent A.X] : CategoryStruct.comp A.relativeSpecIsoSpec.hom (CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ↑(X.presheaf.obj (Opposite.op ⊤)) ↑(A.X.presheaf.obj (Opposite.op ⊤))))) X.isoSpec.inv) = A.relativeSpecToBase

The affine coordinate description of the structure morphism of relative Spec.

@[simp]

theorem CategoryTheory.CommMon.relativeSpecIsoSpec_hom_toBase_assoc {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] (A : CommMon X.Modules) [SheafOfModules.IsQuasicoherent A.X] {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryStruct.comp A.relativeSpecIsoSpec.hom (CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ↑(X.presheaf.obj (Opposite.op ⊤)) ↑(A.X.presheaf.obj (Opposite.op ⊤))))) (CategoryStruct.comp X.isoSpec.inv h)) = CategoryStruct.comp A.relativeSpecToBase h

The affine coordinate description of the structure morphism of relative Spec.

@[simp]

theorem CategoryTheory.CommMon.relativeSpecIsoSpec_hom_naturality {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] {A : CommMon X.Modules} [SheafOfModules.IsQuasicoherent A.X] {B : CommMon X.Modules} [SheafOfModules.IsQuasicoherent B.X] (f : A ⟶ B) : CategoryStruct.comp (relativeSpecMap f) A.relativeSpecIsoSpec.hom = CategoryStruct.comp B.relativeSpecIsoSpec.hom (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (sectionsAlgHom f ⊤).toRingHom))

Affine normalization is contravariantly natural in the quasi-coherent algebra.

@[simp]

theorem CategoryTheory.CommMon.relativeSpecIsoSpec_hom_naturality_assoc {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] {A : CommMon X.Modules} [SheafOfModules.IsQuasicoherent A.X] {B : CommMon X.Modules} [SheafOfModules.IsQuasicoherent B.X] (f : A ⟶ B) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧↑(A.X.presheaf.obj (Opposite.op ⊤)) ⟶ Z) : CategoryStruct.comp (relativeSpecMap f) (CategoryStruct.comp A.relativeSpecIsoSpec.hom h) = CategoryStruct.comp B.relativeSpecIsoSpec.hom (CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (sectionsAlgHom f ⊤).toRingHom)) h)

Affine normalization is contravariantly natural in the quasi-coherent algebra.

noncomputable def TauCeti.AlgebraicGeometry.specGlobalSections (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] : CategoryTheory.Functor (QuasicoherentAlgebra X)ᵒᵖ (AffineSchemeOver X)

On an affine base, take the spectrum of the global sections of a quasi-coherent algebra, with its structure map to the base induced by the algebra map on global sections.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.specGlobalSections_obj_left (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] (A : (QuasicoherentAlgebra X)ᵒᵖ) : ((specGlobalSections X).obj A).left = AlgebraicGeometry.Spec ↧↑((Opposite.unop A).obj.X.presheaf.obj (Opposite.op ⊤))

The scheme obtained by the global-sections construction is the ordinary spectrum of the ring of global sections of the algebra.

@[simp]

theorem TauCeti.AlgebraicGeometry.specGlobalSections_obj_hom (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] (A : (QuasicoherentAlgebra X)ᵒᵖ) : ((specGlobalSections X).obj A).hom = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map ((Opposite.unop A).obj.toSectionsPresheaf.app (Opposite.op ⊤))) X.isoSpec.inv

The structure morphism of the global-sections construction is induced by the algebra map.

@[simp]

theorem TauCeti.AlgebraicGeometry.specGlobalSections_map_left (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] {A B : (QuasicoherentAlgebra X)ᵒᵖ} (f : A ⟶ B) : ((specGlobalSections X).map f).left = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (CategoryTheory.CommMon.sectionsAlgHom f.unop.hom ⊤).toRingHom)

On morphisms, the global-sections construction is Spec of the algebra homomorphism on global sections.

noncomputable def TauCeti.AlgebraicGeometry.relativeSpecAffineIso (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] : relativeSpec X ≅ specGlobalSections X

On an affine base, relative Spec is naturally the usual spectrum of global sections, as a functor to affine schemes over the base.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.relativeSpecAffineIso_hom_app_left (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] (A : (QuasicoherentAlgebra X)ᵒᵖ) : ((relativeSpecAffineIso X).hom.app A).left = (Opposite.unop A).obj.relativeSpecIsoSpec.hom

The components of affine normalization use the canonical chart isomorphisms.

@[simp]

theorem TauCeti.AlgebraicGeometry.relativeSpecAffineIso_inv_app_left (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] (A : (QuasicoherentAlgebra X)ᵒᵖ) : ((relativeSpecAffineIso X).inv.app A).left = (Opposite.unop A).obj.relativeSpecCover.f ⟨⊤, ⋯⟩

The inverse component of affine normalization is the chart over the whole affine base.