Ringed spaces #
We introduce the category of ringed spaces, as an alias for SheafedSpace CommRingCat
.
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 https://stacks.math.columbia.edu/tag/01HZ.
The type of Ringed spaces, as an abbreviation for SheafedSpace CommRingCat
.
Instances For
Equations
- AlgebraicGeometry.RingedSpace.instCoeSortType = { coe := fun (X : AlgebraicGeometry.RingedSpace) => ↑↑X.toPresheafedSpace }
If the germ of a section f
is zero in the stalk at x
, then f
is zero on some neighbourhood
around x
.
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.
Equations
Instances For
A variant of mem_basicOpen
with bundled x : U
.
The restriction of a section f
to the basic open of f
is a unit.
The zero locus of a set of sections s
over an open set U
is the closed set consisting of
the complement of U
and of all points of U
, where all elements of f
vanish.