mathlib3 documentation


Affine schemes #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.


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.