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

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

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

Equations
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
noncomputable def algebraic_geometry.Spec.SheafedSpace_map {R S : CommRing} (f : R S) :

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]
theorem algebraic_geometry.Spec.basic_open_hom_ext {R : CommRing} {α β : X } (w : α.base = β.base) (h : ∀ (r : R), let U : := in ) :
α = β

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]
noncomputable def algebraic_geometry.Spec.LocallyRingedSpace_map {R S : CommRing} (f : R S) :

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]

The counit morphism R ⟶ Γ(Spec R) given by algebraic_geometry.structure_sheaf.to_open.

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

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

Equations

The stalk map of Spec M⁻¹R ⟶ Spec R is an iso for each p : Spec M⁻¹R.