The category of schemes

A scheme is a locally ringed space such that every point is contained in some open set where there is an isomorphism of presheaves between the restriction to that open set, and the structure sheaf of Spec R, for some commutative ring R.

A morphism of schemes is just a morphism of the underlying locally ringed spaces.

structure AlgebraicGeometry.Schemeextends AlgebraicGeometry.LocallyRingedSpace : Type (u_1 + 1)

• carrier : TopCat
• presheaf : TopCat.Presheaf CommRingCat ↑s.toPresheafedSpace
• IsSheaf : TopCat.Presheaf.IsSheaf s.presheaf
• localRing : ∀ (x : ↑↑s.toPresheafedSpace), LocalRing ↑(TopCat.Presheaf.stalk s.presheaf x)
• local_affine : ∀ (x : ↑(AlgebraicGeometry.LocallyRingedSpace.toTopCat s.toLocallyRingedSpace)), ∃ U R, Nonempty (AlgebraicGeometry.LocallyRingedSpace.restrict s.toLocallyRingedSpace (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion U.obj)) ≅ AlgebraicGeometry.Spec.toLocallyRingedSpace.obj (Opposite.op R))

We define Scheme as an X : LocallyRingedSpace, along with a proof that every point has an open neighbourhood U so that that the restriction of X to U is isomorphic, as a locally ringed space, to Spec.toLocallyRingedSpace.obj (op R) for some R : CommRingCat.

def AlgebraicGeometry.Scheme.Hom (X : AlgebraicGeometry.Scheme) (Y : AlgebraicGeometry.Scheme) : Type u_1

A morphism between schemes is a morphism between the underlying locally ringed spaces.

instance AlgebraicGeometry.Scheme.instCategoryScheme : CategoryTheory.Category.{u_1, u_1 + 1} AlgebraicGeometry.Scheme

Schemes are a full subcategory of locally ringed spaces.

theorem AlgebraicGeometry.Scheme.Hom.continuous {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : Continuous ↑f.val.base

@[inline, reducible]

abbrev AlgebraicGeometry.Scheme.sheaf (X : AlgebraicGeometry.Scheme) : TopCat.Sheaf CommRingCat ↑X.toPresheafedSpace

The structure sheaf of a scheme.

instance AlgebraicGeometry.Scheme.instCoeSortSchemeType : CoeSort AlgebraicGeometry.Scheme (Type u_1)

@[simp]

theorem AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace_obj (self : AlgebraicGeometry.Scheme) : AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace.obj self = self.toLocallyRingedSpace

@[simp]

theorem AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace_map : ∀ {X Y : CategoryTheory.InducedCategory AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace} (f : X ⟶ Y), AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace.map f = f

def AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace : CategoryTheory.Functor AlgebraicGeometry.Scheme AlgebraicGeometry.LocallyRingedSpace

The forgetful functor from Scheme to LocallyRingedSpace.

instance AlgebraicGeometry.Scheme.instFullSchemeInstCategorySchemeLocallyRingedSpaceInstCategoryLocallyRingedSpaceForgetToLocallyRingedSpace : CategoryTheory.Full AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace

instance AlgebraicGeometry.Scheme.instFaithfulSchemeInstCategorySchemeLocallyRingedSpaceInstCategoryLocallyRingedSpaceForgetToLocallyRingedSpace : CategoryTheory.Faithful AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace

@[simp]

theorem AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace_preimage {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace.preimage f = f

@[simp]

theorem AlgebraicGeometry.Scheme.forgetToTop_map : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), AlgebraicGeometry.Scheme.forgetToTop.map f = (AlgebraicGeometry.SheafedSpace.forget CommRingCat).map f.val

@[simp]

theorem AlgebraicGeometry.Scheme.forgetToTop_obj (X : AlgebraicGeometry.Scheme) : AlgebraicGeometry.Scheme.forgetToTop.obj X = (AlgebraicGeometry.SheafedSpace.forget CommRingCat).obj X.toSheafedSpace

def AlgebraicGeometry.Scheme.forgetToTop : CategoryTheory.Functor AlgebraicGeometry.Scheme TopCat

The forgetful functor from Scheme to TopCat.

instance AlgebraicGeometry.Scheme.hasCoeToTopCat : CoeOut AlgebraicGeometry.Scheme TopCat

def AlgebraicGeometry.Scheme.forgetToTop_obj_eq_coe (X : AlgebraicGeometry.Scheme) : Prop

forgetful functor to TopCat is the same as coercion

@[simp]

theorem AlgebraicGeometry.Scheme.id_val_base (X : AlgebraicGeometry.Scheme) : (CategoryTheory.CategoryStruct.id X).val.base = CategoryTheory.CategoryStruct.id ↑X.toPresheafedSpace

@[simp]

theorem AlgebraicGeometry.Scheme.id_app {X : AlgebraicGeometry.Scheme} (U : (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)ᵒᵖ) : (CategoryTheory.CategoryStruct.id X).val.c.app U = X.presheaf.map (CategoryTheory.eqToHom (_ : U = U))

theorem AlgebraicGeometry.Scheme.comp_val_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) {Z : AlgebraicGeometry.SheafedSpace CommRingCat} (h : Z.toSheafedSpace ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).val h = CategoryTheory.CategoryStruct.comp f.val (CategoryTheory.CategoryStruct.comp g.val h)

theorem AlgebraicGeometry.Scheme.comp_val {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).val = CategoryTheory.CategoryStruct.comp f.val g.val

theorem AlgebraicGeometry.Scheme.comp_coeBase_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) {Z : TopCat} (h : ↑Z.toPresheafedSpace ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).val.base h = CategoryTheory.CategoryStruct.comp f.val.base (CategoryTheory.CategoryStruct.comp g.val.base h)

@[simp]

theorem AlgebraicGeometry.Scheme.comp_coeBase {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).val.base = CategoryTheory.CategoryStruct.comp f.val.base g.val.base

theorem AlgebraicGeometry.Scheme.comp_val_base_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) {Z : TopCat} (h : ↑Z.toPresheafedSpace ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).val.base h = CategoryTheory.CategoryStruct.comp f.val.base (CategoryTheory.CategoryStruct.comp g.val.base h)

theorem AlgebraicGeometry.Scheme.comp_val_base {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).val.base = CategoryTheory.CategoryStruct.comp f.val.base g.val.base

theorem AlgebraicGeometry.Scheme.comp_val_base_apply {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑↑X.toPresheafedSpace) : ↑(CategoryTheory.CategoryStruct.comp f g).val.base x = ↑g.val.base (↑f.val.base x)

theorem AlgebraicGeometry.Scheme.comp_val_c_app_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : (TopologicalSpace.Opens ↑↑Z.toPresheafedSpace)ᵒᵖ) {Z : CommRingCat} (h : ((CategoryTheory.CategoryStruct.comp f g).val.base _* X.presheaf).obj U ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp f g).val.c.app U) h = CategoryTheory.CategoryStruct.comp (g.val.c.app U) (CategoryTheory.CategoryStruct.comp (f.val.c.app ((TopologicalSpace.Opens.map g.val.base).op.obj U)) h)

@[simp]

theorem AlgebraicGeometry.Scheme.comp_val_c_app {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : (TopologicalSpace.Opens ↑↑Z.toPresheafedSpace)ᵒᵖ) : (CategoryTheory.CategoryStruct.comp f g).val.c.app U = CategoryTheory.CategoryStruct.comp (g.val.c.app U) (f.val.c.app ((TopologicalSpace.Opens.map g.val.base).op.obj U))

theorem AlgebraicGeometry.Scheme.congr_app {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {g : X ⟶ Y} (e : f = g) (U : (TopologicalSpace.Opens ↑↑Y.toPresheafedSpace)ᵒᵖ) : f.val.c.app U = CategoryTheory.CategoryStruct.comp (g.val.c.app U) (X.presheaf.map (CategoryTheory.eqToHom (_ : (TopologicalSpace.Opens.map g.val.base).op.obj U = (TopologicalSpace.Opens.map f.val.base).op.obj U)))

theorem AlgebraicGeometry.Scheme.app_eq {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace} {V : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace} (e : U = V) : f.val.c.app (Opposite.op U) = CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.eqToHom (_ : V = U)).op) (CategoryTheory.CategoryStruct.comp (f.val.c.app (Opposite.op V)) (X.presheaf.map (CategoryTheory.eqToHom (_ : (TopologicalSpace.Opens.map f.val.base).obj U = (TopologicalSpace.Opens.map f.val.base).obj V)).op))

theorem AlgebraicGeometry.Scheme.presheaf_map_eqToHom_op (X : AlgebraicGeometry.Scheme) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (i : U = V) : X.presheaf.map (CategoryTheory.eqToHom i).op = CategoryTheory.eqToHom (_ : X.presheaf.obj (Opposite.op V) = X.presheaf.obj (Opposite.op U))

instance AlgebraicGeometry.Scheme.is_locallyRingedSpace_iso {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] : CategoryTheory.IsIso f

instance AlgebraicGeometry.Scheme.instIsIsoCommRingCatInstCommRingCatLargeCategoryObjOppositeOpensαTopologicalSpaceCarrierToPresheafedSpaceToSheafedSpaceToLocallyRingedSpaceTopologicalSpace_coeToQuiverToCategoryStructOppositeSmallCategoryToPreorderToPartialOrderToCompleteSemilatticeInfInstCompleteLatticeOpensToQuiverToCategoryStructToPrefunctorPresheafPushforwardObjBaseValAppC {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] (U : (TopologicalSpace.Opens ↑↑Y.toPresheafedSpace)ᵒᵖ) : CategoryTheory.IsIso (f.val.c.app U)

@[simp]

theorem AlgebraicGeometry.Scheme.inv_val_c_app {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : (CategoryTheory.inv f).val.c.app (Opposite.op U) = CategoryTheory.CategoryStruct.comp (X.presheaf.map (CategoryTheory.eqToHom (_ : (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv f)).val.base).obj U = U)).op) (CategoryTheory.inv (f.val.c.app (Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.inv f).val.base).obj U))))

@[inline, reducible]

abbrev AlgebraicGeometry.Scheme.Hom.appLe {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace} (e : V ≤ (TopologicalSpace.Opens.map f.val.base).obj U) : Y.presheaf.obj (Opposite.op U) ⟶ X.presheaf.obj (Opposite.op V)

Given a morphism of schemes f : X ⟶ Y, and open sets U ⊆ Y, V ⊆ f ⁻¹' U, this is the induced map Γ(Y, U) ⟶ Γ(X, V).

def AlgebraicGeometry.Scheme.specObj (R : CommRingCat) : AlgebraicGeometry.Scheme

The spectrum of a commutative ring, as a scheme.

@[simp]

theorem AlgebraicGeometry.Scheme.specObj_toLocallyRingedSpace (R : CommRingCat) : (AlgebraicGeometry.Scheme.specObj R).toLocallyRingedSpace = AlgebraicGeometry.Spec.locallyRingedSpaceObj R

def AlgebraicGeometry.Scheme.specMap {R : CommRingCat} {S : CommRingCat} (f : R ⟶ S) : AlgebraicGeometry.Scheme.specObj S ⟶ AlgebraicGeometry.Scheme.specObj R

The induced map of a ring homomorphism on the ring spectra, as a morphism of schemes.

@[simp]

theorem AlgebraicGeometry.Scheme.specMap_id (R : CommRingCat) : AlgebraicGeometry.Scheme.specMap (CategoryTheory.CategoryStruct.id R) = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Scheme.specObj R)

theorem AlgebraicGeometry.Scheme.specMap_comp {R : CommRingCat} {S : CommRingCat} {T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) : AlgebraicGeometry.Scheme.specMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.specMap g) (AlgebraicGeometry.Scheme.specMap f)

def AlgebraicGeometry.Scheme.Spec : CategoryTheory.Functor CommRingCatᵒᵖ AlgebraicGeometry.Scheme

The spectrum, as a contravariant functor from commutative rings to schemes.

@[simp]

theorem AlgebraicGeometry.Scheme.empty_presheaf : AlgebraicGeometry.Scheme.empty.presheaf = (CategoryTheory.Functor.const (TopologicalSpace.Opens ↑(TopCat.of PEmpty.{u + 1} ))ᵒᵖ).obj (CommRingCat.of PUnit.{u + 1} )

@[simp]

theorem AlgebraicGeometry.Scheme.empty_carrier : ↑AlgebraicGeometry.Scheme.empty.toPresheafedSpace = TopCat.of PEmpty.{u + 1}

def AlgebraicGeometry.Scheme.empty : AlgebraicGeometry.Scheme

The empty scheme.

instance AlgebraicGeometry.Scheme.instEmptyCollectionScheme : EmptyCollection AlgebraicGeometry.Scheme

instance AlgebraicGeometry.Scheme.instInhabitedScheme : Inhabited AlgebraicGeometry.Scheme

def AlgebraicGeometry.Scheme.Γ : CategoryTheory.Functor AlgebraicGeometry.Schemeᵒᵖ CommRingCat

The global sections, notated Gamma.

theorem AlgebraicGeometry.Scheme.Γ_def : AlgebraicGeometry.Scheme.Γ = CategoryTheory.Functor.comp (CategoryTheory.inducedFunctor AlgebraicGeometry.Scheme.toLocallyRingedSpace).op AlgebraicGeometry.LocallyRingedSpace.Γ

@[simp]

theorem AlgebraicGeometry.Scheme.Γ_obj (X : AlgebraicGeometry.Schemeᵒᵖ) : AlgebraicGeometry.Scheme.Γ.obj X = X.unop.presheaf.obj (Opposite.op ⊤)

theorem AlgebraicGeometry.Scheme.Γ_obj_op (X : AlgebraicGeometry.Scheme) : AlgebraicGeometry.Scheme.Γ.obj (Opposite.op X) = X.presheaf.obj (Opposite.op ⊤)

@[simp]

theorem AlgebraicGeometry.Scheme.Γ_map {X : AlgebraicGeometry.Schemeᵒᵖ} {Y : AlgebraicGeometry.Schemeᵒᵖ} (f : X ⟶ Y) : AlgebraicGeometry.Scheme.Γ.map f = f.unop.val.c.app (Opposite.op ⊤)

theorem AlgebraicGeometry.Scheme.Γ_map_op {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : AlgebraicGeometry.Scheme.Γ.map f.op = f.val.c.app (Opposite.op ⊤)

def AlgebraicGeometry.Scheme.basicOpen (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (f : ↑(X.presheaf.obj (Opposite.op U))) : TopologicalSpace.Opens ↑↑X.toPresheafedSpace

The subset of the underlying space where the given section does not vanish.

@[simp]

theorem AlgebraicGeometry.Scheme.mem_basicOpen (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (f : ↑(X.presheaf.obj (Opposite.op U))) (x : { x // x ∈ U }) : ↑x ∈ AlgebraicGeometry.Scheme.basicOpen X f ↔ IsUnit (↑(TopCat.Presheaf.germ X.presheaf x) f)

theorem AlgebraicGeometry.Scheme.mem_basicOpen_top' (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (f : ↑(X.presheaf.obj (Opposite.op U))) (x : ↑↑X.toPresheafedSpace) : x ∈ AlgebraicGeometry.Scheme.basicOpen X f ↔ ∃ m, IsUnit (↑(TopCat.Presheaf.germ X.presheaf { val := x, property := m }) f)

@[simp]

theorem AlgebraicGeometry.Scheme.mem_basicOpen_top (X : AlgebraicGeometry.Scheme) (f : ↑(X.presheaf.obj (Opposite.op ⊤))) (x : ↑↑X.toPresheafedSpace) : x ∈ AlgebraicGeometry.Scheme.basicOpen X f ↔ IsUnit (↑(TopCat.Presheaf.germ X.presheaf { val := x, property := trivial }) f)

@[simp]

theorem AlgebraicGeometry.Scheme.basicOpen_res (X : AlgebraicGeometry.Scheme) {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (f : ↑(X.presheaf.obj (Opposite.op U))) (i : Opposite.op U ⟶ Opposite.op V) : AlgebraicGeometry.Scheme.basicOpen X (↑(X.presheaf.map i) f) = V ⊓ AlgebraicGeometry.Scheme.basicOpen X f

@[simp]

theorem AlgebraicGeometry.Scheme.basicOpen_res_eq (X : AlgebraicGeometry.Scheme) {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (f : ↑(X.presheaf.obj (Opposite.op U))) (i : Opposite.op U ⟶ Opposite.op V) [CategoryTheory.IsIso i] : AlgebraicGeometry.Scheme.basicOpen X (↑(X.presheaf.map i) f) = AlgebraicGeometry.Scheme.basicOpen X f

theorem AlgebraicGeometry.Scheme.basicOpen_le (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (f : ↑(X.presheaf.obj (Opposite.op U))) : AlgebraicGeometry.Scheme.basicOpen X f ≤ U

@[simp]

theorem AlgebraicGeometry.Scheme.preimage_basicOpen {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace} (r : ↑(Y.presheaf.obj (Opposite.op U))) : (TopologicalSpace.Opens.map f.val.base).obj (AlgebraicGeometry.Scheme.basicOpen Y r) = AlgebraicGeometry.Scheme.basicOpen X (↑(f.val.c.app (Opposite.op U)) r)

@[simp]

theorem AlgebraicGeometry.Scheme.basicOpen_zero (X : AlgebraicGeometry.Scheme) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : AlgebraicGeometry.Scheme.basicOpen X 0 = ⊥

@[simp]

theorem AlgebraicGeometry.Scheme.basicOpen_mul (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (f : ↑(X.presheaf.obj (Opposite.op U))) (g : ↑(X.presheaf.obj (Opposite.op U))) : AlgebraicGeometry.Scheme.basicOpen X (f * g) = AlgebraicGeometry.Scheme.basicOpen X f ⊓ AlgebraicGeometry.Scheme.basicOpen X g

theorem AlgebraicGeometry.Scheme.basicOpen_of_isUnit (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {f : ↑(X.presheaf.obj (Opposite.op U))} (hf : IsUnit f) : AlgebraicGeometry.Scheme.basicOpen X f = U

theorem AlgebraicGeometry.basicOpen_eq_of_affine {R : CommRingCat} (f : ↑R) : AlgebraicGeometry.Scheme.basicOpen (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op R)) (↑(AlgebraicGeometry.SpecΓIdentity.app R).inv f) = PrimeSpectrum.basicOpen f

@[simp]

theorem AlgebraicGeometry.basicOpen_eq_of_affine' {R : CommRingCat} (f : ↑((AlgebraicGeometry.Spec.toSheafedSpace.obj (Opposite.op R)).presheaf.obj (Opposite.op ⊤))) : AlgebraicGeometry.Scheme.basicOpen (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op R)) f = PrimeSpectrum.basicOpen (↑(AlgebraicGeometry.SpecΓIdentity.app R).hom f)