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 = CategoryTheory.Functor.EssImageSubcategory AlgebraicGeometry.Scheme.Spec

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)

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

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

Equations

• AlgebraicGeometry.Scheme.isoSpec X = 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 := (_ : X ∈ CategoryTheory.Functor.essImage AlgebraicGeometry.Scheme.Spec) }

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 ∈ CategoryTheory.Functor.essImage AlgebraicGeometry.Scheme.Spec ↔ AlgebraicGeometry.IsAffine X

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

Equations

• (_ : AlgebraicGeometry.IsAffine X.obj) = (_ : AlgebraicGeometry.IsAffine X.obj)

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

Equations

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

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 = CategoryTheory.Functor.toEssImage AlgebraicGeometry.Scheme.Spec

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

Equations

• AlgebraicGeometry.AffineScheme.Spec_full = CategoryTheory.Full.toEssImage AlgebraicGeometry.Scheme.Spec

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

Equations

• AlgebraicGeometry.AffineScheme.Spec_faithful = (_ : CategoryTheory.Faithful (CategoryTheory.Functor.toEssImage AlgebraicGeometry.Scheme.Spec))

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

Equations

• AlgebraicGeometry.AffineScheme.Spec_essSurj = (_ : CategoryTheory.EssSurj (CategoryTheory.Functor.toEssImage AlgebraicGeometry.Scheme.Spec))

@[simp]

theorem AlgebraicGeometry.AffineScheme.forgetToScheme_obj (self : CategoryTheory.FullSubcategory (CategoryTheory.Functor.essImage AlgebraicGeometry.Scheme.Spec)) : AlgebraicGeometry.AffineScheme.forgetToScheme.toPrefunctor.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.toPrefunctor.map f = f

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

The forgetful functor AffineScheme ⥤ Scheme.

Equations

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

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

Equations

• AlgebraicGeometry.AffineScheme.forgetToScheme_full = let_fun this := inferInstance; this

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

Equations

• AlgebraicGeometry.AffineScheme.forgetToScheme_faithful = (_ : CategoryTheory.Faithful (CategoryTheory.Functor.essImageInclusion AlgebraicGeometry.Scheme.Spec))

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

The global section functor of an affine scheme.

Equations

• AlgebraicGeometry.AffineScheme.Γ = CategoryTheory.Functor.comp AlgebraicGeometry.AffineScheme.forgetToScheme.op 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 : CategoryTheory.IsEquivalence AlgebraicGeometry.AffineScheme.Γ

Equations

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

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

Equations

• AlgebraicGeometry.AffineScheme.hasColimits = (_ : CategoryTheory.Limits.HasColimitsOfSize.{u, u, u, u + 1} AlgebraicGeometry.AffineScheme)

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

Equations

• AlgebraicGeometry.AffineScheme.hasLimits = (_ : CategoryTheory.Limits.HasLimitsOfSize.{u, u, u, u + 1} AlgebraicGeometry.AffineScheme)

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 (AlgebraicGeometry.Scheme.restrict X (_ : OpenEmbedding ⇑(TopologicalSpace.Opens.inclusion U)))

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

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

Equations

• AlgebraicGeometry.Scheme.affineOpens X = {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 : (AlgebraicGeometry.Scheme.affineCover X).J) : AlgebraicGeometry.IsAffine ((AlgebraicGeometry.Scheme.affineCover X).obj i)

Equations

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

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

Equations

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

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

theorem AlgebraicGeometry.Scheme.map_PrimeSpectrum_basicOpen_of_affine (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] (f : ↑(AlgebraicGeometry.Scheme.Γ.toPrefunctor.obj (Opposite.op X))) : (AlgebraicGeometry.Scheme.isoSpec X).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.toPrefunctor.obj (Opposite.op (X.presheaf.toPrefunctor.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 (AlgebraicGeometry.IsAffineOpen.fromSpec hU)

Equations

• (_ : AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.IsAffineOpen.fromSpec hU)) = (_ : 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) : (AlgebraicGeometry.Scheme.Hom.opensFunctor (AlgebraicGeometry.IsAffineOpen.fromSpec hU)).toPrefunctor.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).toPrefunctor.obj U)

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

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

Equations

• (_ : CompactSpace ↑↑X.toPresheafedSpace) = (_ : CompactSpace ↑↑X.toPresheafedSpace)

theorem AlgebraicGeometry.IsAffineOpen.fromSpec_base_preimage {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) : AlgebraicGeometry.IsAffineOpen.fromSpec hU⁻¹ᵁ 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.toPrefunctor.obj (Opposite.op U))) ((AlgebraicGeometry.IsAffineOpen.fromSpec hU).val.c.app (Opposite.op U)) = (AlgebraicGeometry.Scheme.Spec.toPrefunctor.obj (Opposite.op (X.presheaf.toPrefunctor.obj (Opposite.op U)))).presheaf.toPrefunctor.map (CategoryTheory.eqToHom (_ : AlgebraicGeometry.IsAffineOpen.fromSpec hU⁻¹ᵁ U = ⊤)).op

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

theorem AlgebraicGeometry.IsAffineOpen.fromSpec_app_self {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.toPrefunctor.obj (Opposite.op U))) ((AlgebraicGeometry.Scheme.Spec.toPrefunctor.obj (Opposite.op (X.presheaf.toPrefunctor.obj (Opposite.op U)))).presheaf.toPrefunctor.map (CategoryTheory.eqToHom (_ : AlgebraicGeometry.IsAffineOpen.fromSpec hU⁻¹ᵁ U = ⊤)).op)

theorem AlgebraicGeometry.IsAffineOpen.fromSpec_map_basicOpen' {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : ↑(X.presheaf.toPrefunctor.obj (Opposite.op U))) : AlgebraicGeometry.IsAffineOpen.fromSpec hU⁻¹ᵁ X.basicOpen f = (AlgebraicGeometry.Scheme.Spec.toPrefunctor.obj (Opposite.op (X.presheaf.toPrefunctor.obj (Opposite.op U)))).basicOpen ((AlgebraicGeometry.SpecΓIdentity.inv.app (X.presheaf.toPrefunctor.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.toPrefunctor.obj (Opposite.op U))) : AlgebraicGeometry.IsAffineOpen.fromSpec hU⁻¹ᵁ 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.toPrefunctor.obj (Opposite.op U))) : (AlgebraicGeometry.Scheme.Hom.opensFunctor (AlgebraicGeometry.IsAffineOpen.fromSpec hU)).toPrefunctor.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.toPrefunctor.obj (Opposite.op U))) : (AlgebraicGeometry.Scheme.Spec.toPrefunctor.obj (Opposite.op (X.presheaf.toPrefunctor.obj (Opposite.op U)))).basicOpen (((AlgebraicGeometry.IsAffineOpen.fromSpec hU).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.toPrefunctor.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.toPrefunctor.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.toPrefunctor.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.toPrefunctor.obj (Opposite.op U))) : X.presheaf.toPrefunctor.obj (Opposite.op (X.basicOpen f)) ⟶ (AlgebraicGeometry.Scheme.Spec.toPrefunctor.obj (Opposite.op (X.presheaf.toPrefunctor.obj (Opposite.op U)))).presheaf.toPrefunctor.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.toPrefunctor.obj (Opposite.op U))) : CategoryTheory.IsIso (AlgebraicGeometry.IsAffineOpen.basicOpenSectionsToAffine hU f)

Equations

• (_ : CategoryTheory.IsIso (AlgebraicGeometry.IsAffineOpen.basicOpenSectionsToAffine hU f)) = (_ : CategoryTheory.IsIso (AlgebraicGeometry.IsAffineOpen.basicOpenSectionsToAffine hU f))

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

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

Equations

• (_ : IsLocalization.Away r ↑(X.presheaf.toPrefunctor.obj (Opposite.op (X.basicOpen r)))) = (_ : IsLocalization.Away r ↑(X.presheaf.toPrefunctor.obj (Opposite.op (X.basicOpen r))))

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

instance AlgebraicGeometry.Γ_restrict_isLocalization (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] (r : ↑(AlgebraicGeometry.Scheme.Γ.toPrefunctor.obj (Opposite.op X))) : IsLocalization.Away r ↑(AlgebraicGeometry.Scheme.Γ.toPrefunctor.obj (Opposite.op (X ∣_ᵤ X.basicOpen r)))

Equations

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

theorem AlgebraicGeometry.IsAffineOpen.basicOpen_basicOpen_is_basicOpen {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : ↑(X.presheaf.toPrefunctor.obj (Opposite.op U))) (g : ↑(X.presheaf.toPrefunctor.obj (Opposite.op (X.basicOpen f)))) : ∃ (f' : ↑(X.presheaf.toPrefunctor.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.toPrefunctor.obj (Opposite.op U))) (g : ↑(X.presheaf.toPrefunctor.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.toPrefunctor.obj (Opposite.op U))

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

Equations

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

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

theorem AlgebraicGeometry.IsAffineOpen.isLocalization_stalk' {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (y : PrimeSpectrum ↑(X.presheaf.toPrefunctor.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 : ↥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.toPrefunctor.obj (Opposite.op ↑U))) : ↑(AlgebraicGeometry.Scheme.affineBasicOpen X f) = X.basicOpen f

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

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

Equations

• AlgebraicGeometry.Scheme.affineBasicOpen X f = { val := X.basicOpen f, property := (_ : AlgebraicGeometry.IsAffineOpen (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.toPrefunctor.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.toPrefunctor.obj (Opposite.op U))) : U ≤ ⨆ (f : ↑s), X.basicOpen ↑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.toPrefunctor.obj (Opposite.op ↑U))), P U → P (AlgebraicGeometry.Scheme.affineBasicOpen X f)) (hP₂ : ∀ (U : ↑(AlgebraicGeometry.Scheme.affineOpens X)) (s : Finset ↑(X.presheaf.toPrefunctor.obj (Opposite.op ↑U))), Ideal.span ↑s = ⊤ → (∀ (f : { x : ↑(X.presheaf.toPrefunctor.obj (Opposite.op ↑U)) // 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].