# mathlibdocumentation

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

• algebraic_geometry.AffineScheme: The category of affine schemes.
• algebraic_geometry.is_affine: A scheme is affine if the canonical map X ⟶ Spec Γ(X) is an isomorphism.
• algebraic_geometry.Scheme.iso_Spec: The canonical isomorphism X ≅ Spec Γ(X) for an affine scheme.
• algebraic_geometry.AffineScheme.equiv_CommRing: The equivalence of categories AffineScheme ≌ CommRingᵒᵖ given by AffineScheme.Spec : CommRingᵒᵖ ⥤ AffineScheme and AffineScheme.Γ : AffineSchemeᵒᵖ ⥤ CommRing.
• algebraic_geometry.is_affine_open: An open subset of a scheme is affine if the open subscheme is affine.
• algebraic_geometry.is_affine_open.from_Spec: The immersion Spec 𝒪ₓ(U) ⟶ X for an affine U.
@[protected, instance]
@[nolint]
def algebraic_geometry.AffineScheme  :
Type (u_1+1)

The category of affine schemes

Equations
Instances for algebraic_geometry.AffineScheme
@[class]
structure algebraic_geometry.is_affine  :
Prop

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

Instances of this typeclass

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

Equations
@[simp]

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

Equations

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

Equations

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

Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]

The Spec functor into the category of affine schemes.

Equations
Instances for algebraic_geometry.AffineScheme.Spec
@[protected, instance]
@[simp]

The forgetful functor AffineScheme ⥤ Scheme.

Equations
Instances for algebraic_geometry.AffineScheme.forget_to_Scheme
@[simp]
noncomputable def algebraic_geometry.AffineScheme.Γ  :

The global section functor of an affine scheme.

Equations
Instances for algebraic_geometry.AffineScheme.Γ

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

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations

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

Equations

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

Equations
@[protected, instance]
@[protected, instance]

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

Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations

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

Equations
Instances for algebraic_geometry.basic_open_sections_to_affine
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]

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

Equations

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

Equations
@[simp]
theorem algebraic_geometry.of_affine_open_cover (V : (X.affine_opens)) (S : set (X.affine_opens)) {P : (X.affine_opens) → Prop} (hP₁ : ∀ (U : (X.affine_opens)) (f : , P UP (X.affine_basic_open f)) (hP₂ : ∀ (U : (X.affine_opens)) (s : , (∀ (f : s), P (X.affine_basic_open f.val))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 Vakil's "The rising sea".