mathlib3 documentation

algebraic_geometry.Spec

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

The adjunction Γ ⊣ Spec is constructed in algebraic_geometry/Gamma_Spec_adjunction.lean.

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

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

Equations

The counit (Spec_Γ_identity.inv.op) of the adjunction Γ ⊣ Spec is an isomorphism.

Equations

For an algebra f : R →+* S, this is the ring homomorphism S →+* (f∗ 𝒪ₛ)ₚ for a p : Spec R. This is shown to be the localization at p in is_localized_module_to_pushforward_stalk_alg_hom.

Equations