mathlibdocumentation

algebraic_geometry.Spec

$Spec$ as a functor to locally ringed spaces. #

We define the functor $Spec$ from commutative rings to locally ringed spaces.

Implementation notes #

We define $Spec$ in three consecutive steps, each with more structure than the last:

1. Spec.to_Top, valued in the category of topological spaces,
2. Spec.to_SheafedSpace, valued in the category of sheafed spaces and
3. Spec.to_LocallyRingedSpace, valued in the category of locally ringed spaces.

Additionally, we provide Spec.to_PresheafedSpace as a composition of Spec.to_SheafedSpace with a forgetful functor.

Future work #

Adjunction between Γ and Spec

The spectrum of a commutative ring, as a topological space.

Equations
@[simp]
theorem algebraic_geometry.Spec.Top_map_to_fun {R S : CommRing} (f : R S) (ᾰ : prime_spectrum S) :
def algebraic_geometry.Spec.Top_map {R S : CommRing} (f : R S) :

The induced map of a ring homomorphism on the ring spectra, as a morphism of topological spaces.

Equations
@[simp]
theorem algebraic_geometry.Spec.Top_map_comp {R S T : CommRing} (f : R S) (g : S T) :
@[simp]

The spectrum, as a contravariant functor from commutative rings to topological spaces.

Equations
@[simp]

The spectrum of a commutative ring, as a SheafedSpace.

Equations

The induced map of a ring homomorphism on the ring spectra, as a morphism of sheafed spaces.

Equations
@[simp]
@[simp]
@[simp]
theorem algebraic_geometry.Spec.SheafedSpace_map_comp {R S T : CommRing} (f : R S) (g : S T) :
@[simp]
@[simp]

Spec, as a contravariant functor from commutative rings to sheafed spaces.

Equations

Spec, as a contravariant functor from commutative rings to presheafed spaces.

Equations
@[simp]

The spectrum of a commutative ring, as a LocallyRingedSpace.

Equations

Under the isomorphisms stalk_iso, the map stalk_map (Spec.SheafedSpace_map f) p corresponds to the induced local ring homomorphism localization.local_ring_hom.

@[simp]

The induced map of a ring homomorphism on the prime spectra, as a morphism of locally ringed spaces.

Equations
@[simp]

Spec, as a contravariant functor from commutative rings to locally ringed spaces.

Equations
@[simp]