mathlib3 documentation


Adjunction between Γ and Spec #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 preimage of a basic open in Spec Γ(X) under the unit is the basic open in X defined by the same element (they are equal as sets).

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


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

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


Immediate consequences of the adjunction.