Points of an affine scheme over an affine base

Let f : X ⟶ Spec R be a morphism from an affine scheme to the spectrum of a commutative ring. Its points with values in Spec R, that is the sections of f, are the characters Γ(X, ⊤) →ₐ[R] R of its coordinate ring. This is TauCeti.AlgebraicGeometry.specOverHomEquivAlgHom (the OverClass form of Mathlib's AlgebraicGeometry.Spec.homEquivAlgHom), read through X ≅ Spec Γ(X, ⊤).

Points over Spec R are written as morphisms 𝟙_ (Over (Spec R)) ⟶ Over.mk f of the cartesian monoidal category Over (Spec R), as for the points of group schemes over Spec R.

Main definitions

• AlgebraicGeometry.Scheme.Hom.pointsEquivAlgHom: for affine X, the points of X over Spec R are the characters of Γ(X, ⊤).

Main results

• AlgebraicGeometry.Scheme.Hom.pointsEquivAlgHom_apply: the character attached to a point pulls back functions along it.
• AlgebraicGeometry.Scheme.Hom.pointsEquivAlgHom_symm_apply_left: the point attached to a character φ is Spec φ.

noncomputable def AlgebraicGeometry.Scheme.Hom.pointsEquivAlgHom {R : Type u} [CommRing R] {X : Scheme} (f : X ⟶ Spec ↧R) [IsAffine X] [Algebra R ↑(X.presheaf.obj (Opposite.op ⊤))] (hf : algebraMap R ↑(X.presheaf.obj (Opposite.op ⊤)) = CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (ΓSpecIso ↧R).inv (appTop f))) : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (Spec ↧R)) ⟶ CategoryTheory.Over.mk f) ≃ (↑(X.presheaf.obj (Opposite.op ⊤)) →ₐ[R] R)

The points of an affine scheme over Spec R are the characters of its coordinate ring. Let f : X ⟶ Spec R be a morphism from an affine scheme, and give Γ(X, ⊤) the R-algebra structure of the map of global sections of f (the hypothesis hf). A point x of X over Spec R, that is a section of f, corresponds to the character of Γ(X, ⊤) given by pulling back functions along x. This is TauCeti.AlgebraicGeometry.specOverHomEquivAlgHom, read through X ≅ Spec Γ(X, ⊤).

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.pointsEquivAlgHom_apply {R : Type u} [CommRing R] {X : Scheme} (f : X ⟶ Spec ↧R) [IsAffine X] [Algebra R ↑(X.presheaf.obj (Opposite.op ⊤))] (hf : algebraMap R ↑(X.presheaf.obj (Opposite.op ⊤)) = CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (ΓSpecIso ↧R).inv (appTop f))) (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (Spec ↧R)) ⟶ CategoryTheory.Over.mk f) (c : ↑(X.presheaf.obj (Opposite.op ⊤))) : ((pointsEquivAlgHom f hf) x) c = (CategoryTheory.ConcreteCategory.hom (ΓSpecIso ↧R).hom) ((CategoryTheory.ConcreteCategory.hom (appTop (CategoryTheory.Over.Hom.left x))) c)

The character attached to a point x of X over Spec R pulls back functions along x.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.pointsEquivAlgHom_symm_apply_left {R : Type u} [CommRing R] {X : Scheme} (f : X ⟶ Spec ↧R) [IsAffine X] [Algebra R ↑(X.presheaf.obj (Opposite.op ⊤))] (hf : algebraMap R ↑(X.presheaf.obj (Opposite.op ⊤)) = CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (ΓSpecIso ↧R).inv (appTop f))) (φ : ↑(X.presheaf.obj (Opposite.op ⊤)) →ₐ[R] R) : CategoryTheory.Over.Hom.left ((pointsEquivAlgHom f hf).symm φ) = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom ↑φ)) X.isoSpec.inv

The point attached to a character φ of Γ(X, ⊤) is Spec φ, read through X ≅ Spec Γ(X, ⊤).