mathlib documentation


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 #

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


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


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


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

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

theorem algebraic_geometry.of_affine_open_cover {X : algebraic_geometry.Scheme} (V : (X.affine_opens)) (S : set (X.affine_opens)) {P : (X.affine_opens) → Prop} (hP₁ : ∀ (U : (X.affine_opens)) (f : (X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U.val))), P UP (X.affine_basic_open f)) (hP₂ : ∀ (U : (X.affine_opens)) (s : finset (X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))), ideal.span s = (∀ (f : s), P (X.affine_basic_open f.val))P U) (hS : (⋃ (i : S), i) = set.univ) (hS' : ∀ (U : S), P U) :

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