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 IsLocalHom on the stalk maps).

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.

@[reducible, inline]

An alias for toSheafedSpace, 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

The structure sheaf of a locally ringed space.

Equations

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

theorem AlgebraicGeometry.LocallyRingedSpace.Hom.ext {X Y : LocallyRingedSpace} {x y : X.Hom Y} (base : x.base = y.base) (c : x.c y.c) :
x = y
@[reducible, inline]

A morphism of locally ringed spaces as a morphism of sheafed spaces.

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

The category of locally ringed spaces.

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

The forgetful functor from LocallyRingedSpace to SheafedSpace CommRing.

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

The canonical map X ⟶ Spec Γ(X, ⊤). This is the unit of the Γ-Spec adjunction.

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

Equations

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

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

Equations

The canonical map from the restriction to the subspace.

Equations

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

Equations

The empty locally ringed space.

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

The canonical map from the empty locally ringed space.

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

For an open embedding f : U ⟶ X and a point x : U, we get an isomorphism between the stalk of X at f x and the stalk of the restriction of X along f at t x.

Equations