mathlib documentation

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.

In progress #

Adjunction between Γ and Spec: Currently, the counit of the adjunction is proven to be a natural transformation in Spec_Γ_naturality, and realized as a natural isomorphism in Spec_Γ_identity.

TODO: provide the unit, and prove the triangle identities.

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

Equations

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

Equations

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

Equations

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

Equations

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

Equations