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

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.instCategoryAffineScheme : 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)

noncomputable 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

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

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

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.

noncomputable 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

instance AlgebraicGeometry.instIsAffineXSchemeCover (P : CategoryTheory.MorphismProperty Scheme) {S : Scheme} (𝒰 : Scheme.AffineCover P S) (i : 𝒰.I₀) : IsAffine (𝒰.cover.X i)

instance AlgebraicGeometry.preservesLimit_rightOp_Γ {I : Type w} [CategoryTheory.Category.{v, w} I] (D : CategoryTheory.Functor I Scheme) [∀ (i : I), IsAffine (D.obj i)] : CategoryTheory.Limits.PreservesLimit D Scheme.Γ.rightOp

Scheme.Γ.rightOp : Scheme ⥤ CommRingCatᵒᵖ preserves limits of diagrams consisting of affine schemes.

instance AlgebraicGeometry.preservesColimit_Γ {I : Type w} [CategoryTheory.Category.{v, w} I] (D : CategoryTheory.Functor I Schemeᵒᵖ) [∀ (i : I), IsAffine (Opposite.unop (D.obj i))] : CategoryTheory.Limits.PreservesColimit D Scheme.Γ

Scheme.Γ : Schemeᵒᵖ ⥤ CommRingCat preserves colimits of diagrams consisting of affine schemes.

noncomputable 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_map {X✝ Y✝ : CategoryTheory.InducedCategory Scheme CategoryTheory.ObjectProperty.FullSubcategory.obj} (f : X✝ ⟶ Y✝) : forgetToScheme.map f = f.hom

@[simp]

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

We copy over instances from Scheme.Spec.essImageInclusion.

instance AlgebraicGeometry.AffineScheme.forgetToScheme_full : forgetToScheme.Full

instance AlgebraicGeometry.AffineScheme.forgetToScheme_faithful : forgetToScheme.Faithful

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

The global section functor of an affine scheme.

noncomputable 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

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.AffineScheme.createsLimitsForgetToScheme : CategoryTheory.CreatesLimits forgetToScheme

The forgetful functor AffineScheme ⥤ Scheme creates small limits.

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.I₀) : IsAffine (X.affineCover.X i)

instance AlgebraicGeometry.Scheme.isAffine_affineBasisCover (X : Scheme) (i : X.affineBasisCover.I₀) : IsAffine (X.affineBasisCover.X i)

instance AlgebraicGeometry.Scheme.isAffine_affineOpenCover (X : Scheme) (𝒰 : X.AffineOpenCover) (i : 𝒰.I₀) : IsAffine (𝒰.openCover.X i)

instance AlgebraicGeometry.instIsAffineXSchemeFiniteSubcover (X : Scheme) [CompactSpace ↥X] (𝒰 : X.OpenCover) [∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)] (i : 𝒰.finiteSubcover.I₀) : IsAffine (𝒰.finiteSubcover.X i)

instance AlgebraicGeometry.instIsAffineXSchemeCoverOfIsIsoIsOpenImmersionId {X : Scheme} [IsAffine X] (i : (Scheme.coverOfIsIso (CategoryTheory.CategoryStruct.id X)).I₀) : IsAffine ((Scheme.coverOfIsIso (CategoryTheory.CategoryStruct.id X)).X i)

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

@[deprecated AlgebraicGeometry.Scheme.isBasis_affineOpens (since := "2025-10-07")]

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

Alias of AlgebraicGeometry.Scheme.isBasis_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_presheaf_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_presheaf_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✝)

@[deprecated AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map (since := "2025-10-07")]

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Γ

Alias of AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map.

@[deprecated AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc (since := "2025-10-07")]

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✝)

Alias of AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc.

theorem AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top {X : Scheme} (U : X.Opens) : CategoryTheory.CategoryStruct.comp U.toSpecΓ (Spec.map (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) = CategoryTheory.CategoryStruct.comp U.ι X.toSpecΓ

theorem AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top_assoc {X : Scheme} (U : X.Opens) {Z : Scheme} (h : Spec (X.presheaf.obj (Opposite.op ⊤)) ⟶ Z) : CategoryTheory.CategoryStruct.comp U.toSpecΓ (CategoryTheory.CategoryStruct.comp (Spec.map (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) h) = CategoryTheory.CategoryStruct.comp U.ι (CategoryTheory.CategoryStruct.comp X.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)

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) : CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj U).toSpecΓ (Spec.map (Hom.app f U)) = CategoryTheory.CategoryStruct.comp (f ∣_ U) U.toSpecΓ

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality_assoc {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) {Z : Scheme} (h : Spec (Y.presheaf.obj (Opposite.op U)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj U).toSpecΓ (CategoryTheory.CategoryStruct.comp (Spec.map (Hom.app f U)) h) = CategoryTheory.CategoryStruct.comp (f ∣_ U) (CategoryTheory.CategoryStruct.comp U.toSpecΓ h)

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_appLE {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) (V : X.Opens) (hUV : V ≤ (TopologicalSpace.Opens.map f.base).obj U) : CategoryTheory.CategoryStruct.comp V.toSpecΓ (Spec.map (Hom.appLE f U V hUV)) = CategoryTheory.CategoryStruct.comp (Hom.resLE f U V hUV) U.toSpecΓ

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_appLE_assoc {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) (V : X.Opens) (hUV : V ≤ (TopologicalSpace.Opens.map f.base).obj U) {Z : Scheme} (h : Spec (Y.presheaf.obj (Opposite.op U)) ⟶ Z) : CategoryTheory.CategoryStruct.comp V.toSpecΓ (CategoryTheory.CategoryStruct.comp (Spec.map (Hom.appLE f U V hUV)) h) = CategoryTheory.CategoryStruct.comp (Hom.resLE f U V hUV) (CategoryTheory.CategoryStruct.comp U.toSpecΓ h)

noncomputable 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_apply {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) (x : ↥U) : hU.isoSpec.hom x = (Spec.map (X.presheaf.germ U ↑x ⋯)) (IsLocalRing.closedPoint ↑(X.presheaf.stalk ↑x))

@[deprecated AlgebraicGeometry.IsAffineOpen.isoSpec_hom_apply (since := "2025-10-07")]

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

Alias of AlgebraicGeometry.IsAffineOpen.isoSpec_hom_apply.

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

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

noncomputable 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 ⇑hU.fromSpec = ↑U

@[simp]

theorem AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) : CategoryTheory.CategoryStruct.comp hU.fromSpec X.toSpecΓ = Spec.map (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)

@[simp]

theorem AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ_assoc {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) {Z : Scheme} (h : Spec (X.presheaf.obj (Opposite.op ⊤)) ⟶ Z) : CategoryTheory.CategoryStruct.comp hU.fromSpec (CategoryTheory.CategoryStruct.comp X.toSpecΓ h) = CategoryTheory.CategoryStruct.comp (Spec.map (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) h

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

@[deprecated AlgebraicGeometry.IsAffineOpen.SpecMap_appLE_fromSpec (since := "2025-10-07")]

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

Alias of AlgebraicGeometry.IsAffineOpen.SpecMap_appLE_fromSpec.

@[deprecated AlgebraicGeometry.IsAffineOpen.SpecMap_appLE_fromSpec_assoc (since := "2025-10-07")]

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)

Alias of AlgebraicGeometry.IsAffineOpen.SpecMap_appLE_fromSpec_assoc.

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.Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] {U : X.Opens} : IsAffineOpen ((opensFunctor f).obj U) ↔ IsAffineOpen 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.IsAffineOpen.preimage_of_isOpenImmersion {X Y : Scheme} {U : Y.Opens} (hU : IsAffineOpen U) (f : X ⟶ Y) [IsOpenImmersion f] (hU' : U ≤ Scheme.Hom.opensRange f) : IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U)

def AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] : ↑X.affineOpens ≃o { 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 }) : ↑((RelIso.symm (affineOpensEquiv f)) 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 : ↑(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

@[implicit_reducible]

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)))

noncomputable 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)

noncomputable 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) : hU.fromSpec (hU.primeIdealOf x) = ↑x

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

theorem AlgebraicGeometry.IsAffineOpen.comap_primeIdealOf_appLE {X Y : Scheme} {f : X ⟶ Y} {x : ↥X} (U : Y.Opens) (hU : IsAffineOpen U) (V : X.Opens) (hV : IsAffineOpen V) (hVU : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (hx : x ∈ V) : PrimeSpectrum.comap (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)) (hV.primeIdealOf ⟨x, hx⟩) = hU.primeIdealOf ⟨f x, ⋯⟩

theorem AlgebraicGeometry.IsAffineOpen.primeIdealOf_isMaximal_of_isClosed {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) (x : ↥U) (hx : IsClosed {↑x}) : (hU.primeIdealOf x).asIdeal.IsMaximal

If a point x : U is a closed point, then its corresponding prime ideal is maximal.

theorem AlgebraicGeometry.IsAffineOpen.isLocalization_stalk' {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) (y : PrimeSpectrum ↑(X.presheaf.obj (Opposite.op U))) (hy : hU.fromSpec y ∈ U) : IsLocalization.AtPrime (↑(X.presheaf.stalk (hU.fromSpec 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 : f 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 (f x) hx)) g) = 0 → (CategoryTheory.ConcreteCategory.hom (Y.presheaf.germ U (f 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

noncomputable def AlgebraicGeometry.IsAffineOpen.arrowStalkMapIso {X Y : Scheme} (f : X ⟶ Y) {x : ↥X} (U : Y.Opens) (hU : IsAffineOpen U) (V : X.Opens) (hV : IsAffineOpen V) (hVU : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (hx : x ∈ V) : CategoryTheory.Arrow.mk (Scheme.Hom.stalkMap f x) ≅ CategoryTheory.Arrow.mk (CommRingCat.ofHom (Localization.localRingHom (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal (hV.primeIdealOf ⟨x, hx⟩).asIdeal (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)) ⋯))

Given affine opens x ∈ V ⊆ f⁻¹(U), the stalk map of f at x is isomorphic to Localization.localRingHom of f.appLE U V.

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.iSup_basicOpen_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.

@[deprecated AlgebraicGeometry.IsAffineOpen.iSup_basicOpen_eq_self_iff (since := "2025-10-07")]

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 = ⊤

Alias of AlgebraicGeometry.IsAffineOpen.iSup_basicOpen_eq_self_iff.

---

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_iSup_basicOpen_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 = ⊤

@[deprecated AlgebraicGeometry.IsAffineOpen.self_le_iSup_basicOpen_iff (since := "2025-10-07")]

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 = ⊤

Alias of AlgebraicGeometry.IsAffineOpen.self_le_iSup_basicOpen_iff.

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 (f x))) g) = 0 → (CategoryTheory.ConcreteCategory.hom (Y.presheaf.Γgerm (f 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 : ↥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.eq_of_SpecMap_comp_eq_of_isAffineOpen {R S : CommRingCat} {X : Scheme} (φ : R ⟶ S) (hφ : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom φ)) {f g : Spec R ⟶ X} (U : X.Opens) (hU : IsAffineOpen U) (hUf : (TopologicalSpace.Opens.map f.base).obj U = ⊤) (hUg : (TopologicalSpace.Opens.map g.base).obj U = ⊤) (H : CategoryTheory.CategoryStruct.comp (Spec.map φ) f = CategoryTheory.CategoryStruct.comp (Spec.map φ) g) : f = g

If φ is a monomorphism in CommRingCat, it is not in general true that Spec φ is epi. (ℤ ⊆ ℤ[1/2] but Spec ℤ[1/2] ⟶ Spec ℤ is not epi, since epi open immersions are isomorphisms) But if the range of f g : Spec R ⟶ X are contained in an common affine open U, one can still cancel Spec.map φ ≫ f = Spec.map φ ≫ g to get f = g.

theorem AlgebraicGeometry.Scheme.toSpecΓ_preimage_zeroLocus (X : Scheme) (s : Set ↑(X.presheaf.obj (Opposite.op ⊤))) : ⇑X.toSpecΓ ⁻¹' 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 ⊤))) : ⇑X.isoSpec.hom '' 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 ⊤))) : ⇑X.toSpecΓ '' X.zeroLocus s = PrimeSpectrum.zeroLocus s

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

theorem AlgebraicGeometry.Scheme.isoSpec_inv_image_zeroLocus (X : Scheme) [IsAffine X] (s : Set ↑(X.presheaf.obj (Opposite.op ⊤))) : ⇑X.isoSpec.inv '' 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_basicOpen {X : Scheme} (U : X.Opens) (r : ↑(X.presheaf.obj (Opposite.op U))) : (TopologicalSpace.Opens.map U.toSpecΓ.base).obj (PrimeSpectrum.basicOpen r) = (TopologicalSpace.Opens.map U.ι.base).obj (X.basicOpen r)

theorem AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_zeroLocus {X : Scheme} (U : X.Opens) (s : Set ↑(X.presheaf.obj (Opposite.op U))) : ⇑U.toSpecΓ ⁻¹' 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))) : ⇑hU.fromSpec ⁻¹' 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))) : ⇑hU.fromSpec '' 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)

noncomputable 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

noncomputable 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.

noncomputable 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).

noncomputable 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.

noncomputable 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

noncomputable def AlgebraicGeometry.Spec.stalkIso (R : CommRingCat) (x : PrimeSpectrum ↑R) : (Spec R).presheaf.stalk x ≅ CommRingCat.of (Localization.AtPrime x.asIdeal)

The stalk of Spec R at x is isomorphic to Rₚ, where p is the prime corresponding to x.

@[simp]

theorem AlgebraicGeometry.Spec.algebraMap_stalkIso_inv {R : CommRingCat} (x : PrimeSpectrum ↑R) : CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap (↑R) (Localization.AtPrime x.asIdeal))) (stalkIso R x).inv = CategoryTheory.CategoryStruct.comp (Scheme.ΓSpecIso R).inv ((Spec R).presheaf.germ ⊤ x trivial)

@[simp]

theorem AlgebraicGeometry.Spec.algebraMap_stalkIso_inv_assoc {R : CommRingCat} (x : PrimeSpectrum ↑R) {Z : CommRingCat} (h : (Spec R).presheaf.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap (↑R) (Localization.AtPrime x.asIdeal))) (CategoryTheory.CategoryStruct.comp (stalkIso R x).inv h) = CategoryTheory.CategoryStruct.comp (Scheme.ΓSpecIso R).inv (CategoryTheory.CategoryStruct.comp ((Spec R).presheaf.germ ⊤ x trivial) h)

@[simp]

theorem AlgebraicGeometry.Spec.germ_stalkMapIso_hom {R : CommRingCat} (x : PrimeSpectrum ↑R) : CategoryTheory.CategoryStruct.comp ((Spec R).presheaf.germ ⊤ x trivial) (stalkIso R x).hom = CategoryTheory.CategoryStruct.comp (Scheme.ΓSpecIso R).hom (CommRingCat.ofHom (algebraMap (↑R) (Localization.AtPrime x.asIdeal)))

@[simp]

theorem AlgebraicGeometry.Spec.germ_stalkMapIso_hom_assoc {R : CommRingCat} (x : PrimeSpectrum ↑R) {Z : CommRingCat} (h : CommRingCat.of (Localization.AtPrime x.asIdeal) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((Spec R).presheaf.germ ⊤ x trivial) (CategoryTheory.CategoryStruct.comp (stalkIso R x).hom h) = CategoryTheory.CategoryStruct.comp (Scheme.ΓSpecIso R).hom (CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap (↑R) (Localization.AtPrime x.asIdeal))) h)

theorem AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso {R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑S) : CategoryTheory.CategoryStruct.comp (Spec.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) ⋯)) (Spec.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 : ↑((Spec R).presheaf.stalk (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p))) : (CategoryTheory.ConcreteCategory.hom (Spec.stalkIso S p).inv) ((Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom f) ⋯) ((CategoryTheory.ConcreteCategory.hom (Spec.stalkIso R (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)).hom) x)) = (CategoryTheory.ConcreteCategory.hom (Hom.stalkMap (Spec.map f) p)) x

Variant of AlgebraicGeometry.localRingHom_comp_stalkIso for Spec.map.

noncomputable 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.