# Documentation

Mathlib.AlgebraicGeometry.AffineScheme

# 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

Instances For
• affine :

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

Instances

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

Instances For
@[simp]
theorem AlgebraicGeometry.AffineScheme.mk_obj (h : ) :
().obj = X

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

Instances For

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

Instances For

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

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

The Spec functor into the category of affine schemes.

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

The forgetful functor AffineScheme ⥤ Scheme.

Instances For

The global section functor of an affine scheme.

Instances For

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

Instances For
def AlgebraicGeometry.IsAffineOpen (U : TopologicalSpace.Opens X.toPresheafedSpace) :

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

Instances For

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

Instances For
def AlgebraicGeometry.IsAffineOpen.fromSpec {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) :
AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj ())) X

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

Instances For
theorem AlgebraicGeometry.IsAffineOpen.fromSpec_range {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) :
Set.range .base = U
theorem AlgebraicGeometry.IsAffineOpen.fromSpec_image_top {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) :
(IsOpenMap.functor (_ : IsOpenMap .base)).obj = U
theorem AlgebraicGeometry.IsAffineOpen.isCompact {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) :
theorem AlgebraicGeometry.IsAffineOpen.imageIsOpenImmersion {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (f : X Y) :
theorem AlgebraicGeometry.IsAffineOpen.fromSpec_base_preimage {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) :
().obj U =
theorem AlgebraicGeometry.Scheme.Spec_map_presheaf_map_eqToHom {U : TopologicalSpace.Opens X.toPresheafedSpace} {V : TopologicalSpace.Opens X.toPresheafedSpace} (h : U = V) (W : (TopologicalSpace.Opens (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj ()))).toPresheafedSpace)ᵒᵖ) :
(AlgebraicGeometry.Scheme.Spec.map (X.presheaf.map ().op).op).val.c.app W = CategoryTheory.eqToHom (_ : (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj ()))).presheaf.obj W = ((AlgebraicGeometry.Scheme.Spec.map (X.presheaf.map ().op).op).val.base _* (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj ()))).presheaf).obj W)
theorem AlgebraicGeometry.IsAffineOpen.SpecΓIdentity_hom_app_fromSpec {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) :
CategoryTheory.CategoryStruct.comp (.app (X.presheaf.obj ())) (.c.app ()) = (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj ()))).presheaf.map (CategoryTheory.eqToHom (_ : ().obj U = )).op
theorem AlgebraicGeometry.IsAffineOpen.fromSpec_app_eq_apply {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (x : ().obj (X.presheaf.obj ())) :
↑(.c.app ()) x = ↑((AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj ()))).presheaf.map (CategoryTheory.eqToHom (_ : = Opposite.op (().obj U)))) (↑(AlgebraicGeometry.toSpecΓ (X.presheaf.obj ())) x)
theorem AlgebraicGeometry.IsAffineOpen.fromSpec_app_eq {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) :
.c.app () = CategoryTheory.CategoryStruct.comp (.app (X.presheaf.obj ())) ((AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj ()))).presheaf.map (CategoryTheory.eqToHom (_ : ().obj U = )).op)
theorem AlgebraicGeometry.IsAffineOpen.basicOpenIsAffine {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (f : ↑(X.presheaf.obj ())) :
theorem AlgebraicGeometry.IsAffineOpen.exists_basicOpen_le {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) {V : TopologicalSpace.Opens X.toPresheafedSpace} (x : { x // x V }) (h : x U) :
f,
instance AlgebraicGeometry.algebra_section_section_basicOpen {U : TopologicalSpace.Opens X.toPresheafedSpace} (f : ↑(X.presheaf.obj ())) :
Algebra ↑(X.presheaf.obj ()) ↑(X.presheaf.obj ())
theorem AlgebraicGeometry.IsAffineOpen.opens_map_fromSpec_basicOpen {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (f : ↑(X.presheaf.obj ())) :
().obj () = AlgebraicGeometry.RingedSpace.basicOpen (.obj (.obj (X.presheaf.obj ()))).unop (↑(.app (X.presheaf.obj ())) f)
def AlgebraicGeometry.basicOpenSectionsToAffine {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (f : ↑(X.presheaf.obj ())) :
X.presheaf.obj () (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj ()))).presheaf.obj (Opposite.op (AlgebraicGeometry.Scheme.basicOpen (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj ()))) (↑(.app (X.presheaf.obj ())) f)))

The canonical map Γ(𝒪ₓ, D(f)) ⟶ Γ(Spec 𝒪ₓ(U), D(Spec_Γ_identity.inv f)) This is an isomorphism, as witnessed by an is_iso instance.

Instances For
instance AlgebraicGeometry.basicOpenSectionsToAffine_isIso {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (f : ↑(X.presheaf.obj ())) :
theorem AlgebraicGeometry.isLocalization_basicOpen {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (f : ↑(X.presheaf.obj ())) :
IsLocalization.Away f ↑(X.presheaf.obj ())
instance AlgebraicGeometry.isLocalization_away_of_isAffine (r : ↑(X.presheaf.obj ())) :
IsLocalization.Away r ↑(X.presheaf.obj ())
theorem AlgebraicGeometry.isLocalization_of_eq_basicOpen {U : TopologicalSpace.Opens X.toPresheafedSpace} {V : TopologicalSpace.Opens X.toPresheafedSpace} (i : V U) (hU : ) (r : ↑(X.presheaf.obj ())) (e : ) :
IsLocalization.Away r ↑(X.presheaf.obj ())
instance AlgebraicGeometry.ΓRestrictAlgebra {Y : TopCat} {f : Y X.toPresheafedSpace} (hf : ) :
Algebra ↑() ↑()
theorem AlgebraicGeometry.basicOpen_basicOpen_is_basicOpen {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (f : ↑(X.presheaf.obj ())) (g : ↑(X.presheaf.obj ())) :
theorem AlgebraicGeometry.exists_basicOpen_le_affine_inter {U : TopologicalSpace.Opens X.toPresheafedSpace} {V : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (hV : ) (x : X.toPresheafedSpace) (hx : x U V) :
f g,
noncomputable def AlgebraicGeometry.IsAffineOpen.primeIdealOf {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (x : { x // x U }) :
PrimeSpectrum ↑(X.presheaf.obj ())

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

Instances For
theorem AlgebraicGeometry.IsAffineOpen.fromSpec_primeIdealOf {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (x : { x // x U }) :
.base () = x
theorem AlgebraicGeometry.IsAffineOpen.isLocalization_stalk_aux (U : TopologicalSpace.Opens X.toPresheafedSpace) :
(CategoryTheory.inv (.app ())).val.c.app () = CategoryTheory.CategoryStruct.comp (X.presheaf.map (Opposite.op (CategoryTheory.eqToHom (_ : (Opposite.op (().obj )).unop = (().op.obj ()).unop)))) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.toSpecΓ (X.presheaf.obj (Opposite.op (().obj )))) ((AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj (Opposite.op (().obj ))))).presheaf.map (Opposite.op (CategoryTheory.eqToHom (_ : ((TopologicalSpace.Opens.map (CategoryTheory.inv (.app ())).val.base).op.obj ()).unop = ().unop)))))
theorem AlgebraicGeometry.IsAffineOpen.isLocalization_stalk_aux' {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (y : PrimeSpectrum ↑(X.presheaf.obj ())) (hy : .base y U) :
CategoryTheory.CategoryStruct.comp (.c.app ()) (TopCat.Presheaf.germ (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj ()))).presheaf { val := y, property := hy }) = AlgebraicGeometry.StructureSheaf.toStalk (↑(X.presheaf.obj ())) y
theorem AlgebraicGeometry.IsAffineOpen.isLocalization_stalk' {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (y : PrimeSpectrum ↑(X.presheaf.obj ())) (hy : .base y U) :
IsLocalization.AtPrime (↑(TopCat.Presheaf.stalk X.presheaf (.base y))) y.asIdeal
theorem AlgebraicGeometry.IsAffineOpen.isLocalization_stalk {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (x : { x // x U }) :
IsLocalization.AtPrime (↑(TopCat.Presheaf.stalk X.presheaf x)) ().asIdeal
@[simp]
theorem AlgebraicGeometry.Scheme.affineBasicOpen_coe {U : } (f : ↑(X.presheaf.obj ())) :
def AlgebraicGeometry.Scheme.affineBasicOpen {U : } (f : ↑(X.presheaf.obj ())) :

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

Instances For
@[simp]
theorem AlgebraicGeometry.IsAffineOpen.basicOpen_fromSpec_app {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (f : ↑(X.presheaf.obj ())) :
AlgebraicGeometry.Scheme.basicOpen (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj ()))) (↑(.c.app ()) f) =
theorem AlgebraicGeometry.IsAffineOpen.fromSpec_map_basicOpen {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (f : ↑(X.presheaf.obj ())) :
().obj () =
theorem AlgebraicGeometry.IsAffineOpen.basicOpen_union_eq_self_iff {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (s : Set ↑(X.presheaf.obj ())) :
⨆ (f : s), = U
theorem AlgebraicGeometry.IsAffineOpen.self_le_basicOpen_union_iff {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) (s : Set ↑(X.presheaf.obj ())) :
U ⨆ (f : s),
theorem AlgebraicGeometry.of_affine_open_cover (V : ) (S : ) {P : } (hP₁ : (U : ) → (f : ↑(X.presheaf.obj ())) → P U) (hP₂ : (U : ) → (s : Finset ↑(X.presheaf.obj ())) → = ((f : { x // x s }) → ) → 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].