noncomputable def Prop17.absolute : AlgebraicGeometry.AffineScheme ≌ CommRingCatᵒᵖ

The "absolute" anti-equivalence between affine schemes and commutative rings: AffineScheme ≌ CommRingᵒᵖ via Spec. (Thm 2.1.)

noncomputable def Prop17.underlyingModule (Y : AlgebraicGeometry.Scheme) (A : TopCat.Sheaf CommRingCat ↑Y.toPresheafedSpace) (α : Y.sheaf ⟶ A) : Y.Modules

The O_Y-module underlying an O_Y-algebra A (with structure map α : O_Y → A), obtained by restriction of scalars from the natural A-module structure on A.

structure Prop17.QCohAlg (Y : AlgebraicGeometry.Scheme) : Type (u + 1)

A quasi-coherent O_Y-algebra: a sheaf of commutative rings on Y, together with a structure map from O_Y, whose underlying O_Y-module is quasi-coherent.

• sheaf : TopCat.Sheaf CommRingCat ↑Y.toPresheafedSpace
• algebraMap : Y.sheaf ⟶ self.sheaf
• isQCoh : SheafOfModules.IsQuasicoherent (underlyingModule Y self.sheaf self.algebraMap)

structure Prop17.QCohAlg.Hom {Y : AlgebraicGeometry.Scheme} (A B : QCohAlg Y) : Type u

A morphism of quasi-coherent O_Y-algebras: a map of sheaves of rings commuting with the structure maps from O_Y.

• ringHom : A.sheaf ⟶ B.sheaf
• algebraMap_comp : CategoryTheory.CategoryStruct.comp A.algebraMap self.ringHom = B.algebraMap

theorem Prop17.QCohAlg.Hom.ext {Y : AlgebraicGeometry.Scheme} {A B : QCohAlg Y} {x y : A.Hom B} (ringHom : x.ringHom = y.ringHom) : x = y

theorem Prop17.QCohAlg.Hom.ext_iff {Y : AlgebraicGeometry.Scheme} {A B : QCohAlg Y} {x y : A.Hom B} : x = y ↔ x.ringHom = y.ringHom

@[implicit_reducible]

noncomputable instance Prop17.instCategoryQCohAlg (Y : AlgebraicGeometry.Scheme) : CategoryTheory.Category.{u, u + 1} (QCohAlg Y)

Category structure on quasi-coherent O_Y-algebras.

@[reducible, inline]

abbrev Prop17.AffineSchemeOver (Y : AlgebraicGeometry.Scheme) : Type (u + 1)

The category of affine schemes over Y: schemes equipped with an affine morphism to Y (Def 9, Lec 2).

noncomputable def Prop17.affine_antiequiv (Y : AlgebraicGeometry.Scheme) : AffineSchemeOver Y ≌ (QCohAlg Y)ᵒᵖ

Proposition 17 (relative Spec): the category of affine Y-schemes is anti-equivalent to the category of quasi-coherent O_Y-algebras, via X ↦ f_* O_X.