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

instance AlgebraicGeometry.instAffineSchemeCategory : CategoryTheory.Category.{u_1, u_1 + 1} AffineScheme

class AlgebraicGeometry.IsAffine (X : Scheme) : Prop

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

• affine : CategoryTheory.IsIso X.toSpecΓ

instance AlgebraicGeometry.instIsIsoSchemeAppUnitOppositeCommRingCatAdjunctionOfIsAffine (X : Scheme) [IsAffine X] : CategoryTheory.IsIso (ΓSpec.adjunction.unit.app X)

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

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

theorem AlgebraicGeometry.Scheme.isoSpec_hom (X : Scheme) [IsAffine X] : X.isoSpec.hom = X.toSpecΓ

theorem AlgebraicGeometry.Scheme.isoSpec_hom_naturality {X Y : Scheme} [IsAffine X] [IsAffine Y] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp X.isoSpec.hom (Spec.map (Hom.appTop f)) = CategoryTheory.CategoryStruct.comp f Y.isoSpec.hom

theorem AlgebraicGeometry.Scheme.isoSpec_hom_naturality_assoc {X Y : Scheme} [IsAffine X] [IsAffine Y] (f : X ⟶ Y) {Z : Scheme} (h : Spec (Y.presheaf.obj (Opposite.op ⊤)) ⟶ Z) : CategoryTheory.CategoryStruct.comp X.isoSpec.hom (CategoryTheory.CategoryStruct.comp (Spec.map (Hom.appTop f)) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp Y.isoSpec.hom h)

theorem AlgebraicGeometry.Scheme.isoSpec_inv_naturality {X Y : Scheme} [IsAffine X] [IsAffine Y] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (Spec.map (Hom.appTop f)) Y.isoSpec.inv = CategoryTheory.CategoryStruct.comp X.isoSpec.inv f

theorem AlgebraicGeometry.Scheme.isoSpec_inv_naturality_assoc {X Y : Scheme} [IsAffine X] [IsAffine Y] (f : X ⟶ Y) {Z : Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (Spec.map (Hom.appTop f)) (CategoryTheory.CategoryStruct.comp Y.isoSpec.inv h) = CategoryTheory.CategoryStruct.comp X.isoSpec.inv (CategoryTheory.CategoryStruct.comp f h)

@[simp]

theorem AlgebraicGeometry.Scheme.toSpecΓ_isoSpec_inv (X : Scheme) [IsAffine X] : CategoryTheory.CategoryStruct.comp X.toSpecΓ X.isoSpec.inv = CategoryTheory.CategoryStruct.id X

@[simp]

theorem AlgebraicGeometry.Scheme.toSpecΓ_isoSpec_inv_assoc (X : Scheme) [IsAffine X] {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp X.toSpecΓ (CategoryTheory.CategoryStruct.comp X.isoSpec.inv h) = h

@[simp]

theorem AlgebraicGeometry.Scheme.isoSpec_inv_toSpecΓ (X : Scheme) [IsAffine X] : CategoryTheory.CategoryStruct.comp X.isoSpec.inv X.toSpecΓ = CategoryTheory.CategoryStruct.id (Spec (X.presheaf.obj (Opposite.op ⊤)))

@[simp]

theorem AlgebraicGeometry.Scheme.isoSpec_inv_toSpecΓ_assoc (X : Scheme) [IsAffine X] {Z : Scheme} (h : Spec (X.presheaf.obj (Opposite.op ⊤)) ⟶ Z) : CategoryTheory.CategoryStruct.comp X.isoSpec.inv (CategoryTheory.CategoryStruct.comp X.toSpecΓ h) = h

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

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

@[simp]

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

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

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

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

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

@[simp]

theorem AlgebraicGeometry.essImage_Spec {X : Scheme} : Scheme.Spec.essImage X ↔ IsAffine X

@[deprecated AlgebraicGeometry.essImage_Spec (since := "2025-04-08")]

theorem AlgebraicGeometry.mem_Spec_essImage {X : Scheme} : Scheme.Spec.essImage X ↔ IsAffine X

Alias of AlgebraicGeometry.essImage_Spec.

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

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

instance AlgebraicGeometry.isAffine_Spec (R : CommRingCat) : IsAffine (Spec R)

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

@[deprecated AlgebraicGeometry.IsAffine.of_isIso (since := "2025-03-31")]

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

Alias of AlgebraicGeometry.IsAffine.of_isIso.

noncomputable def AlgebraicGeometry.arrowIsoSpecΓOfIsAffine {X Y : Scheme} [IsAffine X] [IsAffine Y] (f : X ⟶ Y) : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk (Spec.map (Scheme.Hom.appTop f))

If f : X ⟶ Y is a morphism between affine schemes, the corresponding arrow is isomorphic to the arrow of the morphism on prime spectra induced by the map on global sections.

def AlgebraicGeometry.arrowIsoΓSpecOfIsAffine {A B : CommRingCat} (f : A ⟶ B) : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk (Scheme.Hom.appTop (Spec.map f))

If f : A ⟶ B is a ring homomorphism, the corresponding arrow is isomorphic to the arrow of the morphism induced on global sections by the map on prime spectra.

theorem AlgebraicGeometry.Scheme.isoSpec_Spec (R : CommRingCat) : (Spec R).isoSpec = Scheme.Spec.mapIso (ΓSpecIso R).op

@[simp]

theorem AlgebraicGeometry.Scheme.isoSpec_Spec_hom (R : CommRingCat) : (Spec R).isoSpec.hom = Spec.map (ΓSpecIso R).hom

@[simp]

theorem AlgebraicGeometry.Scheme.isoSpec_Spec_inv (R : CommRingCat) : (Spec R).isoSpec.inv = Spec.map (ΓSpecIso R).inv

theorem AlgebraicGeometry.ext_of_isAffine {X Y : Scheme} [IsAffine Y] {f g : X ⟶ Y} (e : Scheme.Hom.appTop f = Scheme.Hom.appTop g) : f = g

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

The Spec functor into the category of affine schemes.

We copy over instances from Scheme.Spec.toEssImage.

instance AlgebraicGeometry.AffineScheme.Spec_full : Spec.Full

instance AlgebraicGeometry.AffineScheme.Spec_faithful : Spec.Faithful

instance AlgebraicGeometry.AffineScheme.Spec_essSurj : Spec.EssSurj

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

The forgetful functor AffineScheme ⥤ Scheme.

@[simp]

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

@[simp]

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

We copy over instances from Scheme.Spec.essImageInclusion.

instance AlgebraicGeometry.AffineScheme.forgetToScheme_full : forgetToScheme.Full

instance AlgebraicGeometry.AffineScheme.forgetToScheme_faithful : forgetToScheme.Faithful

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

The global section functor of an affine scheme.

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

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

instance AlgebraicGeometry.AffineScheme.instIsEquivalenceOppositeCommRingCatRightOpΓ : Γ.rightOp.IsEquivalence

instance AlgebraicGeometry.AffineScheme.instIsEquivalenceOppositeCommRingCatOpRightOpΓ : Γ.rightOp.op.IsEquivalence

instance AlgebraicGeometry.AffineScheme.ΓIsEquiv : Γ.IsEquivalence

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

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

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

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

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

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

def AlgebraicGeometry.Scheme.affineOpens (X : Scheme) : Set X.Opens

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

instance AlgebraicGeometry.instIsAffineToSchemeValOpensMemSetAffineOpens {Y : Scheme} (U : ↑Y.affineOpens) : IsAffine ↑↑U

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

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

theorem AlgebraicGeometry.exists_isAffineOpen_mem_and_subset {X : Scheme} {x : ↥X} {U : X.Opens} (hxU : x ∈ U) : ∃ (W : X.Opens), IsAffineOpen W ∧ x ∈ W ∧ W.carrier ⊆ ↑U

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

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

instance AlgebraicGeometry.Scheme.isAffine_affineOpenCover (X : Scheme) (𝒰 : X.AffineOpenCover) (i : 𝒰.J) : IsAffine (𝒰.openCover.obj i)

instance AlgebraicGeometry.instIsAffineObjIsOpenImmersionFiniteSubcover (X : Scheme) [CompactSpace ↥X] (𝒰 : X.OpenCover) [∀ (i : 𝒰.J), IsAffine (𝒰.obj i)] (i : 𝒰.finiteSubcover.J) : IsAffine (𝒰.finiteSubcover.obj i)

instance AlgebraicGeometry.instIsAffineObjIsOpenImmersionCoverOfIsIsoIdScheme {X : Scheme} [IsAffine X] (i : (Scheme.coverOfIsIso (CategoryTheory.CategoryStruct.id X)).J) : IsAffine ((Scheme.coverOfIsIso (CategoryTheory.CategoryStruct.id X)).obj i)

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

theorem AlgebraicGeometry.iSup_affineOpens_eq_top (X : Scheme) : ⨆ (i : ↑X.affineOpens), ↑i = ⊤

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

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

noncomputable def AlgebraicGeometry.Scheme.Opens.toSpecΓ {X : Scheme} (U : X.Opens) : ↑U ⟶ Spec (X.presheaf.obj (Opposite.op U))

The canonical map U ⟶ Spec Γ(X, U) for an open U ⊆ X.

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_map {X : Scheme} (U V : X.Opens) (h : U ≤ V) : CategoryTheory.CategoryStruct.comp U.toSpecΓ (Spec.map (X.presheaf.map (CategoryTheory.homOfLE h).op)) = CategoryTheory.CategoryStruct.comp (X.homOfLE h) V.toSpecΓ

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_map_assoc {X : Scheme} (U V : X.Opens) (h : U ≤ V) {Z : Scheme} (h✝ : Spec (X.presheaf.obj (Opposite.op V)) ⟶ Z) : CategoryTheory.CategoryStruct.comp U.toSpecΓ (CategoryTheory.CategoryStruct.comp (Spec.map (X.presheaf.map (CategoryTheory.homOfLE h).op)) h✝) = CategoryTheory.CategoryStruct.comp (X.homOfLE h) (CategoryTheory.CategoryStruct.comp V.toSpecΓ h✝)

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.toSpecΓ_top {X : Scheme} : ⊤.toSpecΓ = CategoryTheory.CategoryStruct.comp ⊤.ι X.toSpecΓ

theorem AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop {X : Scheme} (U : X.Opens) : Hom.appTop U.toSpecΓ = CategoryTheory.CategoryStruct.comp (ΓSpecIso (X.presheaf.obj (Opposite.op U))).hom U.topIso.inv

theorem AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop_assoc {X : Scheme} (U : X.Opens) {Z : CommRingCat} (h : (↑U).presheaf.obj (Opposite.op ⊤) ⟶ Z) : CategoryTheory.CategoryStruct.comp (Hom.appTop U.toSpecΓ) h = CategoryTheory.CategoryStruct.comp (ΓSpecIso (X.presheaf.obj (Opposite.op U))).hom (CategoryTheory.CategoryStruct.comp U.topIso.inv h)

def AlgebraicGeometry.IsAffineOpen.isoSpec {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) : ↑U ≅ Spec (X.presheaf.obj (Opposite.op U))

The isomorphism U ≅ Spec Γ(X, U) for an affine U.

theorem AlgebraicGeometry.IsAffineOpen.isoSpec_inv {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) : hU.isoSpec.inv = CategoryTheory.CategoryStruct.comp (Spec.map (X.presheaf.map (CategoryTheory.eqToHom ⋯).op)) (↑U).isoSpec.inv

theorem AlgebraicGeometry.IsAffineOpen.isoSpec_hom {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) : hU.isoSpec.hom = U.toSpecΓ

@[simp]

theorem AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) : CategoryTheory.CategoryStruct.comp U.toSpecΓ hU.isoSpec.inv = CategoryTheory.CategoryStruct.id ↑U

@[simp]

theorem AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv_assoc {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) {Z : Scheme} (h : ↑U ⟶ Z) : CategoryTheory.CategoryStruct.comp U.toSpecΓ (CategoryTheory.CategoryStruct.comp hU.isoSpec.inv h) = h

@[simp]

theorem AlgebraicGeometry.IsAffineOpen.isoSpec_inv_toSpecΓ {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) : CategoryTheory.CategoryStruct.comp hU.isoSpec.inv U.toSpecΓ = CategoryTheory.CategoryStruct.id (Spec (X.presheaf.obj (Opposite.op U)))

@[simp]

theorem AlgebraicGeometry.IsAffineOpen.isoSpec_inv_toSpecΓ_assoc {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) {Z : Scheme} (h : Spec (X.presheaf.obj (Opposite.op U)) ⟶ Z) : CategoryTheory.CategoryStruct.comp hU.isoSpec.inv (CategoryTheory.CategoryStruct.comp U.toSpecΓ h) = h

theorem AlgebraicGeometry.IsAffineOpen.isoSpec_hom_base_apply {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) (x : ↥U) : (CategoryTheory.ConcreteCategory.hom hU.isoSpec.hom.base) x = (CategoryTheory.ConcreteCategory.hom (Spec.map (X.presheaf.germ U ↑x ⋯)).base) (IsLocalRing.closedPoint ↑(X.presheaf.stalk ↑x))

theorem AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) : Scheme.Hom.appTop hU.isoSpec.inv = CategoryTheory.CategoryStruct.comp U.topIso.hom (Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op U))).inv

theorem AlgebraicGeometry.IsAffineOpen.isoSpec_hom_appTop {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) : Scheme.Hom.appTop hU.isoSpec.hom = CategoryTheory.CategoryStruct.comp (Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op U))).hom U.topIso.inv

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

The open immersion Spec Γ(X, U) ⟶ X for an affine U.

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

@[simp]

theorem AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) : CategoryTheory.CategoryStruct.comp hU.isoSpec.inv U.ι = hU.fromSpec

@[simp]

theorem AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι_assoc {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp hU.isoSpec.inv (CategoryTheory.CategoryStruct.comp U.ι h) = CategoryTheory.CategoryStruct.comp hU.fromSpec h

@[simp]

theorem AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) : CategoryTheory.CategoryStruct.comp U.toSpecΓ hU.fromSpec = U.ι

@[simp]

theorem AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec_assoc {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp U.toSpecΓ (CategoryTheory.CategoryStruct.comp hU.fromSpec h) = CategoryTheory.CategoryStruct.comp U.ι h

@[simp]

theorem AlgebraicGeometry.IsAffineOpen.range_fromSpec {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom hU.fromSpec.base) = ↑U

@[simp]

theorem AlgebraicGeometry.IsAffineOpen.opensRange_fromSpec {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) : Scheme.Hom.opensRange hU.fromSpec = U

@[simp]

theorem AlgebraicGeometry.IsAffineOpen.map_fromSpec {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) {V : X.Opens} (hV : IsAffineOpen V) (f : Opposite.op U ⟶ Opposite.op V) : CategoryTheory.CategoryStruct.comp (Spec.map (X.presheaf.map f)) hU.fromSpec = hV.fromSpec

@[simp]

theorem AlgebraicGeometry.IsAffineOpen.map_fromSpec_assoc {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) {V : X.Opens} (hV : IsAffineOpen V) (f : Opposite.op U ⟶ Opposite.op V) {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (Spec.map (X.presheaf.map f)) (CategoryTheory.CategoryStruct.comp hU.fromSpec h) = CategoryTheory.CategoryStruct.comp hV.fromSpec h

theorem AlgebraicGeometry.IsAffineOpen.Spec_map_appLE_fromSpec {X Y : Scheme} (f : X ⟶ Y) {V : X.Opens} {U : Y.Opens} (hU : IsAffineOpen U) (hV : IsAffineOpen V) (i : V ≤ (TopologicalSpace.Opens.map f.base).obj U) : CategoryTheory.CategoryStruct.comp (Spec.map (Scheme.Hom.appLE f U V i)) hU.fromSpec = CategoryTheory.CategoryStruct.comp hV.fromSpec f

theorem AlgebraicGeometry.IsAffineOpen.Spec_map_appLE_fromSpec_assoc {X Y : Scheme} (f : X ⟶ Y) {V : X.Opens} {U : Y.Opens} (hU : IsAffineOpen U) (hV : IsAffineOpen V) (i : V ≤ (TopologicalSpace.Opens.map f.base).obj U) {Z : Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (Spec.map (Scheme.Hom.appLE f U V i)) (CategoryTheory.CategoryStruct.comp hU.fromSpec h) = CategoryTheory.CategoryStruct.comp hV.fromSpec (CategoryTheory.CategoryStruct.comp f h)

theorem AlgebraicGeometry.IsAffineOpen.fromSpec_top {X : Scheme} [IsAffine X] : ⋯.fromSpec = X.isoSpec.inv

theorem AlgebraicGeometry.IsAffineOpen.fromSpec_app_of_le {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) (V : X.Opens) (h : U ≤ V) : Scheme.Hom.app hU.fromSpec V = CategoryTheory.CategoryStruct.comp (X.presheaf.map (CategoryTheory.homOfLE h).op) (CategoryTheory.CategoryStruct.comp (Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op U))).inv ((Spec (X.presheaf.obj (Opposite.op U))).presheaf.map (CategoryTheory.homOfLE ⋯).op))

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

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

theorem AlgebraicGeometry.IsAffineOpen.preimage_of_isIso {X Y : Scheme} {U : Y.Opens} (hU : IsAffineOpen U) (f : X ⟶ Y) [CategoryTheory.IsIso f] : IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U)

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

def AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] : ↑X.affineOpens ≃ { U : ↑Y.affineOpens // ↑U ≤ Scheme.Hom.opensRange f }

The affine open sets of an open subscheme corresponds to the affine open sets containing in the image.

@[simp]

theorem AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv_apply_coe_coe {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : ↑X.affineOpens) : ↑↑((affineOpensEquiv f) U) = (Scheme.Hom.opensFunctor f).obj ↑U

@[simp]

theorem AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv_symm_apply_coe {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] (U : { U : ↑Y.affineOpens // ↑U ≤ Scheme.Hom.opensRange f }) : ↑((affineOpensEquiv f).symm U) = (TopologicalSpace.Opens.map f.base).obj ↑↑U

def AlgebraicGeometry.affineOpensRestrict {X : Scheme} (U : X.Opens) : ↑(↑U).affineOpens ≃ { V : ↑X.affineOpens // ↑V ≤ U }

The affine open sets of an open subscheme corresponds to the affine open sets containing in the subset.

@[simp]

theorem AlgebraicGeometry.affineOpensRestrict_apply_coe_coe {X : Scheme} (U : X.Opens) (a✝ : ↑(↑U).affineOpens) : ↑↑((affineOpensRestrict U) a✝) = (Scheme.Hom.opensFunctor U.ι).obj ↑a✝

@[simp]

theorem AlgebraicGeometry.affineOpensRestrict_symm_apply_coe {X : Scheme} (U : X.Opens) (V : { V : ↑X.affineOpens // ↑V ≤ U }) : ↑((affineOpensRestrict U).symm V) = (TopologicalSpace.Opens.map U.ι.base).obj ↑↑V

@[instance 100]

instance AlgebraicGeometry.Scheme.compactSpace_of_isAffine (X : Scheme) [IsAffine X] : CompactSpace ↥X

@[simp]

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

theorem AlgebraicGeometry.IsAffineOpen.ΓSpecIso_hom_fromSpec_app {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) : CategoryTheory.CategoryStruct.comp (Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op U))).hom (Scheme.Hom.app hU.fromSpec U) = (Spec (X.presheaf.obj (Opposite.op U))).presheaf.map (CategoryTheory.eqToHom ⋯).op

theorem AlgebraicGeometry.IsAffineOpen.fromSpec_app_self {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) : Scheme.Hom.app hU.fromSpec U = CategoryTheory.CategoryStruct.comp (Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op U))).inv ((Spec (X.presheaf.obj (Opposite.op U))).presheaf.map (CategoryTheory.eqToHom ⋯).op)

theorem AlgebraicGeometry.IsAffineOpen.fromSpec_app_self_apply {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) (x : CategoryTheory.ToType (X.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.app hU.fromSpec U)) x = (CategoryTheory.ConcreteCategory.hom ((Spec (X.presheaf.obj (Opposite.op U))).presheaf.map (CategoryTheory.eqToHom ⋯))) ((CategoryTheory.ConcreteCategory.hom (Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op U))).inv) x)

theorem AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen' {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) (f : ↑(X.presheaf.obj (Opposite.op U))) : (TopologicalSpace.Opens.map hU.fromSpec.base).obj (X.basicOpen f) = (Spec (X.presheaf.obj (Opposite.op U))).basicOpen ((CategoryTheory.ConcreteCategory.hom (Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op U))).inv) f)

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

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

@[simp]

theorem AlgebraicGeometry.IsAffineOpen.basicOpen_fromSpec_app {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) (f : ↑(X.presheaf.obj (Opposite.op U))) : (Spec (X.presheaf.obj (Opposite.op U))).basicOpen ((CategoryTheory.ConcreteCategory.hom (Scheme.Hom.app hU.fromSpec U)) f) = PrimeSpectrum.basicOpen f

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

theorem AlgebraicGeometry.IsAffineOpen.Spec_basicOpen {R : CommRingCat} (f : ↑R) : IsAffineOpen (PrimeSpectrum.basicOpen f)

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

theorem AlgebraicGeometry.IsAffineOpen.ι_basicOpen_preimage {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) (r : ↑(X.presheaf.obj (Opposite.op ⊤))) : IsAffineOpen ((TopologicalSpace.Opens.map (X.basicOpen r).ι.base).obj U)

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

noncomputable instance AlgebraicGeometry.IsAffineOpen.instAlgebraCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecPresheafOpOpens {R : CommRingCat} {U : (Spec R).Opens} : Algebra ↑R ↑((Spec R).presheaf.obj (Opposite.op U))

@[simp]

theorem AlgebraicGeometry.IsAffineOpen.algebraMap_Spec_obj {R : CommRingCat} {U : (Spec R).Opens} : algebraMap ↑R ↑((Spec R).presheaf.obj (Opposite.op U)) = CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (Scheme.ΓSpecIso R).inv ((Spec R).presheaf.map (CategoryTheory.homOfLE ⋯).op))

instance AlgebraicGeometry.IsAffineOpen.instAwayCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecPresheafOpOpensBasicOpen {R : CommRingCat} {f : ↑R} : IsLocalization.Away f ↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f)))

def AlgebraicGeometry.IsAffineOpen.basicOpenSectionsToAffine {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) (f : ↑(X.presheaf.obj (Opposite.op U))) : X.presheaf.obj (Opposite.op (X.basicOpen f)) ⟶ (Spec (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.

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

theorem AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen {X : Scheme} {U : X.Opens} (hU : 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 : Scheme} [IsAffine X] (r : ↑(X.presheaf.obj (Opposite.op ⊤))) : IsLocalization.Away r ↑(X.presheaf.obj (Opposite.op (X.basicOpen r)))

theorem AlgebraicGeometry.IsAffineOpen.appLE_eq_away_map {X Y : Scheme} (f : X ⟶ Y) {U : Y.Opens} (hU : IsAffineOpen U) {V : X.Opens} (hV : IsAffineOpen V) (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (r : ↑(Y.presheaf.obj (Opposite.op U))) : Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen ((CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) ⋯ = CommRingCat.ofHom (IsLocalization.Away.map (↑(Y.presheaf.1 (Opposite.op (Y.basicOpen r)))) (↑(X.presheaf.1 (Opposite.op (X.basicOpen ((CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r))))) (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)) r)

theorem AlgebraicGeometry.IsAffineOpen.app_basicOpen_eq_away_map {X Y : Scheme} (f : X ⟶ Y) {U : Y.Opens} (hU : IsAffineOpen U) (h : IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U)) (r : ↑(Y.presheaf.obj (Opposite.op U))) : Scheme.Hom.app f (Y.basicOpen r) = CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (IsLocalization.Away.map (↑(Y.presheaf.obj (Opposite.op (Y.basicOpen r)))) (↑(X.presheaf.obj (Opposite.op (X.basicOpen ((CategoryTheory.ConcreteCategory.hom (Scheme.Hom.app f U)) r))))) (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r)) (X.presheaf.map (CategoryTheory.eqToHom ⋯).op)

def AlgebraicGeometry.IsAffineOpen.appBasicOpenIsoAwayMap {X Y : Scheme} (f : X ⟶ Y) {U : Y.Opens} (hU : IsAffineOpen U) (h : IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U)) (r : ↑(Y.presheaf.obj (Opposite.op U))) : CategoryTheory.Arrow.mk (Scheme.Hom.app f (Y.basicOpen r)) ≅ CategoryTheory.Arrow.mk (CommRingCat.ofHom (IsLocalization.Away.map (↑(Y.presheaf.obj (Opposite.op (Y.basicOpen r)))) (↑(X.presheaf.obj (Opposite.op (X.basicOpen ((CategoryTheory.ConcreteCategory.hom (Scheme.Hom.app f U)) r))))) (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r))

f.app (Y.basicOpen r) is isomorphic to map induced on localizations Γ(Y, Y.basicOpen r) ⟶ Γ(X, X.basicOpen (f.app U r))

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

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

theorem AlgebraicGeometry.IsAffineOpen.basicOpen_basicOpen_is_basicOpen {X : Scheme} {U : X.Opens} (hU : 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 : Scheme} {U : X.Opens} (hU : IsAffineOpen U) {V : X.Opens} (hV : IsAffineOpen V) (x : ↥X) (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 : Scheme} {U : X.Opens} (hU : IsAffineOpen U) (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 : Scheme} {U : X.Opens} (hU : IsAffineOpen U) (x : ↥U) : (CategoryTheory.ConcreteCategory.hom hU.fromSpec.base) (hU.primeIdealOf x) = ↑x

theorem AlgebraicGeometry.IsAffineOpen.primeIdealOf_eq_map_closedPoint {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) (x : ↥U) : hU.primeIdealOf x = (CategoryTheory.ConcreteCategory.hom (Spec.map (X.presheaf.germ U ↑x ⋯)).base) (IsLocalRing.closedPoint ↑(X.presheaf.stalk ↑x))

theorem AlgebraicGeometry.IsAffineOpen.isLocalization_stalk' {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) (y : PrimeSpectrum ↑(X.presheaf.obj (Opposite.op U))) (hy : (CategoryTheory.ConcreteCategory.hom hU.fromSpec.base) y ∈ U) : IsLocalization.AtPrime (↑(X.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom hU.fromSpec.base) y))) y.asIdeal

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

theorem AlgebraicGeometry.IsAffineOpen.stalkMap_injective {X Y : Scheme} (f : X ⟶ Y) {U : TopologicalSpace.Opens ↥Y} (hU : IsAffineOpen U) (x : ↥X) (hx : (CategoryTheory.ConcreteCategory.hom f.base) x ∈ U) (h : ∀ (g : ↑(Y.presheaf.obj (Opposite.op U))), (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap f x)) ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.germ U ((CategoryTheory.ConcreteCategory.hom f.base) x) hx)) g) = 0 → (CategoryTheory.ConcreteCategory.hom (Y.presheaf.germ U ((CategoryTheory.ConcreteCategory.hom f.base) x) hx)) g = 0) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

theorem AlgebraicGeometry.IsAffineOpen.mem_ideal_iff {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) {s : ↑(X.presheaf.obj (Opposite.op U))} {I : Ideal ↑(X.presheaf.obj (Opposite.op U))} : s ∈ I ↔ ∀ (x : ↥X) (h : x ∈ U), (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x h)) s ∈ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I

theorem AlgebraicGeometry.IsAffineOpen.ideal_le_iff {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) {I J : Ideal ↑(X.presheaf.obj (Opposite.op U))} : I ≤ J ↔ ∀ (x : ↥X) (h : x ∈ U), Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I ≤ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J

theorem AlgebraicGeometry.IsAffineOpen.ideal_ext_iff {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) {I J : Ideal ↑(X.presheaf.obj (Opposite.op U))} : I = J ↔ ∀ (x : ↥X) (h : x ∈ U), Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I = Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J

def AlgebraicGeometry.Scheme.affineBasicOpen (X : 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.

@[simp]

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

theorem AlgebraicGeometry.Scheme.affineBasicOpen_le (X : Scheme) {V : ↑X.affineOpens} (f : ↑(X.presheaf.obj (Opposite.op ↑V))) : X.affineBasicOpen f ≤ V

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

In an affine open set U, a family of basic open covers U iff the sections span Γ(X, U). See iSup_basicOpen_of_span_eq_top for the inverse direction without the affine-ness assumption.

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

noncomputable def AlgebraicGeometry.SpecMapRestrictBasicOpenIso {R S : CommRingCat} (f : R ⟶ S) (r : ↑R) : CategoryTheory.Arrow.mk (Spec.map f ∣_ PrimeSpectrum.basicOpen r) ≅ CategoryTheory.Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))

The restriction of Spec.map f to a basic open D(r) is isomorphic to Spec.map of the localization of f away from r.

theorem AlgebraicGeometry.stalkMap_injective_of_isAffine {X Y : Scheme} (f : X ⟶ Y) [IsAffine Y] (x : ↥X) (h : ∀ (g : ↑(Y.presheaf.obj (Opposite.op ⊤))), (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap f x)) ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.Γgerm ((CategoryTheory.ConcreteCategory.hom f.base) x))) g) = 0 → (CategoryTheory.ConcreteCategory.hom (Y.presheaf.Γgerm ((CategoryTheory.ConcreteCategory.hom f.base) x))) g = 0) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

theorem AlgebraicGeometry.iSup_basicOpen_of_span_eq_top {X : Scheme} (U : X.Opens) (s : Set ↑(X.presheaf.obj (Opposite.op U))) (hs : Ideal.span s = ⊤) : ⨆ i ∈ s, X.basicOpen i = U

Given a spanning set of Γ(X, U), the corresponding basic open sets cover U. See IsAffineOpen.basicOpen_union_eq_self_iff for the inverse direction for affine open sets.

theorem AlgebraicGeometry.of_affine_open_cover {X : Scheme} {P : ↑X.affineOpens → Prop} {ι : Sort u_2} (U : ι → ↑X.affineOpens) (iSup_U : ⨆ (i : ι), ↑(U i) = ⊤) (V : ↑X.affineOpens) (basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑(X.presheaf.obj (Opposite.op ↑U))), P U → P (X.affineBasicOpen f)) (openCover : ∀ (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) (hU : ∀ (i : ι), P (U i)) : 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].

theorem AlgebraicGeometry.Scheme.toSpecΓ_preimage_zeroLocus (X : Scheme) (s : Set ↑(X.presheaf.obj (Opposite.op ⊤))) : ⇑(CategoryTheory.ConcreteCategory.hom X.toSpecΓ.base) ⁻¹' PrimeSpectrum.zeroLocus s = X.zeroLocus s

On a scheme X, the preimage of the zero locus of the prime spectrum of Γ(X, ⊤) under X.toSpecΓ : X ⟶ Spec Γ(X, ⊤) agrees with the associated zero locus on X.

theorem AlgebraicGeometry.Scheme.isoSpec_image_zeroLocus (X : Scheme) [IsAffine X] (s : Set ↑(X.presheaf.obj (Opposite.op ⊤))) : ⇑(CategoryTheory.ConcreteCategory.hom X.isoSpec.hom.base) '' X.zeroLocus s = PrimeSpectrum.zeroLocus s

If X is affine, the image of the zero locus of global sections of X under X.isoSpec is the zero locus in terms of the prime spectrum of Γ(X, ⊤).

theorem AlgebraicGeometry.Scheme.toSpecΓ_image_zeroLocus (X : Scheme) [IsAffine X] (s : Set ↑(X.presheaf.obj (Opposite.op ⊤))) : ⇑(CategoryTheory.ConcreteCategory.hom X.toSpecΓ.base) '' X.zeroLocus s = PrimeSpectrum.zeroLocus s

theorem AlgebraicGeometry.Scheme.isoSpec_inv_preimage_zeroLocus (X : Scheme) [IsAffine X] (s : Set ↑(X.presheaf.obj (Opposite.op ⊤))) : ⇑(CategoryTheory.ConcreteCategory.hom X.isoSpec.inv.base) ⁻¹' X.zeroLocus s = PrimeSpectrum.zeroLocus s

theorem AlgebraicGeometry.Scheme.isoSpec_inv_image_zeroLocus (X : Scheme) [IsAffine X] (s : Set ↑(X.presheaf.obj (Opposite.op ⊤))) : ⇑(CategoryTheory.ConcreteCategory.hom X.isoSpec.inv.base) '' PrimeSpectrum.zeroLocus s = X.zeroLocus s

theorem AlgebraicGeometry.Scheme.eq_zeroLocus_of_isClosed_of_isAffine (X : Scheme) [IsAffine X] (s : Set ↥X) : IsClosed s ↔ ∃ (I : Ideal ↑(X.presheaf.obj (Opposite.op ⊤))), s = X.zeroLocus ↑I

If X is an affine scheme, every closed set of X is the zero locus of a set of global sections.

theorem AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_zeroLocus {X : Scheme} (U : X.Opens) (s : Set ↑(X.presheaf.obj (Opposite.op U))) : ⇑(CategoryTheory.ConcreteCategory.hom U.toSpecΓ.base) ⁻¹' PrimeSpectrum.zeroLocus s = Subtype.val ⁻¹' X.zeroLocus s

theorem AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_zeroLocus {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) (s : Set ↑(X.presheaf.obj (Opposite.op U))) : ⇑(CategoryTheory.ConcreteCategory.hom hU.fromSpec.base) ⁻¹' X.zeroLocus s = PrimeSpectrum.zeroLocus s

theorem AlgebraicGeometry.IsAffineOpen.fromSpec_image_zeroLocus {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) (s : Set ↑(X.presheaf.obj (Opposite.op U))) : ⇑(CategoryTheory.ConcreteCategory.hom hU.fromSpec.base) '' PrimeSpectrum.zeroLocus s = X.zeroLocus s ∩ ↑U

theorem AlgebraicGeometry.Scheme.zeroLocus_inf (X : Scheme) {U : X.Opens} (I J : Ideal ↑(X.presheaf.obj (Opposite.op U))) : X.zeroLocus ↑(I ⊓ J) = X.zeroLocus ↑I ∪ X.zeroLocus ↑J

theorem AlgebraicGeometry.Scheme.zeroLocus_biInf {X : Scheme} {U : X.Opens} {ι : Type u_1} (I : ι → Ideal ↑(X.presheaf.obj (Opposite.op U))) {t : Set ι} (ht : t.Finite) : X.zeroLocus ↑(⨅ i ∈ t, I i) = (⋃ i ∈ t, X.zeroLocus ↑(I i)) ∪ (↑U)ᶜ

theorem AlgebraicGeometry.Scheme.zeroLocus_biInf_of_nonempty {X : Scheme} {U : X.Opens} {ι : Type u_1} (I : ι → Ideal ↑(X.presheaf.obj (Opposite.op U))) {t : Set ι} (ht : t.Finite) (ht' : t.Nonempty) : X.zeroLocus ↑(⨅ i ∈ t, I i) = ⋃ i ∈ t, X.zeroLocus ↑(I i)

theorem AlgebraicGeometry.Scheme.zeroLocus_iInf {X : Scheme} {U : X.Opens} {ι : Type u_1} (I : ι → Ideal ↑(X.presheaf.obj (Opposite.op U))) [Finite ι] : X.zeroLocus ↑(⨅ (i : ι), I i) = (⋃ (i : ι), X.zeroLocus ↑(I i)) ∪ (↑U)ᶜ

theorem AlgebraicGeometry.Scheme.zeroLocus_iInf_of_nonempty {X : Scheme} {U : X.Opens} {ι : Type u_1} (I : ι → Ideal ↑(X.presheaf.obj (Opposite.op U))) [Finite ι] [Nonempty ι] : X.zeroLocus ↑(⨅ (i : ι), I i) = ⋃ (i : ι), X.zeroLocus ↑(I i)

def AlgebraicGeometry.Scheme.Hom.liftQuotient {X : Scheme} {A : CommRingCat} (f : X.Hom (Spec A)) (I : Ideal ↑A) (hI : I ≤ RingHom.ker (CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (ΓSpecIso A).inv f.appTop))) : X ⟶ Spec (CommRingCat.of (↑A ⧸ I))

Given f : X ⟶ Spec A and some ideal I ≤ ker(A ⟶ Γ(X, ⊤)), this is the lift to X ⟶ Spec (A ⧸ I).

theorem AlgebraicGeometry.Scheme.Hom.liftQuotient_comp {X : Scheme} {A : CommRingCat} (f : X.Hom (Spec A)) (I : Ideal ↑A) (hI : I ≤ RingHom.ker (CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (ΓSpecIso A).inv f.appTop))) : CategoryTheory.CategoryStruct.comp (f.liftQuotient I hI) (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) = f

theorem AlgebraicGeometry.Scheme.Hom.liftQuotient_comp_assoc {X : Scheme} {A : CommRingCat} (f : X.Hom (Spec A)) (I : Ideal ↑A) (hI : I ≤ RingHom.ker (CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (ΓSpecIso A).inv f.appTop))) {Z : Scheme} (h : Spec (CommRingCat.of ↑A) ⟶ Z) : CategoryTheory.CategoryStruct.comp (f.liftQuotient I hI) (CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) h) = CategoryTheory.CategoryStruct.comp f h

def AlgebraicGeometry.specTargetImageIdeal {X : Scheme} {A : CommRingCat} (f : X ⟶ Spec A) : Ideal ↑A

If X ⟶ Spec A is a morphism of schemes, then Spec of A ⧸ specTargetImage f is the scheme-theoretic image of f. For this quotient as an object of CommRingCat see specTargetImage below.

def AlgebraicGeometry.specTargetImage {X : Scheme} {A : CommRingCat} (f : X ⟶ Spec A) : CommRingCat

If X ⟶ Spec A is a morphism of schemes, then Spec of specTargetImage f is the scheme-theoretic image of f and f factors as specTargetImageFactorization f ≫ Spec.map (specTargetImageRingHom f) (see specTargetImageFactorization_comp).

def AlgebraicGeometry.specTargetImageFactorization {X : Scheme} {A : CommRingCat} (f : X ⟶ Spec A) : X ⟶ Spec (specTargetImage f)

If f : X ⟶ Spec A is a morphism of schemes, then f factors via the inclusion of Spec (specTargetImage f) into X.

def AlgebraicGeometry.specTargetImageRingHom {X : Scheme} {A : CommRingCat} (f : X ⟶ Spec A) : A ⟶ specTargetImage f

If f : X ⟶ Spec A is a morphism of schemes, the induced morphism on spectra of specTargetImageRingHom f is the inclusion of the scheme-theoretic image of f into Spec A.

theorem AlgebraicGeometry.specTargetImageRingHom_surjective {X : Scheme} {A : CommRingCat} (f : X ⟶ Spec A) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (specTargetImageRingHom f))

theorem AlgebraicGeometry.specTargetImageFactorization_app_injective {X : Scheme} {A : CommRingCat} (f : X ⟶ Spec A) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop (specTargetImageFactorization f)))

@[simp]

theorem AlgebraicGeometry.specTargetImageFactorization_comp {X : Scheme} {A : CommRingCat} (f : X ⟶ Spec A) : CategoryTheory.CategoryStruct.comp (specTargetImageFactorization f) (Spec.map (specTargetImageRingHom f)) = f

@[simp]

theorem AlgebraicGeometry.specTargetImageFactorization_comp_assoc {X : Scheme} {A : CommRingCat} (f : X ⟶ Spec A) {Z : Scheme} (h : Spec A ⟶ Z) : CategoryTheory.CategoryStruct.comp (specTargetImageFactorization f) (CategoryTheory.CategoryStruct.comp (Spec.map (specTargetImageRingHom f)) h) = CategoryTheory.CategoryStruct.comp f h

theorem AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso {R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑S) : CategoryTheory.CategoryStruct.comp (StructureSheaf.stalkIso (↑R) ((PrimeSpectrum.comap (CommRingCat.Hom.hom f)) p)).hom (CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (Localization.localRingHom ((PrimeSpectrum.comap (CommRingCat.Hom.hom f)) p).asIdeal p.asIdeal (CommRingCat.Hom.hom f) ⋯)) (StructureSheaf.stalkIso (↑S) p).inv) = Hom.stalkMap (Spec.map f) p

Variant of AlgebraicGeometry.localRingHom_comp_stalkIso for Spec.map.

theorem AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso_apply {R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑S) (x : CategoryTheory.ToType ((Spec.structureSheaf ↑R).presheaf.stalk ((PrimeSpectrum.comap (CommRingCat.Hom.hom f)) p))) : (CategoryTheory.ConcreteCategory.hom (StructureSheaf.localizationToStalk (↑S) p)) ((Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom f) ⋯) ((CategoryTheory.ConcreteCategory.hom (StructureSheaf.stalkToFiberRingHom (↑R) ((PrimeSpectrum.comap (CommRingCat.Hom.hom f)) p))) x)) = (Hom.stalkMap (Spec.map f) p) x

def AlgebraicGeometry.Scheme.arrowStalkMapSpecIso {R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑S) : CategoryTheory.Arrow.mk (Hom.stalkMap (Spec.map f) p) ≅ CategoryTheory.Arrow.mk (CommRingCat.ofHom (Localization.localRingHom ((PrimeSpectrum.comap (CommRingCat.Hom.hom f)) p).asIdeal p.asIdeal (CommRingCat.Hom.hom f) ⋯))

Given a morphism of rings f : R ⟶ S, the stalk map of Spec S ⟶ Spec R at a prime of S is isomorphic to the localized ring homomorphism.