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

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

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

Equations

The underlying topological space of a locally ringed space.

Equations
@[protected, instance]
Equations
@[protected, instance]

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
@[protected, instance]
Equations
@[ext]
theorem algebraic_geometry.LocallyRingedSpace.hom_ext (f g : X.hom Y) (w : f.val = g.val) :
f = g

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

Equations
noncomputable def algebraic_geometry.LocallyRingedSpace.stalk_map (f : X Y) (x : X) :
Y.stalk ((f.val.base) x) X.stalk x

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

The identity morphism on a locally ringed space.

Equations
@[protected, instance]
Equations
@[simp]
theorem algebraic_geometry.LocallyRingedSpace.comp_coe (f : X.hom Y) (g : Y.hom Z) :
def algebraic_geometry.LocallyRingedSpace.comp (f : X.hom Y) (g : Y.hom Z) :
X.hom Z

Composition of morphisms of locally ringed spaces.

Equations
@[protected, instance]

The category of locally ringed spaces.

Equations
@[simp]

The forgetful functor from LocallyRingedSpace to SheafedSpace CommRing.

Equations

The forgetful functor from LocallyRingedSpace to Top.

Equations
@[simp]
@[simp]
theorem algebraic_geometry.LocallyRingedSpace.comp_val (f : X Y) (g : Y Z) :
(f g).val = f.val g.val
@[simp]
theorem algebraic_geometry.LocallyRingedSpace.comp_val_c (f : X Y) (g : Y Z) :
(f g).val.c = g.val.c

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.

Equations
@[simp]

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

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

Equations

The canonical map from the restriction to the supspace.

Equations

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

Equations

The global sections, notated Gamma.

Equations
@[simp]
@[protected, instance]