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

Equations

• AlgebraicGeometry.AffineScheme = AlgebraicGeometry.Scheme.Spec.EssImageSubcategory

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

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

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

theorem AlgebraicGeometry.IsAffine.affine {X : AlgebraicGeometry.Scheme} [self : AlgebraicGeometry.IsAffine X] : CategoryTheory.IsIso (AlgebraicGeometry.ΓSpec.adjunction.unit.app X)

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.

Equations

• X.isoSpec = CategoryTheory.asIso (AlgebraicGeometry.ΓSpec.adjunction.unit.app X)

@[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.

Equations

• AlgebraicGeometry.AffineScheme.mk X h = { obj := X, property := ⋯ }

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.

Equations

• AlgebraicGeometry.AffineScheme.of X = AlgebraicGeometry.AffineScheme.mk X h

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.

Equations

• AlgebraicGeometry.AffineScheme.ofHom f = f

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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.

Equations

• AlgebraicGeometry.AffineScheme.Spec = AlgebraicGeometry.Scheme.Spec.toEssImage

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

Equations

• AlgebraicGeometry.AffineScheme.Spec_full = ⋯

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

Equations

• AlgebraicGeometry.AffineScheme.Spec_faithful = ⋯

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

Equations

• AlgebraicGeometry.AffineScheme.Spec_essSurj = ⋯

@[simp]

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

@[simp]

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

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

The forgetful functor AffineScheme ⥤ Scheme.

Equations

• AlgebraicGeometry.AffineScheme.forgetToScheme = AlgebraicGeometry.Scheme.Spec.essImageInclusion

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

Equations

• AlgebraicGeometry.AffineScheme.forgetToScheme_full = ⋯

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

Equations

• AlgebraicGeometry.AffineScheme.forgetToScheme_faithful = ⋯

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

The global section functor of an affine scheme.

Equations

• AlgebraicGeometry.AffineScheme.Γ = AlgebraicGeometry.AffineScheme.forgetToScheme.op.comp AlgebraicGeometry.Scheme.Γ

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

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

Equations

• AlgebraicGeometry.AffineScheme.equivCommRingCat = CategoryTheory.equivEssImageOfReflective.symm

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

Equations

• AlgebraicGeometry.AffineScheme.ΓIsEquiv = AlgebraicGeometry.AffineScheme.Γ.rightOp.op.isEquivalenceTrans (CategoryTheory.opOpEquivalence CommRingCat).functor

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

Equations

• AlgebraicGeometry.AffineScheme.hasColimits = ⋯

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

Equations

• AlgebraicGeometry.AffineScheme.hasLimits = ⋯

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

Equations

• AlgebraicGeometry.AffineScheme.Γ_preservesLimits = CategoryTheory.Adjunction.isEquivalencePreservesLimits AlgebraicGeometry.AffineScheme.Γ.rightOp

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

Equations

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

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.

Equations

• AlgebraicGeometry.IsAffineOpen U = AlgebraicGeometry.IsAffine (X.restrict ⋯)

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

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

Equations

• X.affineOpens = {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace | AlgebraicGeometry.IsAffineOpen U}

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 : X.affineCover.J) : AlgebraicGeometry.IsAffine (X.affineCover.obj i)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

theorem AlgebraicGeometry.Scheme.map_PrimeSpectrum_basicOpen_of_affine (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] (f : ↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op X))) : X.isoSpec.hom⁻¹ᵁ PrimeSpectrum.basicOpen f = X.basicOpen f

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

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.

Equations

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

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

Equations

• ⋯ = ⋯

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

theorem AlgebraicGeometry.IsAffineOpen.fromSpec_image_top {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) : (AlgebraicGeometry.Scheme.Hom.opensFunctor hU.fromSpec).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.Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} : AlgebraicGeometry.IsAffineOpen ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U) ↔ AlgebraicGeometry.IsAffineOpen U

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

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.IsAffineOpen.fromSpec_base_preimage {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) : hU.fromSpec⁻¹ᵁ U = ⊤

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))) (hU.fromSpec.val.c.app (Opposite.op U)) = (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj (Opposite.op U)))).presheaf.map (CategoryTheory.eqToHom ⋯).op

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

theorem AlgebraicGeometry.IsAffineOpen.fromSpec_app_self {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) : hU.fromSpec.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 ⋯).op)

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))) : hU.fromSpec⁻¹ᵁ X.basicOpen f = (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj (Opposite.op U)))).basicOpen ((AlgebraicGeometry.SpecΓIdentity.inv.app (X.presheaf.obj (Opposite.op U))) 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))) : hU.fromSpec⁻¹ᵁ X.basicOpen f = PrimeSpectrum.basicOpen f

theorem AlgebraicGeometry.IsAffineOpen.opensFunctor_map_basicOpen {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : ↑(X.presheaf.obj (Opposite.op U))) : (AlgebraicGeometry.Scheme.Hom.opensFunctor hU.fromSpec).obj (PrimeSpectrum.basicOpen f) = X.basicOpen f

@[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.Spec.obj (Opposite.op (X.presheaf.obj (Opposite.op U)))).basicOpen ((hU.fromSpec.val.c.app (Opposite.op U)) f) = PrimeSpectrum.basicOpen f

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 (X.basicOpen f)

theorem AlgebraicGeometry.IsAffineOpen.mapRestrictBasicOpen {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (r : ↑(X.presheaf.obj (Opposite.op ⊤))) : AlgebraicGeometry.IsAffineOpen (AlgebraicGeometry.Scheme.ιOpens (X.basicOpen r)⁻¹ᵁ U)

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

def AlgebraicGeometry.IsAffineOpen.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 (X.basicOpen f)) ⟶ (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj (Opposite.op U)))).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))

Given an affine open U and some f : U, this is the canonical map Γ(𝒪ₓ, D(f)) ⟶ Γ(Spec 𝒪ₓ(U), D(f)) This is an isomorphism, as witnessed by an IsIso instance.

Equations

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

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

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.IsAffineOpen.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 (X.basicOpen 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 (X.basicOpen r)))

Equations

• ⋯ = ⋯

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

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 (X ∣_ᵤ X.basicOpen r)))

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.IsAffineOpen.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 (X.basicOpen f)))) : ∃ (f' : ↑(X.presheaf.obj (Opposite.op U))), X.basicOpen f' = X.basicOpen g

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

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

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

Equations

• hU.primeIdealOf x = (CategoryTheory.CategoryStruct.comp (X.restrict ⋯).isoSpec.hom (AlgebraicGeometry.Scheme.Spec.map (X.presheaf.map (CategoryTheory.eqToHom ⋯).op).op)).val.base x

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

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 : hU.fromSpec.val.base y ∈ U) : IsLocalization.AtPrime (↑(X.presheaf.stalk (hU.fromSpec.val.base y))) y.asIdeal

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

@[simp]

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

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

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

Equations

• X.affineBasicOpen f = ⟨X.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), X.basicOpen ↑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), X.basicOpen ↑f ↔ Ideal.span s = ⊤

theorem AlgebraicGeometry.of_affine_open_cover {X : AlgebraicGeometry.Scheme} (V : ↑X.affineOpens) (S : Set ↑X.affineOpens) {P : ↑X.affineOpens → Prop} (hP₁ : ∀ (U : ↑X.affineOpens) (f : ↑(X.presheaf.obj (Opposite.op ↑U))), P U → P (X.affineBasicOpen f)) (hP₂ : ∀ (U : ↑X.affineOpens) (s : Finset ↑(X.presheaf.obj (Opposite.op ↑U))), Ideal.span ↑s = ⊤ → (∀ (f : { x : ↑(X.presheaf.obj (Opposite.op ↑U)) // x ∈ s }), P (X.affineBasicOpen ↑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].