Recovering an affine morphism from its function algebra

For an affine morphism p : V ⟶ X, the relative spectrum of the actual function algebra p_* 𝒪_V is canonically isomorphic to V, over X. On an affine open U of X, the isomorphism is the usual affine identification of p⁻¹ U with the spectrum of its regular functions. These identifications glue and are natural in morphisms over the base.

The resulting relativeSpecCounit is the geometric counit for the correspondence between quasi-coherent algebras and affine morphisms. No affineness assumption on the base is needed.

References

• The Stacks Project, Tag 01LL (relative spectrum).
• The local isomorphism argument follows Mathlib's Scheme.AffineZariskiSite.isColimitCocone in Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski.

noncomputable def AlgebraicGeometry.Scheme.Hom.relativeSpecFunctionsToScheme {X V : Scheme} (p : V ⟶ X) [IsAffineHom p] : (pushforwardStructureAlgebra p).relativeSpec ⟶ V

The canonical map from the relative spectrum of an affine morphism's function algebra back to its source, obtained by gluing the affine identifications on inverse images.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.relativeSpecCover_f_relativeSpecFunctionsToScheme {X V : Scheme} (p : V ⟶ X) [IsAffineHom p] (U : X.AffineZariskiSite) : CategoryTheory.CategoryStruct.comp ((pushforwardStructureAlgebra p).relativeSpecCover.f U) (relativeSpecFunctionsToScheme p) = CategoryTheory.CategoryStruct.comp (Spec.map ((pushforwardStructureAlgebraPresheafIso p).inv.app (Opposite.op ↑U))) ⋯.fromSpec

On each affine open of the base, recovery from the function algebra is the ordinary affine chart map on its inverse image.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.relativeSpecCover_f_relativeSpecFunctionsToScheme_assoc {X V : Scheme} (p : V ⟶ X) [IsAffineHom p] (U : X.AffineZariskiSite) {Z : Scheme} (h : V ⟶ Z) : CategoryTheory.CategoryStruct.comp ((pushforwardStructureAlgebra p).relativeSpecCover.f U) (CategoryTheory.CategoryStruct.comp (relativeSpecFunctionsToScheme p) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (Spec.map ((pushforwardStructureAlgebraPresheafIso p).inv.app (Opposite.op ↑U))) ⋯.fromSpec) h

On each affine open of the base, recovery from the function algebra is the ordinary affine chart map on its inverse image.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.relativeSpecFunctionsToScheme_comp {X V : Scheme} (p : V ⟶ X) [IsAffineHom p] : CategoryTheory.CategoryStruct.comp (relativeSpecFunctionsToScheme p) p = (pushforwardStructureAlgebra p).relativeSpecToBase

Recovery from the function algebra respects the structure morphism to the base.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.relativeSpecFunctionsToScheme_comp_assoc {X V : Scheme} (p : V ⟶ X) [IsAffineHom p] {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (relativeSpecFunctionsToScheme p) (CategoryTheory.CategoryStruct.comp p h) = CategoryTheory.CategoryStruct.comp (pushforwardStructureAlgebra p).relativeSpecToBase h

Recovery from the function algebra respects the structure morphism to the base.

instance AlgebraicGeometry.Scheme.Hom.isIso_relativeSpecFunctionsToScheme {X V : Scheme} (p : V ⟶ X) [IsAffineHom p] : CategoryTheory.IsIso (relativeSpecFunctionsToScheme p)

An affine scheme over a base is recovered from its actual algebra of regular functions.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.relativeSpecFunctionsToScheme_naturality {X V W : Scheme} {p : V ⟶ X} [IsAffineHom p] {q : W ⟶ X} [IsAffineHom q] (g : V ⟶ W) (h : CategoryTheory.CategoryStruct.comp g q = p) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CommMon.relativeSpecMap (pushforwardStructureAlgebraMap g h)) (relativeSpecFunctionsToScheme q) = CategoryTheory.CategoryStruct.comp (relativeSpecFunctionsToScheme p) g

Recovery of an affine morphism from its function algebra is natural in scheme morphisms over the base.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.relativeSpecFunctionsToScheme_naturality_assoc {X V W : Scheme} {p : V ⟶ X} [IsAffineHom p] {q : W ⟶ X} [IsAffineHom q] (g : V ⟶ W) (h : CategoryTheory.CategoryStruct.comp g q = p) {Z : Scheme} (h✝ : W ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CommMon.relativeSpecMap (pushforwardStructureAlgebraMap g h)) (CategoryTheory.CategoryStruct.comp (relativeSpecFunctionsToScheme q) h✝) = CategoryTheory.CategoryStruct.comp (relativeSpecFunctionsToScheme p) (CategoryTheory.CategoryStruct.comp g h✝)

Recovery of an affine morphism from its function algebra is natural in scheme morphisms over the base.

theorem AlgebraicGeometry.Scheme.Hom.inv_relativeSpecFunctionsToScheme_naturality {X V W : Scheme} {p : V ⟶ X} [IsAffineHom p] {q : W ⟶ X} [IsAffineHom q] (g : V ⟶ W) (h : CategoryTheory.CategoryStruct.comp g q = p) : CategoryTheory.CategoryStruct.comp g (CategoryTheory.inv (relativeSpecFunctionsToScheme q)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (relativeSpecFunctionsToScheme p)) (CategoryTheory.CommMon.relativeSpecMap (pushforwardStructureAlgebraMap g h))

The inverse form of Scheme.Hom.relativeSpecFunctionsToScheme_naturality: a scheme morphism over the base is, through the identifications with the relative spectra of the function algebras, the relative spectrum of pullback of functions.

theorem AlgebraicGeometry.Scheme.Hom.inv_relativeSpecFunctionsToScheme_naturality_assoc {X V W : Scheme} {p : V ⟶ X} [IsAffineHom p] {q : W ⟶ X} [IsAffineHom q] (g : V ⟶ W) (h : CategoryTheory.CategoryStruct.comp g q = p) {Z : Scheme} (h✝ : (pushforwardStructureAlgebra q).relativeSpec ⟶ Z) : CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (relativeSpecFunctionsToScheme q)) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (relativeSpecFunctionsToScheme p)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CommMon.relativeSpecMap (pushforwardStructureAlgebraMap g h)) h✝)

The inverse form of Scheme.Hom.relativeSpecFunctionsToScheme_naturality: a scheme morphism over the base is, through the identifications with the relative spectra of the function algebras, the relative spectrum of pullback of functions.

noncomputable def AlgebraicGeometry.Scheme.Hom.relativeSpecFunctionsIso {X V : Scheme} (p : V ⟶ X) [IsAffineHom p] : (pushforwardStructureAlgebra p).relativeSpec ≅ V

The canonical isomorphism recovering an affine scheme over X from its function algebra. Its forward map is the gluing of the ordinary affine identifications on inverse images.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.relativeSpecFunctionsIso_hom {X V : Scheme} (p : V ⟶ X) [IsAffineHom p] : (relativeSpecFunctionsIso p).hom = relativeSpecFunctionsToScheme p

The forward recovery isomorphism is the canonical map glued from affine charts.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.relativeSpecFunctionsIso_inv {X V : Scheme} (p : V ⟶ X) [IsAffineHom p] : (relativeSpecFunctionsIso p).inv = CategoryTheory.inv (relativeSpecFunctionsToScheme p)

The inverse recovery map is the categorical inverse of the canonical affine recovery.

noncomputable def TauCeti.AlgebraicGeometry.relativeSpecCounit (X : AlgebraicGeometry.Scheme) : (affineFunctions X).comp (relativeSpec X) ≅ CategoryTheory.Functor.id (AffineSchemeOver X)

The geometric counit: an affine scheme over X is naturally the relative spectrum of its actual quasi-coherent algebra of regular functions.

@[simp]

theorem TauCeti.AlgebraicGeometry.relativeSpecCounit_hom_app_left {X : AlgebraicGeometry.Scheme} (V : AffineSchemeOver X) : ((relativeSpecCounit X).hom.app V).left = AlgebraicGeometry.Scheme.Hom.relativeSpecFunctionsToScheme V.hom

The counit on underlying schemes is the canonical recovery map from the function algebra.

@[simp]

theorem TauCeti.AlgebraicGeometry.relativeSpecCounit_inv_app_left {X : AlgebraicGeometry.Scheme} (V : AffineSchemeOver X) : ((relativeSpecCounit X).inv.app V).left = CategoryTheory.inv (AlgebraicGeometry.Scheme.Hom.relativeSpecFunctionsToScheme V.hom)

On underlying schemes, the inverse counit is the inverse of the canonical recovery map.