# 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 #

• AlgebraicGeometry.identityToΓSpec : The natural transformation 𝟭 _ ⟶ Γ ⋙ Spec.
• AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction : The adjunction Γ ⊣ Spec from CommRingᵒᵖ to LocallyRingedSpace.
• AlgebraicGeometry.ΓSpec.adjunction : The adjunction Γ ⊣ Spec from CommRingᵒᵖ to Scheme.

The map from the global sections to a stalk.

Instances For

The canonical map from the underlying set to the prime spectrum of Γ(X).

Instances For

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

toΓSpecFun is continuous.

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

The preimage is the basic open in X defined by the same element r.

@[inline, reducible]
abbrev AlgebraicGeometry.LocallyRingedSpace.toToΓSpecMapBasicOpen (r : ) :
X.presheaf.obj () X.presheaf.obj ()

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

Instances For

r is a unit as a section on the basic open defined by r.

def AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp (r : ) :
.obj () X.presheaf.obj ()

Define the sheaf hom on individual basic opens for the unit.

Instances For
theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_iff (r : ) (f : .obj () X.presheaf.obj ()) :

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.

Instances For

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

Instances For

The map on stalks induced by the unit commutes with maps from Γ(X) to stalks (in Spec Γ(X) and in X).

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

Instances For
theorem AlgebraicGeometry.LocallyRingedSpace.comp_ring_hom_ext {R : CommRingCat} {f : } (w : = β.val.base) (h : ∀ (r : R), CategoryTheory.CategoryStruct.comp f (X.presheaf.map (CategoryTheory.homOfLE (_ : (TopologicalSpace.Opens.map β.val.base).obj () )).op) = CategoryTheory.CategoryStruct.comp () (β.val.c.app ())) :

toSpecΓ _ is an isomorphism so these are mutually two-sided inverses.

The unit as a natural transformation.

Instances For

SpecΓIdentity is iso so these are mutually two-sided inverses.

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

Instances For

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

Instances For
@[simp]