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.
Specialize TopCat.Presheaf.germ_res_apply to sheaves of rings.
This is unfortunately needed because the results on presheaves are stated using the
HasForget.instFunLike instance, which is not reducibly equal to the actual coercion of
morphisms in CommRingCat to functions.
Specialize TopCat.Presheaf.germ_res_apply' to sheaves of rings.
This is unfortunately needed because the results on presheaves are stated using the
HasForget.instFunLike instance, which is not reducibly equal to the actual coercion of
morphisms in CommRingCat to functions.
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
- X.basicOpen f = { carrier := {x : ↑↑X.toPresheafedSpace | ∃ (hx : x ∈ U), IsUnit ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x hx)) f)}, is_open' := ⋯ }
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.