mathlib documentation


Ringed spaces #

We introduce the category of ringed spaces, as an alias for SheafedSpace CommRing.

The facts collected in this file are typically stated for locally ringed spaces, but never actually make use of the locality of stalks. See for instance

def algebraic_geometry.RingedSpace  :
Type (u_1+1)

The type of Ringed spaces, as an abbreviation for SheafedSpace CommRing.

If the germ of a section f is a unit in the stalk at x, then f must be a unit on some small neighborhood around x.

If a section f is a unit in each stalk, f must be a unit.

The basic open of a section f is the set of all points x, such that the germ of f at x is a unit.