mathlib documentation

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 #

@[nolint]
structure algebraic_geometry.LocallyRingedSpace  :
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 morphims induced on stalks are local ring homomorphisms.

The underlying topological space 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

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

The identity morphism on a locally ringed space.

Equations

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