The coordinate algebra of an affine scheme over a base

A scheme p : V ⟶ X over X has a commutative 𝒪ₓ-algebra of regular functions, carried by the actual pushforward p_* 𝒪_V (AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebra), and a morphism g : V ⟶ W over X pulls back regular functions (AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebraMap). When the structure morphism is affine, the algebra of regular functions is quasi-coherent, so this defines the functor

affineFunctions X : AffineSchemeOver X ⥤ (QuasicoherentAlgebra X)ᵒᵖ

in the direction opposite to TauCeti.AlgebraicGeometry.relativeSpec X. These are the two functors of the anti-equivalence between quasi-coherent commutative 𝒪ₓ-algebras and affine schemes over X.

Main declarations

• AlgebraicGeometry.Scheme.Hom.isQuasicoherent_pushforwardStructureAlgebra: the function algebra of an affine morphism is quasi-coherent;
• TauCeti.AlgebraicGeometry.affineFunctions X: the coordinate-algebra functor from affine schemes over X to quasi-coherent commutative 𝒪ₓ-algebras.

References

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

instance AlgebraicGeometry.Scheme.Hom.isQuasicoherent_pushforwardStructureAlgebra {X V : Scheme} (p : V ⟶ X) [IsAffineHom p] : SheafOfModules.IsQuasicoherent (pushforwardStructureAlgebra p).X

The function algebra p_* 𝒪_V of an affine morphism p : V ⟶ X is quasi-coherent.

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

The coordinate-algebra functor: an affine scheme p : V ⟶ X over X goes to its quasi-coherent algebra of regular functions p_* 𝒪_V, and a morphism over X goes to pullback of regular functions along it.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.affineFunctions_obj_unop_obj {X : AlgebraicGeometry.Scheme} (V : AffineSchemeOver X) : (Opposite.unop ((affineFunctions X).obj V)).obj = AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebra V.hom

The coordinate algebra of p : V ⟶ X is the function algebra p_* 𝒪_V.

@[simp]

theorem TauCeti.AlgebraicGeometry.affineFunctions_map_unop_hom {X : AlgebraicGeometry.Scheme} {V W : AffineSchemeOver X} (g : V ⟶ W) : ((affineFunctions X).map g).unop.hom = AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebraMap g.left ⋯

The coordinate-algebra functor sends a morphism over X to pullback of regular functions.