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

The category of affine schemes

Equations
Instances For

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

• affine :
Instances
def AlgebraicGeometry.Scheme.isoSpec :
X { unop := { unop := X } }

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

Equations
• X.isoSpec =
Instances For
@[simp]
theorem AlgebraicGeometry.AffineScheme.mk_obj :
∀ (x : ), .obj = X

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

Equations
• = { obj := X, property := }
Instances For

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

Equations
Instances For

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

Equations
Instances For
Equations
• =
Equations
• =
theorem AlgebraicGeometry.isAffineOfIso (f : X Y) [h : ] :

The Spec functor into the category of affine schemes.

Equations
Instances For
@[simp]
@[simp]
theorem AlgebraicGeometry.AffineScheme.forgetToScheme_map :
∀ {X Y : CategoryTheory.InducedCategory AlgebraicGeometry.Scheme CategoryTheory.FullSubcategory.obj} (f : X Y),

The forgetful functor AffineScheme ⥤ Scheme.

Equations
Instances For

The global section functor of an affine scheme.

Equations
Instances For

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

Equations
Instances For
Equations
• One or more equations did not get rendered due to their size.
def AlgebraicGeometry.IsAffineOpen (U : TopologicalSpace.Opens X.toPresheafedSpace) :

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

Equations
Instances For

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

Equations
Instances For
instance AlgebraicGeometry.instIsAffineRestrict (U : Y.affineOpens) :
Equations
• =
instance AlgebraicGeometry.Scheme.affineCoverIsAffine (i : X.affineCover.J) :
AlgebraicGeometry.IsAffine (X.affineCover.obj i)
Equations
• =
instance AlgebraicGeometry.Scheme.affineBasisCoverIsAffine (i : X.affineBasisCover.J) :
AlgebraicGeometry.IsAffine (X.affineBasisCover.obj i)
Equations
• =
theorem AlgebraicGeometry.Scheme.map_PrimeSpectrum_basicOpen_of_affine (f : ( { unop := X })) :
X.isoSpec.hom⁻¹ᵁ = X.basicOpen f
def AlgebraicGeometry.IsAffineOpen.fromSpec {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) :
{ unop := X.presheaf.obj { unop := U } } X

The open immersion Spec 𝒪ₓ(U) ⟶ X for an affine U.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• =
theorem AlgebraicGeometry.IsAffineOpen.fromSpec_range {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) :
Set.range hU.fromSpec.val.base = U
theorem AlgebraicGeometry.IsAffineOpen.isCompact {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) :
theorem AlgebraicGeometry.IsAffineOpen.imageIsOpenImmersion {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (f : X Y) :
Equations
• =
theorem AlgebraicGeometry.IsAffineOpen.fromSpec_base_preimage {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) :
hU.fromSpec⁻¹ᵁ U =
theorem AlgebraicGeometry.IsAffineOpen.SpecΓIdentity_hom_app_fromSpec {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) :
CategoryTheory.CategoryStruct.comp (.app (X.presheaf.obj { unop := U })) (hU.fromSpec.val.c.app { unop := U }) = ( { unop := X.presheaf.obj { unop := U } }).presheaf.map .op
theorem AlgebraicGeometry.IsAffineOpen.fromSpec_app_self_apply {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (x : (X.presheaf.obj { unop := U })) :
(hU.fromSpec.val.c.app { unop := U }) x = (( { unop := X.presheaf.obj { unop := U } }).presheaf.map ) ((AlgebraicGeometry.toSpecΓ (X.presheaf.obj { unop := U })) x)
theorem AlgebraicGeometry.IsAffineOpen.fromSpec_app_self {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) :
hU.fromSpec.val.c.app { unop := U } = CategoryTheory.CategoryStruct.comp (.app (X.presheaf.obj { unop := U })) (( { unop := X.presheaf.obj { unop := U } }).presheaf.map .op)
theorem AlgebraicGeometry.IsAffineOpen.fromSpec_map_basicOpen' {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (f : (X.presheaf.obj { unop := U })) :
hU.fromSpec⁻¹ᵁ X.basicOpen f = ( { unop := X.presheaf.obj { unop := U } }).basicOpen ((.app (X.presheaf.obj { unop := U })) f)
theorem AlgebraicGeometry.IsAffineOpen.fromSpec_map_basicOpen {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (f : (X.presheaf.obj { unop := U })) :
hU.fromSpec⁻¹ᵁ X.basicOpen f =
theorem AlgebraicGeometry.IsAffineOpen.opensFunctor_map_basicOpen {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (f : (X.presheaf.obj { unop := U })) :
(AlgebraicGeometry.Scheme.Hom.opensFunctor hU.fromSpec).obj = X.basicOpen f
@[simp]
theorem AlgebraicGeometry.IsAffineOpen.basicOpen_fromSpec_app {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (f : (X.presheaf.obj { unop := U })) :
( { unop := X.presheaf.obj { unop := U } }).basicOpen ((hU.fromSpec.val.c.app { unop := U }) f) =
theorem AlgebraicGeometry.IsAffineOpen.basicOpenIsAffine {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (f : (X.presheaf.obj { unop := U })) :
theorem AlgebraicGeometry.IsAffineOpen.mapRestrictBasicOpen {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (r : (X.presheaf.obj { unop := })) :
theorem AlgebraicGeometry.IsAffineOpen.exists_basicOpen_le {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) {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 {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (f : (X.presheaf.obj { unop := U })) :
X.presheaf.obj { unop := X.basicOpen f } ( { unop := X.presheaf.obj { unop := U } }).presheaf.obj { unop := }

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.
Instances For
instance AlgebraicGeometry.IsAffineOpen.basicOpenSectionsToAffine_isIso {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (f : (X.presheaf.obj { unop := U })) :
CategoryTheory.IsIso (hU.basicOpenSectionsToAffine f)
Equations
• =
theorem AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (f : (X.presheaf.obj { unop := U })) :
IsLocalization.Away f (X.presheaf.obj { unop := X.basicOpen f })
instance AlgebraicGeometry.isLocalization_away_of_isAffine (r : (X.presheaf.obj { unop := })) :
IsLocalization.Away r (X.presheaf.obj { unop := X.basicOpen r })
Equations
• =
theorem AlgebraicGeometry.IsAffineOpen.isLocalization_of_eq_basicOpen {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (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 (r : ( { unop := X })) :
IsLocalization.Away r ( { unop := X ∣_ᵤ X.basicOpen r })
Equations
• =
theorem AlgebraicGeometry.IsAffineOpen.basicOpen_basicOpen_is_basicOpen {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (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 {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) {V : TopologicalSpace.Opens X.toPresheafedSpace} (hV : ) (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 {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (x : U) :
PrimeSpectrum (X.presheaf.obj { unop := U })

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

Equations
Instances For
theorem AlgebraicGeometry.IsAffineOpen.fromSpec_primeIdealOf {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (x : U) :
hU.fromSpec.val.base (hU.primeIdealOf x) = x
theorem AlgebraicGeometry.IsAffineOpen.isLocalization_stalk' {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (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 {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (x : U) :
IsLocalization.AtPrime ((X.presheaf.stalk x)) (hU.primeIdealOf x).asIdeal
@[simp]
theorem AlgebraicGeometry.Scheme.affineBasicOpen_coe {U : X.affineOpens} (f : (X.presheaf.obj { unop := U })) :
(X.affineBasicOpen f) = X.basicOpen f
def AlgebraicGeometry.Scheme.affineBasicOpen {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,
Instances For
theorem AlgebraicGeometry.IsAffineOpen.basicOpen_union_eq_self_iff {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (s : Set (X.presheaf.obj { unop := U })) :
⨆ (f : s), X.basicOpen f = U
theorem AlgebraicGeometry.IsAffineOpen.self_le_basicOpen_union_iff {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (s : Set (X.presheaf.obj { unop := U })) :
U ⨆ (f : s), X.basicOpen f
theorem AlgebraicGeometry.of_affine_open_cover (V : X.affineOpens) (S : Set X.affineOpens) {P : X.affineOpensProp} (hP₁ : ∀ (U : X.affineOpens) (f : (X.presheaf.obj { unop := U })), P UP (X.affineBasicOpen f)) (hP₂ : ∀ (U : X.affineOpens) (s : Finset (X.presheaf.obj { unop := U })), = (∀ (f : { x : (X.presheaf.obj { unop := U }) // x s }), P (X.affineBasicOpen f))P U) (hS : ⋃ (i : S), i = Set.univ) (hS' : ∀ (U : S), P U) :
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].