AlgebraicGeometry.RingedSpace.isUnit_res_of_isUnit_germ
theorem AlgebraicGeometry.RingedSpace.isUnit_res_of_isUnit_germ :
∀ (X : AlgebraicGeometry.RingedSpace) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace)
(f : ↑(X.presheaf.obj (Opposite.op U))) (x : ↥U),
IsUnit ((X.presheaf.germ x) f) → ∃ V i, ∃ (_ : ↑x ∈ V), IsUnit ((X.presheaf.map i.op) f)
This theorem in Algebraic Geometry, specifically in the context of Ringed Spaces, asserts that if the germ of a section `f` under a presheaf is a unit in the stalk at a point `x`, then the section `f` itself must be a unit in some small neighborhood around `x` in the underlying topological space of the Ringed Space. Here, a "unit" refers to an element having a two-sided inverse in the monoid structure. The germ of a section represents a local piece or an "infinitesimal neighborhood" around the point, and the theorem essentially states a sort of local-to-global principle: if a property holds at the 'infinitesimal' or germ level, then it also holds in some 'small' neighborhood.
More concisely: If the germ of a section is a unit in the stalk of a Ringed Space at a point, then the section is a unit in some neighborhood of that point.
|
AlgebraicGeometry.RingedSpace.basicOpen_le
theorem AlgebraicGeometry.RingedSpace.basicOpen_le :
∀ (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace}
(f : ↑(X.presheaf.obj (Opposite.op U))), X.basicOpen f ≤ U
This theorem states that for any Ringed Space `X` and any open subset `U` of the underlying topological space of `X`, given a section `f` in the presheaf of `X` over `U`, the basic open set generated by `f` is a subset of `U`. In other words, the basic open set is the set of all points where the germ of `f` (i.e., its localization at a point) is a unit in the ring of all germs, and this set of points is guaranteed to be contained within `U`.
More concisely: Given a Ringed Space `X`, an open subset `U` of its underlying topological space, and a section `f` in the presheaf of `X` over `U`, the basic open set of `f` is contained in `U`.
|
AlgebraicGeometry.RingedSpace.mem_basicOpen
theorem AlgebraicGeometry.RingedSpace.mem_basicOpen :
∀ (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace}
(f : ↑(X.presheaf.obj (Opposite.op U))) (x : ↥U), ↑x ∈ X.basicOpen f ↔ IsUnit ((X.presheaf.germ x) f)
This theorem states that for any Ringed Space `X`, an open subset `U` of the topological space associated with `X`, a section `f` from the presheaf of `X` on the opposite of `U`, and a point `x` in `U`, the point `x` belongs to the basic open of `X` determined by `f` if and only if the germ of `f` at `x` is a unit in the stalk of the presheaf at `x`. In other words, a point `x` is in the set of all points where the germ of `f` is a unit (i.e., has an inverse) if and only if the germ of `f` at that point is indeed a unit.
More concisely: For any Ringed Space X, open subset U, section f over U, and point x in U, x lies in the basic open set of f if and only if the germ of f at x is a unit in the stalk of the presheaf at x.
|
AlgebraicGeometry.RingedSpace.isUnit_res_basicOpen
theorem AlgebraicGeometry.RingedSpace.isUnit_res_basicOpen :
∀ (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace}
(f : ↑(X.presheaf.obj (Opposite.op U))), IsUnit ((X.presheaf.map (CategoryTheory.homOfLE ⋯).op) f)
This theorem states that for any ringed space `X` and a section `f` of the presheaf associated with `X` over a topological open set `U` of `X`, the restriction of `f` to the basic open set of `f` is a unit. Here, a unit in a monoid is an element that has a two-sided inverse. The restriction is done via the map operation on the presheaf in line with the inequality morphism in the corresponding preorder category, hence ensuring the preservation of the section's structure under restriction.
More concisely: For any ringed space X and a section f of its presheaf over an open set U, the restriction of f to each basic open set is a unit in the corresponding stalk monoid.
|
AlgebraicGeometry.RingedSpace.isUnit_of_isUnit_germ
theorem AlgebraicGeometry.RingedSpace.isUnit_of_isUnit_germ :
∀ (X : AlgebraicGeometry.RingedSpace) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace)
(f : ↑(X.presheaf.obj (Opposite.op U))), (∀ (x : ↥U), IsUnit ((X.presheaf.germ x) f)) → IsUnit f
This theorem states that if a section `f` in an algebraic geometry ringed space `X` (over an open set `U` in the topological space underlying `X`) is a unit at each stalk (i.e., for every point `x` in `U`, the germ of `f` at `x` is a unit in the local ring), then the section `f` itself is a unit in the ring of sections. In other words, local invertibility (at each stalk) of a section in a ringed space implies its global invertibility. This theorem is a fundamental notion in the study of algebraic geometry and sheaf theory, relating the local properties of sections to their global properties.
More concisely: If a section in an algebraic geometry ringed space is a unit at each stalk, then it is a global unit in the ring of sections.
|