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

Equations

• AlgebraicGeometry.instAffineSchemeCategory = CategoryTheory.Functor.instCategoryEssImageSubcategory

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

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

• affine : CategoryTheory.IsIso X.toSpecΓ

theorem AlgebraicGeometry.IsAffine.affine {X : AlgebraicGeometry.Scheme} [self : AlgebraicGeometry.IsAffine X] : CategoryTheory.IsIso X.toSpecΓ

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

Equations

• ⋯ = ⋯

def AlgebraicGeometry.Scheme.isoSpec (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] : X ≅ AlgebraicGeometry.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 : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] : X.isoSpec.hom = X.toSpecΓ

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

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

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

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

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

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

Equations

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

@[simp]

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

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

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

Equations

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

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

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

Equations

• AlgebraicGeometry.AffineScheme.ofHom f = f

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

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 : CommRingCat} {B : CommRingCat} (f : A ⟶ B) : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk (AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.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) : (AlgebraicGeometry.Spec R).isoSpec = AlgebraicGeometry.Scheme.Spec.mapIso (AlgebraicGeometry.Scheme.ΓSpecIso R).op

@[simp]

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

@[simp]

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

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

The Spec functor into the category of affine schemes.

Equations

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

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

Equations

• AlgebraicGeometry.AffineScheme.Spec_full = ⋯

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

Equations

• AlgebraicGeometry.AffineScheme.Spec_faithful = ⋯

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

Equations

• AlgebraicGeometry.AffineScheme.Spec_essSurj = ⋯

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

The forgetful functor AffineScheme ⥤ Scheme.

Equations

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

@[simp]

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

@[simp]

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

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

Equations

• AlgebraicGeometry.AffineScheme.forgetToScheme_full = ⋯

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

Equations

• AlgebraicGeometry.AffineScheme.forgetToScheme_faithful = ⋯

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

The global section functor of an affine scheme.

Equations

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

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

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

Equations

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

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

Equations

• AlgebraicGeometry.AffineScheme.instIsEquivalenceOppositeCommRingCatRightOpΓ = ⋯

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

Equations

• AlgebraicGeometry.AffineScheme.instIsEquivalenceOppositeCommRingCatOpRightOpΓ = ⋯

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

Equations

• AlgebraicGeometry.AffineScheme.ΓIsEquiv = ⋯

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

Equations

• AlgebraicGeometry.AffineScheme.hasColimits = ⋯

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

Equations

• AlgebraicGeometry.AffineScheme.hasLimits = ⋯

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

Equations

• AlgebraicGeometry.AffineScheme.Γ_preservesLimits = inferInstance

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

Equations

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

def AlgebraicGeometry.IsAffineOpen {X : AlgebraicGeometry.Scheme} (U : 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 : AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} (U : ↑Y.affineOpens) : AlgebraicGeometry.IsAffine ↑↑U

Equations

• ⋯ = ⋯

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

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

theorem AlgebraicGeometry.Scheme.map_PrimeSpectrum_basicOpen_of_affine (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.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 : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] : TopologicalSpace.Opens.IsBasis (Set.range X.basicOpen)

noncomputable def AlgebraicGeometry.Scheme.Opens.toSpecΓ {X : AlgebraicGeometry.Scheme} (U : X.Opens) : ↑U ⟶ AlgebraicGeometry.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)

def AlgebraicGeometry.IsAffineOpen.isoSpec {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) : ↑U ≅ AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) : hU.isoSpec.inv = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.map (CategoryTheory.eqToHom ⋯).op)) (↑U).isoSpec.inv

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

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

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

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

def AlgebraicGeometry.IsAffineOpen.fromSpec {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) : AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) : AlgebraicGeometry.IsOpenImmersion hU.fromSpec

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

theorem AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι_assoc {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) {Z : AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) : Set.range ⇑hU.fromSpec.base = ↑U

@[simp]

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

@[simp]

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

@[simp]

theorem AlgebraicGeometry.IsAffineOpen.map_fromSpec_assoc {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) {V : X.Opens} (hV : AlgebraicGeometry.IsAffineOpen V) (f : Opposite.op U ⟶ Opposite.op V) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {V : X.Opens} {U : Y.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (hV : AlgebraicGeometry.IsAffineOpen V) (i : V ≤ (TopologicalSpace.Opens.map f.base).obj U) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.appLE f U V i)) hU.fromSpec = CategoryTheory.CategoryStruct.comp hV.fromSpec f

theorem AlgebraicGeometry.IsAffineOpen.Spec_map_appLE_fromSpec_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {V : X.Opens} {U : Y.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (hV : AlgebraicGeometry.IsAffineOpen V) (i : V ≤ (TopologicalSpace.Opens.map f.base).obj U) {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] : ⋯.fromSpec = X.isoSpec.inv

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

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

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

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

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

def AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] : ↑X.affineOpens ≃ { U : ↑Y.affineOpens // ↑U ≤ AlgebraicGeometry.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_symm_apply_coe {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : { U : ↑Y.affineOpens // ↑U ≤ AlgebraicGeometry.Scheme.Hom.opensRange f }) : ↑((AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv f).symm U) = (TopologicalSpace.Opens.map f.base).obj ↑↑U

@[simp]

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

def AlgebraicGeometry.affineOpensRestrict {X : AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} (U : X.Opens) : ∀ (a : ↑(↑U).affineOpens), ↑↑((AlgebraicGeometry.affineOpensRestrict U) a) = (AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj ↑a

@[simp]

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

@[instance 100]

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

Equations

• ⋯ = ⋯

@[simp]

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

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

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

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

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

theorem AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (f : ↑(X.presheaf.obj (Opposite.op U))) : (AlgebraicGeometry.Scheme.Hom.opensFunctor hU.fromSpec).obj (PrimeSpectrum.basicOpen f) = X.basicOpen f

@[simp]

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

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

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

Equations

• ⋯ = ⋯

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

theorem AlgebraicGeometry.IsAffineOpen.exists_basicOpen_le {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.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

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

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

def AlgebraicGeometry.IsAffineOpen.appBasicOpenIsoAwayMap {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (h : AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U)) (r : ↑(Y.presheaf.obj (Opposite.op U))) : CategoryTheory.Arrow.mk (AlgebraicGeometry.Scheme.Hom.app f (Y.basicOpen r)) ≅ CategoryTheory.Arrow.mk (IsLocalization.Away.map (↑(Y.presheaf.obj (Opposite.op (Y.basicOpen r)))) (↑(X.presheaf.obj (Opposite.op (X.basicOpen ((AlgebraicGeometry.Scheme.Hom.app f U) r))))) (AlgebraicGeometry.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))

Equations

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

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

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.IsAffineOpen.basicOpen_basicOpen_is_basicOpen {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (f : ↑(X.presheaf.obj (Opposite.op U))) (g : ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) : ∃ (f' : ↑(X.presheaf.obj (Opposite.op U))), X.basicOpen f' = X.basicOpen g

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

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

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

Equations

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

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

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

theorem AlgebraicGeometry.IsAffineOpen.isLocalization_stalk' {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (x : ↥U) : IsLocalization.AtPrime (↑(X.presheaf.stalk ↑x)) (hU.primeIdealOf x).asIdeal

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

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

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

Equations

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

@[simp]

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

theorem AlgebraicGeometry.IsAffineOpen.basicOpen_union_eq_self_iff {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (s : Set ↑(X.presheaf.obj (Opposite.op U))) : U ≤ ⨆ (f : ↑s), X.basicOpen ↑f ↔ Ideal.span s = ⊤

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

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

Let P be a predicate on the affine open sets of X satisfying

1. If P holds on U, then P holds on the basic open set of every section on U.
2. If P holds for a family of basic open sets covering U, then P holds for U.
3. There exists an affine open cover of X each satisfying P.

Then P holds for every affine open of X.

This is also known as the Affine communication lemma in [The rising sea][RisingSea].

theorem AlgebraicGeometry.Scheme.toΓSpec_preimage_zeroLocus_eq {X : AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} [AlgebraicGeometry.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 : AlgebraicGeometry.Scheme) [AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} {A : CommRingCat} (f : X ⟶ AlgebraicGeometry.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

def AlgebraicGeometry.specTargetImage {X : AlgebraicGeometry.Scheme} {A : CommRingCat} (f : X ⟶ AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} {A : CommRingCat} (f : X ⟶ AlgebraicGeometry.Spec A) : X ⟶ AlgebraicGeometry.Spec (AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} {A : CommRingCat} (f : X ⟶ AlgebraicGeometry.Spec A) : A ⟶ AlgebraicGeometry.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 = Ideal.Quotient.mk (AlgebraicGeometry.specTargetImageIdeal f)

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

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

@[simp]

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

@[simp]

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

def AlgebraicGeometry.affineTargetImage {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) : AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) : AlgebraicGeometry.IsAffine (AlgebraicGeometry.affineTargetImage f)

Equations

• ⋯ = ⋯

def AlgebraicGeometry.affineTargetImageInclusion {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) : AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) : Function.Surjective ⇑(AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.affineTargetImageInclusion f) ⊤)

def AlgebraicGeometry.affineTargetImageFactorization {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) : X ⟶ AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) : Function.Injective ⇑(AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.affineTargetImageFactorization f) ⊤)

@[simp]

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

@[simp]

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

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

Variant of AlgebraicGeometry.localRingHom_comp_stalkIso for Spec.map.

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

def AlgebraicGeometry.Scheme.arrowStalkMapSpecIso {R : CommRingCat} {S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑S) : CategoryTheory.Arrow.mk (AlgebraicGeometry.Scheme.Hom.stalkMap (AlgebraicGeometry.Spec.map f) p) ≅ CategoryTheory.Arrow.mk (CommRingCat.ofHom (Localization.localRingHom ((PrimeSpectrum.comap f) p).asIdeal p.asIdeal 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.

Equations

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

@[deprecated AlgebraicGeometry.isAffine_affineScheme]

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

Alias of AlgebraicGeometry.isAffine_affineScheme.

Equations

• AlgebraicGeometry.isAffineAffineScheme = AlgebraicGeometry.isAffine_affineScheme

@[deprecated AlgebraicGeometry.isAffine_Spec]

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

Alias of AlgebraicGeometry.isAffine_Spec.

Equations

• AlgebraicGeometry.SpecIsAffine = AlgebraicGeometry.isAffine_Spec

@[deprecated AlgebraicGeometry.isAffine_of_isIso]

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

Alias of AlgebraicGeometry.isAffine_of_isIso.

@[deprecated AlgebraicGeometry.isAffineOpen_opensRange]

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

Alias of AlgebraicGeometry.isAffineOpen_opensRange.

@[deprecated AlgebraicGeometry.isAffineOpen_top]

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

Alias of AlgebraicGeometry.isAffineOpen_top.

@[deprecated AlgebraicGeometry.Scheme.isAffine_affineCover]

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

Alias of AlgebraicGeometry.Scheme.isAffine_affineCover.

Equations

• AlgebraicGeometry.Scheme.affineCoverIsAffine = AlgebraicGeometry.Scheme.isAffine_affineCover

@[deprecated AlgebraicGeometry.Scheme.isAffine_affineBasisCover]

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

Alias of AlgebraicGeometry.Scheme.isAffine_affineBasisCover.

Equations

• AlgebraicGeometry.Scheme.affineBasisCoverIsAffine = AlgebraicGeometry.Scheme.isAffine_affineBasisCover

@[deprecated AlgebraicGeometry.IsAffineOpen.range_fromSpec]

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

Alias of AlgebraicGeometry.IsAffineOpen.range_fromSpec.

@[deprecated AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion]

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

Alias of AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion.

@[deprecated AlgebraicGeometry.Scheme.compactSpace_of_isAffine]

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

Alias of AlgebraicGeometry.Scheme.compactSpace_of_isAffine.

Equations

• AlgebraicGeometry.Scheme.quasi_compact_of_affine = AlgebraicGeometry.Scheme.compactSpace_of_isAffine

@[deprecated AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self]

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

Alias of AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self.

@[deprecated AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen']

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

Alias of AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen'.

@[deprecated AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen]

theorem AlgebraicGeometry.IsAffineOpen.fromSpec_map_basicOpen {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.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]

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

Alias of AlgebraicGeometry.IsAffineOpen.fromSpec_image_basicOpen.

@[deprecated AlgebraicGeometry.IsAffineOpen.basicOpen]

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

Alias of AlgebraicGeometry.IsAffineOpen.basicOpen.

@[deprecated AlgebraicGeometry.IsAffineOpen.ι_basicOpen_preimage]

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

Alias of AlgebraicGeometry.IsAffineOpen.ι_basicOpen_preimage.