The relative-Spec anti-equivalence

Quasi-coherent commutative algebras on a scheme correspond contravariantly to schemes affine over it. The functors are relativeSpec and affineFunctions, the latter taking the actual pushforward of the structure sheaf. The unit identifies an algebra with functions on its relative spectrum; the counit recovers an affine morphism from its function algebra.

The triangle identities make these recovery isomorphisms compatible with both functors. The anti-equivalence allows questions about affine schemes over the base to be translated into questions about quasi-coherent commutative algebras, with the direction of morphisms reversed.

References

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

@[simp]

theorem CategoryTheory.CommMon.relativeSpecMap_relativeSpecPushforwardIso_hom_comp {X : AlgebraicGeometry.Scheme} (A : CommMon X.Modules) [SheafOfModules.IsQuasicoherent A.X] : CategoryStruct.comp (relativeSpecMap A.relativeSpecPushforwardIso.hom) (AlgebraicGeometry.Scheme.Hom.relativeSpecFunctionsToScheme A.relativeSpecToBase) = CategoryStruct.id A.relativeSpec

Applying relative Spec to the algebra-side unit and then recovering the scheme gives the identity on the relative spectrum.

@[simp]

theorem CategoryTheory.CommMon.relativeSpecMap_relativeSpecPushforwardIso_hom_comp_assoc {X : AlgebraicGeometry.Scheme} (A : CommMon X.Modules) [SheafOfModules.IsQuasicoherent A.X] {Z : AlgebraicGeometry.Scheme} (h : A.relativeSpec ⟶ Z) : CategoryStruct.comp (relativeSpecMap A.relativeSpecPushforwardIso.hom) (CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.relativeSpecFunctionsToScheme A.relativeSpecToBase) h) = h

Applying relative Spec to the algebra-side unit and then recovering the scheme gives the identity on the relative spectrum.

@[simp]

theorem TauCeti.AlgebraicGeometry.relativeSpec_unit_counit (X : AlgebraicGeometry.Scheme) (A : (QuasicoherentAlgebra X)ᵒᵖ) : CategoryTheory.CategoryStruct.comp ((relativeSpec X).map ((relativeSpecUnit X).hom.app A)) ((relativeSpecCounit X).hom.app ((relativeSpec X).obj A)) = CategoryTheory.CategoryStruct.id ((relativeSpec X).obj A)

The geometric triangle identity for the canonical relative-Spec unit and counit.

@[simp]

theorem TauCeti.AlgebraicGeometry.relativeSpec_unit_counit_assoc (X : AlgebraicGeometry.Scheme) (A : (QuasicoherentAlgebra X)ᵒᵖ) {Z : AffineSchemeOver X} (h : (relativeSpec X).obj A ⟶ Z) : CategoryTheory.CategoryStruct.comp ((relativeSpec X).map ((relativeSpecUnit X).hom.app A)) (CategoryTheory.CategoryStruct.comp ((relativeSpecCounit X).hom.app ((relativeSpec X).obj A)) h) = h

The geometric triangle identity for the canonical relative-Spec unit and counit.

noncomputable def TauCeti.AlgebraicGeometry.relativeSpecEquiv (X : AlgebraicGeometry.Scheme) : (QuasicoherentAlgebra X)ᵒᵖ ≌ AffineSchemeOver X

Relative Spec and the algebra of regular functions give an anti-equivalence between quasi-coherent commutative algebras and affine schemes over an arbitrary base scheme. Its unit and counit are the canonical section and affine-chart comparisons.

@[simp]

theorem TauCeti.AlgebraicGeometry.relativeSpecEquiv_functor (X : AlgebraicGeometry.Scheme) : (relativeSpecEquiv X).functor = relativeSpec X

The forward functor is the previously constructed relative spectrum.

@[simp]

theorem TauCeti.AlgebraicGeometry.relativeSpecEquiv_inverse (X : AlgebraicGeometry.Scheme) : (relativeSpecEquiv X).inverse = affineFunctions X

The inverse functor takes the actual algebra of regular functions.

@[simp]

theorem TauCeti.AlgebraicGeometry.relativeSpecEquiv_unitIso (X : AlgebraicGeometry.Scheme) : (relativeSpecEquiv X).unitIso ≪≫ CategoryTheory.eqToIso ⋯ = relativeSpecUnit X

The equivalence uses the canonical algebra-side comparison.

@[simp]

theorem TauCeti.AlgebraicGeometry.relativeSpecEquiv_counitIso (X : AlgebraicGeometry.Scheme) : CategoryTheory.eqToIso ⋯ ≪≫ (relativeSpecEquiv X).counitIso = relativeSpecCounit X

The equivalence uses the canonical geometric recovery comparison.

instance TauCeti.AlgebraicGeometry.relativeSpec_isEquivalence (X : AlgebraicGeometry.Scheme) : (relativeSpec X).IsEquivalence

Relative Spec is an equivalence, in particular fully faithful and essentially surjective.

instance TauCeti.AlgebraicGeometry.affineFunctions_isEquivalence (X : AlgebraicGeometry.Scheme) : (affineFunctions X).IsEquivalence

Taking functions is an equivalence, in particular fully faithful and essentially surjective.

theorem TauCeti.AlgebraicGeometry.affineFunctions_unit_counit (X : AlgebraicGeometry.Scheme) (V : AffineSchemeOver X) : CategoryTheory.CategoryStruct.comp ((relativeSpecUnit X).hom.app ((affineFunctions X).obj V)) ((affineFunctions X).map ((relativeSpecCounit X).hom.app V)) = CategoryTheory.CategoryStruct.id ((affineFunctions X).obj V)

The algebraic triangle identity for the canonical relative-Spec comparisons.

theorem TauCeti.AlgebraicGeometry.affineFunctions_unit_counit_assoc (X : AlgebraicGeometry.Scheme) (V : AffineSchemeOver X) {Z : (QuasicoherentAlgebra X)ᵒᵖ} (h : (affineFunctions X).obj V ⟶ Z) : CategoryTheory.CategoryStruct.comp ((relativeSpecUnit X).hom.app ((affineFunctions X).obj V)) (CategoryTheory.CategoryStruct.comp ((affineFunctions X).map ((relativeSpecCounit X).hom.app V)) h) = h

The algebraic triangle identity for the canonical relative-Spec comparisons.

@[simp]

theorem TauCeti.AlgebraicGeometry.affineFunctions_map_relativeSpecCounit_hom_app (X : AlgebraicGeometry.Scheme) (V : AffineSchemeOver X) : (affineFunctions X).map ((relativeSpecCounit X).hom.app V) = (relativeSpecUnit X).inv.app ((affineFunctions X).obj V)

The algebraic triangle identity, inverted: on function algebras, the relative-Spec counit is the inverse of the relative-Spec unit.