# Documentation

Mathlib.Geometry.RingedSpace.LocallyRingedSpace

# The category of locally ringed spaces #

We define (bundled) locally ringed spaces (as SheafedSpace CommRing along with the fact that the stalks are local rings), and morphisms between these (morphisms in SheafedSpace with is_local_ring_hom on the stalk maps).

structure AlgebraicGeometry.LocallyRingedSpaceextends :
Type (u_1 + 1)

A LocallyRingedSpace is a topological space equipped with a sheaf of commutative rings such that all the stalks are local rings.

A morphism of locally ringed spaces is a morphism of ringed spaces such that the morphisms induced on stalks are local ring homomorphisms.

Instances For

An alias for to_SheafedSpace, where the result type is a RingedSpace. This allows us to use dot-notation for the RingedSpace namespace.

Equations
• = X.toSheafedSpace
Instances For

The underlying topological space of a locally ringed space.

Equations
• = X.toPresheafedSpace
Instances For
Equations

The structure sheaf of a locally ringed space.

Equations
Instances For
theorem AlgebraicGeometry.LocallyRingedSpace.Hom.ext (val : x.val = y.val) :
x = y

A morphism of locally ringed spaces is a morphism of ringed spaces such that the morphisms induced on stalks are local ring homomorphisms.

• val : X.toSheafedSpace Y.toSheafedSpace

the underlying morphism between ringed spaces

• prop : ∀ (x : X.toPresheafedSpace),

the underlying morphism induces a local ring homomorphism on stalks

Instances For
theorem AlgebraicGeometry.LocallyRingedSpace.Hom.ext' {f : X Y} {g : X Y} (h : f.val = g.val) :
f = g

The stalk of a locally ringed space, just as a CommRing.

Equations
Instances For
Equations

A morphism of locally ringed spaces f : X ⟶ Y induces a local ring homomorphism from Y.stalk (f x) to X.stalk x for any x : X.

Equations
Instances For

The identity morphism on a locally ringed space.

Equations
• One or more equations did not get rendered due to their size.
Instances For

Composition of morphisms of locally ringed spaces.

Equations
• One or more equations did not get rendered due to their size.
Instances For

The category of locally ringed spaces.

Equations
@[simp]
@[simp]

The forgetful functor from LocallyRingedSpace to SheafedSpace CommRing.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
@[simp]

The forgetful functor from LocallyRingedSpace to Top.

Equations
Instances For
theorem AlgebraicGeometry.LocallyRingedSpace.comp_val_c_app (f : X Y) (g : Y Z) :
.val.c.app U = CategoryTheory.CategoryStruct.comp (g.val.c.app U) (f.val.c.app (Opposite.op ((TopologicalSpace.Opens.map g.val.base).obj U.unop)))
@[simp]
theorem AlgebraicGeometry.LocallyRingedSpace.homOfSheafedSpaceHomOfIsIso_val (f : X.toSheafedSpace Y.toSheafedSpace) :
def AlgebraicGeometry.LocallyRingedSpace.homOfSheafedSpaceHomOfIsIso (f : X.toSheafedSpace Y.toSheafedSpace) :
X Y

Given two locally ringed spaces X and Y, an isomorphism between X and Y as sheafed spaces can be lifted to a morphism X ⟶ Y as locally ringed spaces.

See also iso_of_SheafedSpace_iso.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def AlgebraicGeometry.LocallyRingedSpace.isoOfSheafedSpaceIso (f : X.toSheafedSpace Y.toSheafedSpace) :
X Y

Given two locally ringed spaces X and Y, an isomorphism between X and Y as sheafed spaces can be lifted to an isomorphism X ⟶ Y as locally ringed spaces.

This is related to the property that the functor forget_to_SheafedSpace reflects isomorphisms. In fact, it is slightly stronger as we do not require f to come from a morphism between locally ringed spaces.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Equations
@[simp]
theorem AlgebraicGeometry.LocallyRingedSpace.restrict_carrier {U : TopCat} (h : ) :
.toSheafedSpace.toPresheafedSpace = U
@[simp]
theorem AlgebraicGeometry.LocallyRingedSpace.restrict_presheaf_obj {U : TopCat} (h : ) (X : ) :
.toSheafedSpace.toPresheafedSpace.presheaf.obj X = X✝.presheaf.obj (Opposite.op ((IsOpenMap.functor (_ : )).obj X.unop))
@[simp]
theorem AlgebraicGeometry.LocallyRingedSpace.restrict_presheaf_map {U : TopCat} (h : ) :
∀ {X_1 Y : } (f_1 : X_1 Y), .toSheafedSpace.toPresheafedSpace.presheaf.map f_1 = X.presheaf.map ((IsOpenMap.functor (_ : )).map f_1.unop).op

The restriction of a locally ringed space along an open embedding.

Equations
• One or more equations did not get rendered due to their size.
Instances For

The canonical map from the restriction to the subspace.

Equations
• One or more equations did not get rendered due to their size.
Instances For

The restriction of a locally ringed space X to the top subspace is isomorphic to X itself.

Equations
Instances For

The global sections, notated Gamma.

Equations
Instances For
@[simp]
theorem AlgebraicGeometry.LocallyRingedSpace.Γ_obj :
= X.unop.presheaf.obj ()
@[simp]
theorem AlgebraicGeometry.LocallyRingedSpace.Γ_map (f : X Y) :
= f.unop.val.c.app ()
theorem AlgebraicGeometry.LocallyRingedSpace.preimage_basicOpen (f : X Y) (s : (Y.presheaf.obj ())) :
= AlgebraicGeometry.RingedSpace.basicOpen ((f.val.c.app { unop := U }) s)
instance AlgebraicGeometry.LocallyRingedSpace.component_nontrivial (U : TopologicalSpace.Opens X.toPresheafedSpace) [hU : Nonempty U] :
Nontrivial (X.presheaf.obj ())
Equations