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.

Equations
Instances For

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

    Equations
    Instances For

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        The spectrum of a commutative ring, as a SheafedSpace.

        Equations
        Instances For

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

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

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

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

              Equations
              Instances For

                The spectrum of a commutative ring, as a LocallyRingedSpace.

                Equations
                Instances For

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

                  Equations
                  Instances For

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

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For

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

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        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.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        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.

                          Equations
                          Instances For