Documentation

Mathlib.AlgebraicGeometry.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.toTop, valued in the category of topological spaces,
  2. Spec.toSheafedSpace, valued in the category of sheafed spaces and
  3. Spec.toLocallyRingedSpace, valued in the category of locally ringed spaces.

Additionally, we provide Spec.toPresheafedSpace as a composition of Spec.toSheafedSpace with a forgetful functor.

The adjunction Γ ⊣ Spec is constructed in Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean.

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

Instances For

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

    Instances For

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

      Instances For

        The spectrum of a commutative ring, as a SheafedSpace.

        Instances For

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

          Instances For

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

            Instances For

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

              Instances For

                The spectrum of a commutative ring, as a LocallyRingedSpace.

                Instances For

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

                  Instances For

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

                    Instances For
                      @[simp]

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

                      Instances For

                        This is the AlgHom version of toPushforwardStalk, which is the map S ⟶ (f∗ 𝒪ₛ)ₚ for some algebra R ⟶ S and some p : Spec R.

                        Instances For