mathlib documentation

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 #

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

Equations