Affine schemes

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

Main definitions

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

def AlgebraicGeometry.AffineScheme : Type (u_1 + 1)

The category of affine schemes

Equations

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

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

Equations

• AlgebraicGeometry.instAffineSchemeCategory = CategoryTheory.Functor.instCategoryEssImageSubcategory

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.

Equations

• X.isoSpec = CategoryTheory.asIso X.toSpecΓ

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)

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.

Equations

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

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

Equations

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

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.

Equations

• AlgebraicGeometry.AffineScheme.ofHom f = f

theorem AlgebraicGeometry.mem_Spec_essImage (X : Scheme) : X ∈ Scheme.Spec.essImage ↔ 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

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.

Equations

• AlgebraicGeometry.arrowIsoSpecΓOfIsAffine f = CategoryTheory.Arrow.isoMk X.isoSpec Y.isoSpec ⋯

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.

Equations

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

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.

Equations

• AlgebraicGeometry.AffineScheme.Spec = AlgebraicGeometry.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.

Equations

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

@[simp]

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

@[simp]

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

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.

Equations

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

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

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

Equations

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

instance AlgebraicGeometry.AffineScheme.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.

Equations

• AlgebraicGeometry.IsAffineOpen U = AlgebraicGeometry.IsAffine ↑U

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

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

Equations

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

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 ⊤

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

Equations

• U.toSpecΓ = CategoryTheory.CategoryStruct.comp (↑U).toSpecΓ (AlgebraicGeometry.Spec.map U.topIso.inv)

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

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.

Equations

• hU.isoSpec = (↑U).isoSpec ≪≫ AlgebraicGeometry.Scheme.Spec.mapIso U.topIso.symm.op

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Γ

theorem AlgebraicGeometry.IsAffineOpen.isoSpec_hom_base_apply {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) (x : ↥U) : hU.isoSpec.hom.base x = (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

@[deprecated AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop (since := "2024-11-16")]

theorem AlgebraicGeometry.IsAffineOpen.isoSpec_inv_app_top {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

Alias of AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop.

@[deprecated AlgebraicGeometry.IsAffineOpen.isoSpec_hom_appTop (since := "2024-11-16")]

theorem AlgebraicGeometry.IsAffineOpen.isoSpec_hom_app_top {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

Alias of AlgebraicGeometry.IsAffineOpen.isoSpec_hom_appTop.

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.

Equations

• hU.fromSpec = CategoryTheory.CategoryStruct.comp hU.isoSpec.inv 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.range_fromSpec {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) : Set.range ⇑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.

Equations

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

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

Equations

• AlgebraicGeometry.affineOpensRestrict U = (AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv U.ι).trans (Equiv.subtypeEquivProp ⋯)

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

@[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.forget CommRingCat).obj (X.presheaf.obj (Opposite.op U))) : (Scheme.Hom.app hU.fromSpec U) x = ((Spec (X.presheaf.obj (Opposite.op U))).presheaf.map (CategoryTheory.eqToHom ⋯)) ((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 ((Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op U))).inv.hom 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 ((Scheme.Hom.app hU.fromSpec U).hom 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.instAlgebraCarrierObjOppositeOpensαTopologicalSpaceCarrierCommRingCatSpecPresheafOpOpens {R : CommRingCat} {U : (Spec R).Opens} : Algebra ↑R ↑((Spec R).presheaf.obj (Opposite.op U))

Equations

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

@[simp]

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

instance AlgebraicGeometry.IsAffineOpen.instAwayCarrierObjOppositeOpensαTopologicalSpaceCarrierCommRingCatSpecPresheafOpOpensBasicOpen {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.

Equations

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

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 ((Scheme.Hom.appLE f U V e).hom r)) ⋯ = CommRingCat.ofHom (IsLocalization.Away.map (↑(Y.presheaf.toPrefunctor.1 (Opposite.op (Y.basicOpen r)))) (↑(X.presheaf.toPrefunctor.1 (Opposite.op (X.basicOpen ((Scheme.Hom.appLE f U V e).hom r))))) (Scheme.Hom.appLE f U V e).hom 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 ((Scheme.Hom.app f U).hom r))))) (Scheme.Hom.app f U).hom 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 ((Scheme.Hom.app f U).hom r))))) (Scheme.Hom.app f U).hom r))

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

Equations

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

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.toPresheafedSpace) (hx : x ∈ U ⊓ V) : ∃ (f : ↑(X.presheaf.obj (Opposite.op U))) (g : ↑(X.presheaf.obj (Opposite.op V))), X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f

noncomputable def AlgebraicGeometry.IsAffineOpen.primeIdealOf {X : 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.

Equations

• hU.primeIdealOf x = hU.isoSpec.hom.base x

theorem AlgebraicGeometry.IsAffineOpen.fromSpec_primeIdealOf {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) (x : ↥U) : 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 = (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 : hU.fromSpec.base y ∈ U) : IsLocalization.AtPrime (↑(X.presheaf.stalk (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.toPresheafedSpace} (hU : IsAffineOpen U) (x : ↑↑X.toPresheafedSpace) (hx : f.base x ∈ U) (h : ∀ (g : ↑(Y.presheaf.obj (Opposite.op U))), (Scheme.Hom.stalkMap f x).hom ((Y.presheaf.germ U (f.base x) hx).hom g) = 0 → (Y.presheaf.germ U (f.base x) hx).hom g = 0) : Function.Injective ⇑(Scheme.Hom.stalkMap f x).hom

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.

Equations

• X.affineBasicOpen f = ⟨X.basicOpen f, ⋯⟩

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

Equations

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

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

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.

theorem AlgebraicGeometry.Scheme.toΓSpec_preimage_zeroLocus_eq {X : Scheme} (s : Set ↑(X.presheaf.obj (Opposite.op ⊤))) : ⇑X.toSpecΓ.base ⁻¹' PrimeSpectrum.zeroLocus s = X.zeroLocus s

On a locally ringed space X, the preimage of the zero locus of the prime spectrum of Γ(X, ⊤) under toΓSpecFun agrees with the associated zero locus on X.

theorem AlgebraicGeometry.Scheme.toΓSpec_image_zeroLocus_eq_of_isAffine {X : Scheme} [IsAffine X] (s : Set ↑(X.presheaf.obj (Opposite.op ⊤))) : ⇑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 toΓSpecFun is the zero locus in terms of the prime spectrum of Γ(X, ⊤).

theorem AlgebraicGeometry.Scheme.eq_zeroLocus_of_isClosed_of_isAffine (X : Scheme) [IsAffine X] (s : Set ↑↑X.toPresheafedSpace) : 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.

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.

Equations

• AlgebraicGeometry.specTargetImageIdeal f = RingHom.ker ((AlgebraicGeometry.ΓSpec.adjunction.homEquiv X (Opposite.op A)).symm f).unop.hom

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

Equations

• AlgebraicGeometry.specTargetImage f = CommRingCat.of (↑A ⧸ AlgebraicGeometry.specTargetImageIdeal f)

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.

Equations

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

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.

Equations

• AlgebraicGeometry.specTargetImageRingHom f = CommRingCat.ofHom (Ideal.Quotient.mk (AlgebraicGeometry.specTargetImageIdeal f))

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

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

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

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

The scheme-theoretic image of a morphism f : X ⟶ Y with affine target. f factors as affineTargetImageFactorization f ≫ affineTargetImageInclusion f (see affineTargetImageFactorization_comp).

Equations

• AlgebraicGeometry.affineTargetImage f = AlgebraicGeometry.Spec (AlgebraicGeometry.specTargetImage (CategoryTheory.CategoryStruct.comp f Y.isoSpec.hom))

instance AlgebraicGeometry.instIsAffineAffineTargetImage {X Y : Scheme} [IsAffine Y] (f : X ⟶ Y) : IsAffine (affineTargetImage f)

def AlgebraicGeometry.affineTargetImageInclusion {X Y : Scheme} [IsAffine Y] (f : X ⟶ Y) : affineTargetImage f ⟶ Y

The inclusion of the scheme-theoretic image of a morphism with affine target.

Equations

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

theorem AlgebraicGeometry.affineTargetImageInclusion_app_surjective {X Y : Scheme} [IsAffine Y] (f : X ⟶ Y) : Function.Surjective ⇑(Scheme.Hom.appTop (affineTargetImageInclusion f)).hom

def AlgebraicGeometry.affineTargetImageFactorization {X Y : Scheme} [IsAffine Y] (f : X ⟶ Y) : X ⟶ affineTargetImage f

The induced morphism from X to the scheme-theoretic image of a morphism f : X ⟶ Y with affine target.

Equations

• AlgebraicGeometry.affineTargetImageFactorization f = AlgebraicGeometry.specTargetImageFactorization (CategoryTheory.CategoryStruct.comp f Y.isoSpec.hom)

theorem AlgebraicGeometry.affineTargetImageFactorization_app_injective {X Y : Scheme} [IsAffine Y] (f : X ⟶ Y) : Function.Injective ⇑(Scheme.Hom.appTop (affineTargetImageFactorization f)).hom

@[simp]

theorem AlgebraicGeometry.affineTargetImageFactorization_comp {X Y : Scheme} [IsAffine Y] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (affineTargetImageFactorization f) (affineTargetImageInclusion f) = f

@[simp]

theorem AlgebraicGeometry.affineTargetImageFactorization_comp_assoc {X Y : Scheme} [IsAffine Y] (f : X ⟶ Y) {Z : Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (affineTargetImageFactorization f) (CategoryTheory.CategoryStruct.comp (affineTargetImageInclusion 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 f.hom) p)).hom (CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (Localization.localRingHom ((PrimeSpectrum.comap f.hom) p).asIdeal p.asIdeal f.hom ⋯)) (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.forget CommRingCat).obj ((Spec.structureSheaf ↑R).presheaf.stalk ((PrimeSpectrum.comap f.hom) p))) : (StructureSheaf.localizationToStalk (↑S) p) ((CommRingCat.ofHom (Localization.localRingHom (Ideal.comap f.hom p.asIdeal) p.asIdeal f.hom ⋯)) ((StructureSheaf.stalkToFiberRingHom (↑R) ((PrimeSpectrum.comap f.hom) 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 f.hom) p).asIdeal p.asIdeal f.hom ⋯))

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.

Equations

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

@[deprecated AlgebraicGeometry.isAffine_affineScheme (since := "2024-06-21")]

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

Alias of AlgebraicGeometry.isAffine_affineScheme.

@[deprecated AlgebraicGeometry.isAffine_Spec (since := "2024-06-21")]

theorem AlgebraicGeometry.SpecIsAffine (R : CommRingCat) : IsAffine (Spec R)

Alias of AlgebraicGeometry.isAffine_Spec.

@[deprecated AlgebraicGeometry.isAffine_of_isIso (since := "2024-06-21")]

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

Alias of AlgebraicGeometry.isAffine_of_isIso.

@[deprecated AlgebraicGeometry.isAffineOpen_opensRange (since := "2024-06-21")]

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

Alias of AlgebraicGeometry.isAffineOpen_opensRange.

@[deprecated AlgebraicGeometry.isAffineOpen_top (since := "2024-06-21")]

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

Alias of AlgebraicGeometry.isAffineOpen_top.

@[deprecated AlgebraicGeometry.Scheme.isAffine_affineCover (since := "2024-06-21")]

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

Alias of AlgebraicGeometry.Scheme.isAffine_affineCover.

@[deprecated AlgebraicGeometry.Scheme.isAffine_affineBasisCover (since := "2024-06-21")]

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

Alias of AlgebraicGeometry.Scheme.isAffine_affineBasisCover.

@[deprecated AlgebraicGeometry.IsAffineOpen.range_fromSpec (since := "2024-06-21")]

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

Alias of AlgebraicGeometry.IsAffineOpen.range_fromSpec.

@[deprecated AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion (since := "2024-06-21")]

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

Alias of AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion.

@[deprecated AlgebraicGeometry.Scheme.compactSpace_of_isAffine (since := "2024-06-21")]

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

Alias of AlgebraicGeometry.Scheme.compactSpace_of_isAffine.

@[deprecated AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self (since := "2024-06-21")]

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

Alias of AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self.

@[deprecated AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen' (since := "2024-06-21")]

theorem AlgebraicGeometry.IsAffineOpen.fromSpec_map_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 ((Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op U))).inv.hom f)

Alias of AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen'.

@[deprecated AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen (since := "2024-06-21")]

theorem AlgebraicGeometry.IsAffineOpen.fromSpec_map_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

Alias of AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen.

@[deprecated AlgebraicGeometry.IsAffineOpen.fromSpec_image_basicOpen (since := "2024-06-21")]

theorem AlgebraicGeometry.IsAffineOpen.opensFunctor_map_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

Alias of AlgebraicGeometry.IsAffineOpen.fromSpec_image_basicOpen.

@[deprecated AlgebraicGeometry.IsAffineOpen.basicOpen (since := "2024-06-21")]

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

Alias of AlgebraicGeometry.IsAffineOpen.basicOpen.

@[deprecated AlgebraicGeometry.IsAffineOpen.ι_basicOpen_preimage (since := "2024-06-21")]

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

Alias of AlgebraicGeometry.IsAffineOpen.ι_basicOpen_preimage.