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

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

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

• affine : CategoryTheory.IsIso (AlgebraicGeometry.ΓSpec.adjunction.unit.app X)

theorem AlgebraicGeometry.IsAffine.affine {X : AlgebraicGeometry.Scheme} [self : AlgebraicGeometry.IsAffine X] : CategoryTheory.IsIso (AlgebraicGeometry.ΓSpec.adjunction.unit.app X)

theorem AlgebraicGeometry.Scheme.isoSpec_hom (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] : X.isoSpec.hom = AlgebraicGeometry.ΓSpec.adjunction.unit.app X

def AlgebraicGeometry.Scheme.isoSpec (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] : X ≅ AlgebraicGeometry.Spec (X.presheaf.obj { unop := ⊤ })

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

Equations

• X.isoSpec = CategoryTheory.asIso (AlgebraicGeometry.ΓSpec.adjunction.unit.app X)

@[simp]

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

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 := ⋯ }

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

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

@[simp]

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

@[simp]

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

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

The forgetful functor AffineScheme ⥤ Scheme.

Equations

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

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 : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : Prop

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

Equations

• AlgebraicGeometry.IsAffineOpen U = AlgebraicGeometry.IsAffine (X.restrict ⋯)

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

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

Equations

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

instance AlgebraicGeometry.instIsAffineRestrict {Y : AlgebraicGeometry.Scheme} (U : ↑Y.affineOpens) : AlgebraicGeometry.IsAffine (Y ∣_ᵤ ↑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

• ⋯ = ⋯

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

theorem AlgebraicGeometry.Scheme.map_PrimeSpectrum_basicOpen_of_affine (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] (f : ↑(AlgebraicGeometry.Scheme.Γ.obj { unop := X })) : (TopologicalSpace.Opens.map X.isoSpec.hom.val.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)

def AlgebraicGeometry.IsAffineOpen.fromSpec {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) : AlgebraicGeometry.Spec (X.presheaf.obj { unop := U }) ⟶ X

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

Equations

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

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

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

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

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

theorem AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] : AlgebraicGeometry.IsAffineOpen ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).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 : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} : AlgebraicGeometry.IsAffineOpen (f.opensFunctor.obj U) ↔ AlgebraicGeometry.IsAffineOpen U

@[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.val.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.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.affineOpensRestrict_apply_coe_coe {X : AlgebraicGeometry.Scheme} (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : ∀ (a : ↑(X.restrict ⋯).affineOpens), ↑↑((AlgebraicGeometry.affineOpensRestrict U) a) = (AlgebraicGeometry.Scheme.Hom.opensFunctor (AlgebraicGeometry.Scheme.ιOpens U)).obj ↑a

def AlgebraicGeometry.affineOpensRestrict {X : AlgebraicGeometry.Scheme} (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : ↑(X ∣_ᵤ 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 (AlgebraicGeometry.Scheme.ιOpens U)).trans (Equiv.subtypeEquivProp ⋯)

@[simp]

theorem AlgebraicGeometry.affineOpensRestrict_symm_apply_coe {X : AlgebraicGeometry.Scheme} (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (V : { V : ↑X.affineOpens // ↑V ≤ U }) : ↑((AlgebraicGeometry.affineOpensRestrict U).symm V) = (TopologicalSpace.Opens.map (AlgebraicGeometry.Scheme.ιOpens U).val.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 : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) : (TopologicalSpace.Opens.map hU.fromSpec.val.base).obj U = ⊤

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

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

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

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

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

theorem AlgebraicGeometry.IsAffineOpen.fromSpec_image_basicOpen {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : ↑(X.presheaf.obj { unop := 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 : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : ↑(X.presheaf.obj { unop := U })) : (AlgebraicGeometry.Spec (X.presheaf.obj { unop := U })).basicOpen ((AlgebraicGeometry.Scheme.Hom.app hU.fromSpec U) f) = PrimeSpectrum.basicOpen f

theorem AlgebraicGeometry.IsAffineOpen.basicOpen {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : ↑(X.presheaf.obj { unop := U })) : AlgebraicGeometry.IsAffineOpen (X.basicOpen f)

theorem AlgebraicGeometry.IsAffineOpen.ιOpens_basicOpen_preimage {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (r : ↑(X.presheaf.obj { unop := ⊤ })) : AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map (AlgebraicGeometry.Scheme.ιOpens (X.basicOpen r)).val.base).obj U)

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

def AlgebraicGeometry.IsAffineOpen.basicOpenSectionsToAffine {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : ↑(X.presheaf.obj { unop := U })) : X.presheaf.obj { unop := X.basicOpen f } ⟶ (AlgebraicGeometry.Spec (X.presheaf.obj { unop := U })).presheaf.obj { unop := PrimeSpectrum.basicOpen f }

Given an affine open U and some f : U, this is the canonical map Γ(𝒪ₓ, D(f)) ⟶ Γ(Spec 𝒪ₓ(U), D(f)) This is an isomorphism, as witnessed by an IsIso instance.

Equations

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

instance AlgebraicGeometry.IsAffineOpen.basicOpenSectionsToAffine_isIso {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : ↑(X.presheaf.obj { unop := U })) : CategoryTheory.IsIso (hU.basicOpenSectionsToAffine f)

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.IsAffineOpen.appLE_eq_away_map {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hV : AlgebraicGeometry.IsAffineOpen V) (e : V ≤ (TopologicalSpace.Opens.map f.val.base).obj U) (r : ↑(Y.presheaf.obj { unop := 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 { unop := Y.basicOpen r })) (↑(X.presheaf.obj { unop := X.basicOpen ((AlgebraicGeometry.Scheme.Hom.appLE f U V e) r) })) (AlgebraicGeometry.Scheme.Hom.appLE f U V e) r

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

instance AlgebraicGeometry.Γ_restrict_isLocalization (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] (r : ↑(AlgebraicGeometry.Scheme.Γ.obj { unop := X })) : IsLocalization.Away r ↑(AlgebraicGeometry.Scheme.Γ.obj { unop := X ∣_ᵤ X.basicOpen r })

Equations

• ⋯ = ⋯

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

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

noncomputable def AlgebraicGeometry.IsAffineOpen.primeIdealOf {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (x : ↥U) : PrimeSpectrum ↑(X.presheaf.obj { unop := U })

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

Equations

• hU.primeIdealOf x = (CategoryTheory.CategoryStruct.comp (X.restrict ⋯).isoSpec.hom (AlgebraicGeometry.Spec.map (X.presheaf.map (CategoryTheory.eqToHom ⋯).op))).val.base x

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

theorem AlgebraicGeometry.IsAffineOpen.isLocalization_stalk' {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (y : PrimeSpectrum ↑(X.presheaf.obj { unop := U })) (hy : hU.fromSpec.val.base y ∈ U) : IsLocalization.AtPrime (↑(X.presheaf.stalk (hU.fromSpec.val.base y))) y.asIdeal

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

@[simp]

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

def AlgebraicGeometry.Scheme.affineBasicOpen (X : AlgebraicGeometry.Scheme) {U : ↑X.affineOpens} (f : ↑(X.presheaf.obj { unop := ↑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, ⋯⟩

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

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

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 { unop := ↑U })), P U → P (X.affineBasicOpen f)) (openCover : ∀ (U : ↑X.affineOpens) (s : Finset ↑(X.presheaf.obj { unop := ↑U })), Ideal.span ↑s = ⊤ → (∀ (f : { x : ↑(X.presheaf.obj { unop := ↑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 { unop := ⊤ })) : ⇑(AlgebraicGeometry.ΓSpec.adjunction.unit.app X).val.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 { unop := ⊤ })) : ⇑X.isoSpec.hom.val.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 { unop := ⊤ })), 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.

@[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 : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) : Set.range ⇑hU.fromSpec.val.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 : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (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 : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) : (TopologicalSpace.Opens.map hU.fromSpec.val.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 : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : ↑(X.presheaf.obj { unop := U })) : (TopologicalSpace.Opens.map hU.fromSpec.val.base).obj (X.basicOpen f) = (AlgebraicGeometry.Spec (X.presheaf.obj { unop := U })).basicOpen ((AlgebraicGeometry.Scheme.ΓSpecIso (X.presheaf.obj { unop := 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 : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : ↑(X.presheaf.obj { unop := U })) : (TopologicalSpace.Opens.map hU.fromSpec.val.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 : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : ↑(X.presheaf.obj { unop := 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 : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : ↑(X.presheaf.obj { unop := U })) : AlgebraicGeometry.IsAffineOpen (X.basicOpen f)

Alias of AlgebraicGeometry.IsAffineOpen.basicOpen.

@[deprecated AlgebraicGeometry.IsAffineOpen.ιOpens_basicOpen_preimage]

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

Alias of AlgebraicGeometry.IsAffineOpen.ιOpens_basicOpen_preimage.