mathlib3 documentation

algebraic_geometry.properties

Basic properties of schemes #

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

We provide some basic properties of schemes

Main definition #

To show that a statement P holds for all open subsets of all schemes, it suffices to show that

  1. In any scheme X, if P holds for an open cover of U, then P holds for U.
  2. For an open immerison f : X ⟶ Y, if P holds for the entire space of X, then P holds for the image of f.
  3. P holds for the entire space of an affine scheme.
@[class]

A scheme X is integral if its carrier is nonempty, and 𝒪ₓ(U) is an integral domain for each U ≠ ∅.

Instances of this typeclass