mathlib documentation

algebraic_geometry.Spec

$Spec R$ as a `LocallyRingedSpace`

We bundle the structure_sheaf R construction for R : CommRing as a LocallyRingedSpace.

Future work

Make it a functor.

def algebraic_geometry.Spec.SheafedSpace :

CommRing → algebraic_geometry.SheafedSpace CommRing

Spec of a commutative ring, as a SheafedSpace.

Equations

algebraic_geometry.Spec.SheafedSpace R = {to_PresheafedSpace := {carrier := Top.of (prime_spectrum ↥R) prime_spectrum.zariski_topology, presheaf := (algebraic_geometry.structure_sheaf ↥R).presheaf}, sheaf_condition := (algebraic_geometry.structure_sheaf ↥R).sheaf_condition}

def algebraic_geometry.Spec.PresheafedSpace :

CommRing → algebraic_geometry.PresheafedSpace CommRing

Spec of a commutative ring, as a PresheafedSpace.

Equations

algebraic_geometry.Spec.PresheafedSpace R = (algebraic_geometry.Spec.SheafedSpace R).to_PresheafedSpace

def algebraic_geometry.Spec.LocallyRingedSpace :

CommRing → algebraic_geometry.LocallyRingedSpace

Spec of a commutative ring, as a LocallyRingedSpace.

Equations

algebraic_geometry.Spec.LocallyRingedSpace R = {to_SheafedSpace := {to_PresheafedSpace := (algebraic_geometry.Spec.SheafedSpace R).to_PresheafedSpace, sheaf_condition := (algebraic_geometry.Spec.SheafedSpace R).sheaf_condition}, local_ring := _}