Affine schemes

We define the category of AffineSchemes as the essential image of Spec. We also define predicates about affine schemes and affine open sets.

Main definitions

• AlgebraicGeometry.AffineScheme: The category of affine schemes.
• AlgebraicGeometry.IsAffine: A scheme is affine if the canonical map X ⟶ Spec Γ(X) is an isomorphism.
• AlgebraicGeometry.Scheme.isoSpec: The canonical isomorphism X ≅ Spec Γ(X) for an affine scheme.
• AlgebraicGeometry.AffineScheme.equivCommRingCat: The equivalence of categories AffineScheme ≌ CommRingᵒᵖ given by AffineScheme.Spec : CommRingᵒᵖ ⥤ AffineScheme and AffineScheme.Γ : AffineSchemeᵒᵖ ⥤ CommRingCat.
• AlgebraicGeometry.IsAffineOpen: An open subset of a scheme is affine if the open subscheme is affine.
• AlgebraicGeometry.IsAffineOpen.fromSpec: The immersion Spec 𝒪ₓ(U) ⟶ X for an affine U.

def AlgebraicGeometry.AffineScheme : Type (u_1 + 1)

The category of affine schemes

class AlgebraicGeometry.IsAffine (X : AlgebraicGeometry.Scheme) : Prop

• affine : CategoryTheory.IsIso (AlgebraicGeometry.ΓSpec.adjunction.unit.app X)

A Scheme is affine if the canonical map X ⟶ Spec Γ(X) is an isomorphism.

def AlgebraicGeometry.Scheme.isoSpec (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] : X ≅ AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op X)))

The canonical isomorphism X ≅ Spec Γ(X) for an affine scheme.

@[simp]

theorem AlgebraicGeometry.AffineScheme.mk_obj (X : AlgebraicGeometry.Scheme) (h : AlgebraicGeometry.IsAffine X) : (AlgebraicGeometry.AffineScheme.mk X h).obj = X

def AlgebraicGeometry.AffineScheme.mk (X : AlgebraicGeometry.Scheme) (h : AlgebraicGeometry.IsAffine X) : AlgebraicGeometry.AffineScheme

Construct an affine scheme from a scheme and the information that it is affine. Also see AffineScheme.of for a typeclass version.

def AlgebraicGeometry.AffineScheme.of (X : AlgebraicGeometry.Scheme) [h : AlgebraicGeometry.IsAffine X] : AlgebraicGeometry.AffineScheme

Construct an affine scheme from a scheme. Also see AffineScheme.mk for a non-typeclass version.

def AlgebraicGeometry.AffineScheme.ofHom {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) : AlgebraicGeometry.AffineScheme.of X ⟶ AlgebraicGeometry.AffineScheme.of Y

Type check a morphism of schemes as a morphism in AffineScheme.

theorem AlgebraicGeometry.mem_Spec_essImage (X : AlgebraicGeometry.Scheme) : X ∈ CategoryTheory.Functor.essImage AlgebraicGeometry.Scheme.Spec ↔ AlgebraicGeometry.IsAffine X

instance AlgebraicGeometry.isAffineAffineScheme (X : AlgebraicGeometry.AffineScheme) : AlgebraicGeometry.IsAffine X.obj

instance AlgebraicGeometry.SpecIsAffine (R : CommRingCatᵒᵖ) : AlgebraicGeometry.IsAffine (AlgebraicGeometry.Scheme.Spec.obj R)

theorem AlgebraicGeometry.isAffineOfIso {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] [h : AlgebraicGeometry.IsAffine Y] : AlgebraicGeometry.IsAffine X

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

The Spec functor into the category of affine schemes.

instance AlgebraicGeometry.AffineScheme.Spec_full : CategoryTheory.Full AlgebraicGeometry.AffineScheme.Spec

instance AlgebraicGeometry.AffineScheme.Spec_faithful : CategoryTheory.Faithful AlgebraicGeometry.AffineScheme.Spec

instance AlgebraicGeometry.AffineScheme.Spec_essSurj : CategoryTheory.EssSurj AlgebraicGeometry.AffineScheme.Spec

@[simp]

theorem AlgebraicGeometry.AffineScheme.forgetToScheme_map : ∀ {X Y : CategoryTheory.InducedCategory AlgebraicGeometry.Scheme CategoryTheory.FullSubcategory.obj} (f : X ⟶ Y), AlgebraicGeometry.AffineScheme.forgetToScheme.map f = f

@[simp]

theorem AlgebraicGeometry.AffineScheme.forgetToScheme_obj (self : CategoryTheory.FullSubcategory (CategoryTheory.Functor.essImage AlgebraicGeometry.Scheme.Spec)) : AlgebraicGeometry.AffineScheme.forgetToScheme.obj self = self.obj

def AlgebraicGeometry.AffineScheme.forgetToScheme : CategoryTheory.Functor AlgebraicGeometry.AffineScheme AlgebraicGeometry.Scheme

The forgetful functor AffineScheme ⥤ Scheme.

instance AlgebraicGeometry.AffineScheme.forgetToScheme_full : CategoryTheory.Full AlgebraicGeometry.AffineScheme.forgetToScheme

instance AlgebraicGeometry.AffineScheme.forgetToScheme_faithful : CategoryTheory.Faithful AlgebraicGeometry.AffineScheme.forgetToScheme

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

The global section functor of an affine scheme.

def AlgebraicGeometry.AffineScheme.equivCommRingCat : AlgebraicGeometry.AffineScheme ≌ CommRingCatᵒᵖ

The category of affine schemes is equivalent to the category of commutative rings.

instance AlgebraicGeometry.AffineScheme.ΓIsEquiv : CategoryTheory.IsEquivalence AlgebraicGeometry.AffineScheme.Γ

instance AlgebraicGeometry.AffineScheme.hasColimits : CategoryTheory.Limits.HasColimits AlgebraicGeometry.AffineScheme

instance AlgebraicGeometry.AffineScheme.hasLimits : CategoryTheory.Limits.HasLimits AlgebraicGeometry.AffineScheme

noncomputable instance AlgebraicGeometry.AffineScheme.Γ_preservesLimits : CategoryTheory.Limits.PreservesLimits AlgebraicGeometry.AffineScheme.Γ.rightOp

noncomputable instance AlgebraicGeometry.AffineScheme.forgetToScheme_preservesLimits : CategoryTheory.Limits.PreservesLimits AlgebraicGeometry.AffineScheme.forgetToScheme

def AlgebraicGeometry.IsAffineOpen {X : AlgebraicGeometry.Scheme} (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : Prop

An open subset of a scheme is affine if the open subscheme is affine.

def AlgebraicGeometry.Scheme.affineOpens (X : AlgebraicGeometry.Scheme) : Set (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)

The set of affine opens as a subset of opens X.

theorem AlgebraicGeometry.rangeIsAffineOpenOfOpenImmersion {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] : AlgebraicGeometry.IsAffineOpen (AlgebraicGeometry.Scheme.Hom.opensRange f)

theorem AlgebraicGeometry.topIsAffineOpen (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] : AlgebraicGeometry.IsAffineOpen ⊤

instance AlgebraicGeometry.Scheme.affineCoverIsAffine (X : AlgebraicGeometry.Scheme) (i : (AlgebraicGeometry.Scheme.affineCover X).J) : AlgebraicGeometry.IsAffine (AlgebraicGeometry.Scheme.OpenCover.obj (AlgebraicGeometry.Scheme.affineCover X) i)

instance AlgebraicGeometry.Scheme.affineBasisCoverIsAffine (X : AlgebraicGeometry.Scheme) (i : (AlgebraicGeometry.Scheme.affineBasisCover X).J) : AlgebraicGeometry.IsAffine (AlgebraicGeometry.Scheme.OpenCover.obj (AlgebraicGeometry.Scheme.affineBasisCover X) i)

theorem AlgebraicGeometry.isBasis_affine_open (X : AlgebraicGeometry.Scheme) : TopologicalSpace.Opens.IsBasis (AlgebraicGeometry.Scheme.affineOpens X)

def AlgebraicGeometry.IsAffineOpen.fromSpec {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) : AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj (Opposite.op U))) ⟶ X

The open immersion Spec 𝒪ₓ(U) ⟶ X for an affine U.

instance AlgebraicGeometry.IsAffineOpen.isOpenImmersion_fromSpec {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) : AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.IsAffineOpen.fromSpec hU)

theorem AlgebraicGeometry.IsAffineOpen.fromSpec_range {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) : Set.range ↑(AlgebraicGeometry.IsAffineOpen.fromSpec hU).val.base = ↑U

theorem AlgebraicGeometry.IsAffineOpen.fromSpec_image_top {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) : (IsOpenMap.functor (_ : IsOpenMap ↑(AlgebraicGeometry.IsAffineOpen.fromSpec hU).val.base)).obj ⊤ = U

theorem AlgebraicGeometry.IsAffineOpen.isCompact {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) : IsCompact ↑U

theorem AlgebraicGeometry.IsAffineOpen.imageIsOpenImmersion {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] : AlgebraicGeometry.IsAffineOpen ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U)

theorem AlgebraicGeometry.isAffineOpen_iff_of_isOpenImmersion {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : AlgebraicGeometry.IsAffineOpen ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.openFunctor H).obj U) ↔ AlgebraicGeometry.IsAffineOpen U

instance AlgebraicGeometry.Scheme.quasi_compact_of_affine (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] : CompactSpace ↑↑X.toPresheafedSpace

theorem AlgebraicGeometry.IsAffineOpen.fromSpec_base_preimage {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) : (TopologicalSpace.Opens.map (AlgebraicGeometry.IsAffineOpen.fromSpec hU).val.base).obj U = ⊤

theorem AlgebraicGeometry.Scheme.Spec_map_presheaf_map_eqToHom {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (h : U = V) (W : (TopologicalSpace.Opens ↑↑(AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj (Opposite.op V)))).toPresheafedSpace)ᵒᵖ) : (AlgebraicGeometry.Scheme.Spec.map (X.presheaf.map (CategoryTheory.eqToHom h).op).op).val.c.app W = CategoryTheory.eqToHom (_ : (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj (Opposite.op V)))).presheaf.obj W = ((AlgebraicGeometry.Scheme.Spec.map (X.presheaf.map (CategoryTheory.eqToHom h).op).op).val.base _* (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj (Opposite.op U)))).presheaf).obj W)

theorem AlgebraicGeometry.IsAffineOpen.SpecΓIdentity_hom_app_fromSpec {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.SpecΓIdentity.hom.app (X.presheaf.obj (Opposite.op U))) ((AlgebraicGeometry.IsAffineOpen.fromSpec hU).val.c.app (Opposite.op U)) = (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj (Opposite.op U)))).presheaf.map (CategoryTheory.eqToHom (_ : (TopologicalSpace.Opens.map (AlgebraicGeometry.IsAffineOpen.fromSpec hU).val.base).obj U = ⊤)).op

theorem AlgebraicGeometry.IsAffineOpen.fromSpec_app_eq_apply {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (x : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (Opposite.op U))) : ↑((AlgebraicGeometry.IsAffineOpen.fromSpec hU).val.c.app (Opposite.op U)) x = ↑((AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj (Opposite.op U)))).presheaf.map (CategoryTheory.eqToHom (_ : Opposite.op ⊤ = Opposite.op ((TopologicalSpace.Opens.map (AlgebraicGeometry.IsAffineOpen.fromSpec hU).val.base).obj U)))) (↑(AlgebraicGeometry.toSpecΓ (X.presheaf.obj (Opposite.op U))) x)

theorem AlgebraicGeometry.IsAffineOpen.fromSpec_app_eq {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) : (AlgebraicGeometry.IsAffineOpen.fromSpec hU).val.c.app (Opposite.op U) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.SpecΓIdentity.inv.app (X.presheaf.obj (Opposite.op U))) ((AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj (Opposite.op U)))).presheaf.map (CategoryTheory.eqToHom (_ : (TopologicalSpace.Opens.map (AlgebraicGeometry.IsAffineOpen.fromSpec hU).val.base).obj U = ⊤)).op)

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

theorem AlgebraicGeometry.IsAffineOpen.mapRestrictBasicOpen {X : AlgebraicGeometry.Scheme} (r : ↑(X.presheaf.obj (Opposite.op ⊤))) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) : AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map (AlgebraicGeometry.Scheme.ofRestrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion (AlgebraicGeometry.Scheme.basicOpen X r)))).val.base).obj U)

theorem AlgebraicGeometry.Scheme.map_PrimeSpectrum_basicOpen_of_affine (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] (f : ↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op X))) : (TopologicalSpace.Opens.map (AlgebraicGeometry.Scheme.isoSpec X).hom.val.base).obj (PrimeSpectrum.basicOpen f) = AlgebraicGeometry.Scheme.basicOpen X f

theorem AlgebraicGeometry.isBasis_basicOpen (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] : TopologicalSpace.Opens.IsBasis (Set.range (AlgebraicGeometry.Scheme.basicOpen X))

theorem AlgebraicGeometry.IsAffineOpen.exists_basicOpen_le {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (x : { x // x ∈ V }) (h : ↑x ∈ U) : ∃ f, AlgebraicGeometry.Scheme.basicOpen X f ≤ V ∧ ↑x ∈ AlgebraicGeometry.Scheme.basicOpen X f

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

theorem AlgebraicGeometry.IsAffineOpen.opens_map_fromSpec_basicOpen {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : ↑(X.presheaf.obj (Opposite.op U))) : (TopologicalSpace.Opens.map (AlgebraicGeometry.IsAffineOpen.fromSpec hU).val.base).obj (AlgebraicGeometry.Scheme.basicOpen X f) = AlgebraicGeometry.RingedSpace.basicOpen (AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace.op.obj (AlgebraicGeometry.Spec.toLocallyRingedSpace.rightOp.obj (X.presheaf.obj (Opposite.op U)))).unop (↑(AlgebraicGeometry.SpecΓIdentity.inv.app (X.presheaf.obj (Opposite.op U))) f)

def AlgebraicGeometry.basicOpenSectionsToAffine {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : ↑(X.presheaf.obj (Opposite.op U))) : X.presheaf.obj (Opposite.op (AlgebraicGeometry.Scheme.basicOpen X f)) ⟶ (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj (Opposite.op U)))).presheaf.obj (Opposite.op (AlgebraicGeometry.Scheme.basicOpen (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj (Opposite.op U)))) (↑(AlgebraicGeometry.SpecΓIdentity.inv.app (X.presheaf.obj (Opposite.op U))) f)))

The canonical map Γ(𝒪ₓ, D(f)) ⟶ Γ(Spec 𝒪ₓ(U), D(Spec_Γ_identity.inv f)) This is an isomorphism, as witnessed by an is_iso instance.

instance AlgebraicGeometry.basicOpenSectionsToAffine_isIso {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : ↑(X.presheaf.obj (Opposite.op U))) : CategoryTheory.IsIso (AlgebraicGeometry.basicOpenSectionsToAffine hU f)

theorem AlgebraicGeometry.isLocalization_basicOpen {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : ↑(X.presheaf.obj (Opposite.op U))) : IsLocalization.Away f ↑(X.presheaf.obj (Opposite.op (AlgebraicGeometry.Scheme.basicOpen X f)))

instance AlgebraicGeometry.isLocalization_away_of_isAffine {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] (r : ↑(X.presheaf.obj (Opposite.op ⊤))) : IsLocalization.Away r ↑(X.presheaf.obj (Opposite.op (AlgebraicGeometry.Scheme.basicOpen X r)))

theorem AlgebraicGeometry.isLocalization_of_eq_basicOpen {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (i : V ⟶ U) (hU : AlgebraicGeometry.IsAffineOpen U) (r : ↑(X.presheaf.obj (Opposite.op U))) (e : V = AlgebraicGeometry.Scheme.basicOpen X r) : IsLocalization.Away r ↑(X.presheaf.obj (Opposite.op V))

instance AlgebraicGeometry.ΓRestrictAlgebra {X : AlgebraicGeometry.Scheme} {Y : TopCat} {f : Y ⟶ ↑X.toPresheafedSpace} (hf : OpenEmbedding ↑f) : Algebra ↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op X)) ↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.restrict X hf)))

instance AlgebraicGeometry.Γ_restrict_isLocalization (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] (r : ↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op X))) : IsLocalization.Away r ↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op (AlgebraicGeometry.Scheme.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion (AlgebraicGeometry.Scheme.basicOpen X r))))))

theorem AlgebraicGeometry.basicOpen_basicOpen_is_basicOpen {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : ↑(X.presheaf.obj (Opposite.op U))) (g : ↑(X.presheaf.obj (Opposite.op (AlgebraicGeometry.Scheme.basicOpen X f)))) : ∃ f', AlgebraicGeometry.Scheme.basicOpen X f' = AlgebraicGeometry.Scheme.basicOpen X g

theorem AlgebraicGeometry.exists_basicOpen_le_affine_inter {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (hV : AlgebraicGeometry.IsAffineOpen V) (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U ⊓ V) : ∃ f g, AlgebraicGeometry.Scheme.basicOpen X f = AlgebraicGeometry.Scheme.basicOpen X g ∧ x ∈ AlgebraicGeometry.Scheme.basicOpen X f

noncomputable def AlgebraicGeometry.IsAffineOpen.primeIdealOf {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (x : { x // x ∈ U }) : PrimeSpectrum ↑(X.presheaf.obj (Opposite.op U))

The prime ideal of 𝒪ₓ(U) corresponding to a point x : U.

theorem AlgebraicGeometry.IsAffineOpen.fromSpec_primeIdealOf {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (x : { x // x ∈ U }) : ↑(AlgebraicGeometry.IsAffineOpen.fromSpec hU).val.base (AlgebraicGeometry.IsAffineOpen.primeIdealOf hU x) = ↑x

theorem AlgebraicGeometry.IsAffineOpen.isLocalization_stalk_aux {X : AlgebraicGeometry.Scheme} (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) [AlgebraicGeometry.IsAffine (AlgebraicGeometry.Scheme.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion U)))] : (CategoryTheory.inv (AlgebraicGeometry.ΓSpec.adjunction.unit.app (AlgebraicGeometry.Scheme.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion U))))).val.c.app (Opposite.op ((TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion U)).obj U)) = CategoryTheory.CategoryStruct.comp (X.presheaf.map (Opposite.op (CategoryTheory.eqToHom (_ : (Opposite.op ((IsOpenMap.functor (_ : IsOpenMap ↑(TopologicalSpace.Opens.inclusion U))).obj ⊤)).unop = ((IsOpenMap.functor (_ : IsOpenMap ↑(TopologicalSpace.Opens.inclusion U))).op.obj (Opposite.op ((TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion U)).obj U))).unop)))) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.toSpecΓ (X.presheaf.obj (Opposite.op ((IsOpenMap.functor (_ : IsOpenMap ↑(TopologicalSpace.Opens.inclusion U))).obj ⊤)))) ((AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj (Opposite.op ((IsOpenMap.functor (_ : IsOpenMap ↑(TopologicalSpace.Opens.inclusion U))).obj ⊤))))).presheaf.map (Opposite.op (CategoryTheory.eqToHom (_ : ((TopologicalSpace.Opens.map (CategoryTheory.inv (AlgebraicGeometry.ΓSpec.adjunction.unit.app (AlgebraicGeometry.Scheme.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion U))))).val.base).op.obj (Opposite.op ((TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion U)).obj U))).unop = (Opposite.op ⊤).unop)))))

theorem AlgebraicGeometry.IsAffineOpen.isLocalization_stalk_aux' {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (y : PrimeSpectrum ↑(X.presheaf.obj (Opposite.op U))) (hy : ↑(AlgebraicGeometry.IsAffineOpen.fromSpec hU).val.base y ∈ U) : CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.IsAffineOpen.fromSpec hU).val.c.app (Opposite.op U)) (TopCat.Presheaf.germ (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj (Opposite.op U)))).presheaf { val := y, property := hy }) = AlgebraicGeometry.StructureSheaf.toStalk (↑(X.presheaf.obj (Opposite.op U))) y

theorem AlgebraicGeometry.IsAffineOpen.isLocalization_stalk' {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (y : PrimeSpectrum ↑(X.presheaf.obj (Opposite.op U))) (hy : ↑(AlgebraicGeometry.IsAffineOpen.fromSpec hU).val.base y ∈ U) : IsLocalization.AtPrime (↑(TopCat.Presheaf.stalk X.presheaf (↑(AlgebraicGeometry.IsAffineOpen.fromSpec hU).val.base y))) y.asIdeal

theorem AlgebraicGeometry.IsAffineOpen.isLocalization_stalk {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (x : { x // x ∈ U }) : IsLocalization.AtPrime (↑(TopCat.Presheaf.stalk X.presheaf ↑x)) (AlgebraicGeometry.IsAffineOpen.primeIdealOf hU x).asIdeal

@[simp]

theorem AlgebraicGeometry.Scheme.affineBasicOpen_coe (X : AlgebraicGeometry.Scheme) {U : ↑(AlgebraicGeometry.Scheme.affineOpens X)} (f : ↑(X.presheaf.obj (Opposite.op ↑U))) : ↑(AlgebraicGeometry.Scheme.affineBasicOpen X f) = AlgebraicGeometry.Scheme.basicOpen X f

def AlgebraicGeometry.Scheme.affineBasicOpen (X : AlgebraicGeometry.Scheme) {U : ↑(AlgebraicGeometry.Scheme.affineOpens X)} (f : ↑(X.presheaf.obj (Opposite.op ↑U))) : ↑(AlgebraicGeometry.Scheme.affineOpens X)

The basic open set of a section f on an affine open as an X.affineOpens.

@[simp]

theorem AlgebraicGeometry.IsAffineOpen.basicOpen_fromSpec_app {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : ↑(X.presheaf.obj (Opposite.op U))) : AlgebraicGeometry.Scheme.basicOpen (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj (Opposite.op U)))) (↑((AlgebraicGeometry.IsAffineOpen.fromSpec hU).val.c.app (Opposite.op U)) f) = PrimeSpectrum.basicOpen f

theorem AlgebraicGeometry.IsAffineOpen.fromSpec_map_basicOpen {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : ↑(X.presheaf.obj (Opposite.op U))) : (TopologicalSpace.Opens.map (AlgebraicGeometry.IsAffineOpen.fromSpec hU).val.base).obj (AlgebraicGeometry.Scheme.basicOpen X f) = PrimeSpectrum.basicOpen f

theorem AlgebraicGeometry.IsAffineOpen.basicOpen_union_eq_self_iff {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (s : Set ↑(X.presheaf.obj (Opposite.op U))) : ⨆ (f : ↑s), AlgebraicGeometry.Scheme.basicOpen X ↑f = U ↔ Ideal.span s = ⊤

theorem AlgebraicGeometry.IsAffineOpen.self_le_basicOpen_union_iff {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (s : Set ↑(X.presheaf.obj (Opposite.op U))) : U ≤ ⨆ (f : ↑s), AlgebraicGeometry.Scheme.basicOpen X ↑f ↔ Ideal.span s = ⊤

theorem AlgebraicGeometry.of_affine_open_cover {X : AlgebraicGeometry.Scheme} (V : ↑(AlgebraicGeometry.Scheme.affineOpens X)) (S : Set ↑(AlgebraicGeometry.Scheme.affineOpens X)) {P : ↑(AlgebraicGeometry.Scheme.affineOpens X) → Prop} (hP₁ : (U : ↑(AlgebraicGeometry.Scheme.affineOpens X)) → (f : ↑(X.presheaf.obj (Opposite.op ↑U))) → P U → P (AlgebraicGeometry.Scheme.affineBasicOpen X f)) (hP₂ : (U : ↑(AlgebraicGeometry.Scheme.affineOpens X)) → (s : Finset ↑(X.presheaf.obj (Opposite.op ↑U))) → Ideal.span ↑s = ⊤ → ((f : { x // x ∈ s }) → P (AlgebraicGeometry.Scheme.affineBasicOpen X ↑f)) → P U) (hS : ⋃ (i : ↑S), ↑↑↑i = Set.univ) (hS' : (U : ↑S) → P ↑U) : P V

Let P be a predicate on the affine open sets of X satisfying

1. If P holds on U, then P holds on the basic open set of every section on U.
2. If P holds for a family of basic open sets covering U, then P holds for U.
3. There exists an affine open cover of X each satisfying P.

Then P holds for every affine open of X.

This is also known as the Affine communication lemma in [The rising sea][RisingSea].