Documentation

Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Adjunction between Γ and Spec #

We define the adjunction ΓSpec.adjunction : Γ ⊣ Spec by defining the unit (toΓSpec, in multiple steps in this file) and counit (done in Spec.lean) and checking that they satisfy the left and right triangle identities. The constructions and proofs make use of maps and lemmas defined and proved in structure_sheaf.lean extensively.

Notice that since the adjunction is between contravariant functors, you get to choose one of the two categories to have arrows reversed, and it is equally valid to present the adjunction as Spec ⊣ Γ (Spec.to_LocallyRingedSpace.right_op ⊣ Γ), in which case the unit and the counit would switch to each other.

Main definition #

The canonical (bundled) continuous map from the underlying topological space of X to the prime spectrum of its global sections.

Instances For
    @[inline, reducible]

    The preimage in X of a basic open in Spec Γ(X) (as an open set).

    Instances For
      @[inline, reducible]

      The map from the global sections Γ(X) to the sections on the (preimage of) a basic open.

      Instances For

        The canonical morphism of sheafed spaces from X to the spectrum of its global sections.

        Instances For

          The adjunction Γ ⊣ Spec from CommRingᵒᵖ to LocallyRingedSpace.

          Instances For

            The adjunction Γ ⊣ Spec from CommRingᵒᵖ to Scheme.

            Instances For

              Immediate consequences of the adjunction.