We define the adjunction
ΓSpec.adjunction : Γ ⊣ Spec by defining the unit (
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 #
AlgebraicGeometry.identityToΓSpec: The natural transformation
𝟭 _ ⟶ Γ ⋙ Spec.
AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction: The adjunction
Γ ⊣ Specfrom
AlgebraicGeometry.ΓSpec.adjunction: The adjunction
Γ ⊣ Specfrom
The map from the global sections to a stalk.
The canonical map from the underlying set to the prime spectrum of
The preimage of a basic open in
Spec Γ(X) under the unit is the basic
X defined by the same element (they are equal as sets).
The canonical (bundled) continuous map from the underlying topological
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 preimage is the basic open in
X defined by the same element
The map from the global sections
Γ(X) to the sections on the (preimage of) a basic open.
r is a unit as a section on the basic open defined by
Define the sheaf hom on individual basic opens for the unit.
Characterization of the sheaf hom on basic opens, direction ← (next lemma) is used at various places, but → is not used in this file.
The sheaf hom on all basic opens, commuting with restrictions.
The canonical morphism of sheafed spaces from
X to the spectrum of its global sections.
The map on stalks induced by the unit commutes with maps from
Spec Γ(X) and in
toSpecΓ _ is an isomorphism so these are mutually two-sided inverses.
SpecΓIdentity is iso so these are mutually two-sided inverses.
Γ ⊣ Spec from
Immediate consequences of the adjunction.