# mathlibdocumentation

algebraic_geometry.locally_ringed_space

# 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).

## Future work

• Define the restriction along an open embedding
@[nolint]
structure algebraic_geometry.LocallyRingedSpace  :
Type (u_1+1)
• to_SheafedSpace :
• local_ring :

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 morphims induced on stalks are local ring homomorphisms.

The underlying topological space of a locally ringed space.

Equations

The structure sheaf of a locally ringed space.

Equations

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

Equations
@[instance]

Equations
@[ext]
theorem algebraic_geometry.LocallyRingedSpace.hom_ext (f g : X.hom Y) :
f.val = g.valf = g

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

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
@[instance]

The identity morphism on a locally ringed space.

Equations
@[simp]

@[instance]

Equations
@[simp]
theorem algebraic_geometry.LocallyRingedSpace.comp_val (f : X.hom Y) (g : Y.hom Z) :

Composition of morphisms of locally ringed spaces.

Equations
@[instance]

The category of locally ringed spaces.

Equations

The forgetful functor from LocallyRingedSpace to SheafedSpace CommRing.

Equations

The global sections, notated Gamma.

Equations
@[simp]