mathlib3 documentation

algebraic_geometry.Gamma_Spec_adjunction

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 #

algebraic_geometry.identity_to_Γ_Spec : The natural transformation 𝟭 _ ⟶ Γ ⋙ Spec.
algebraic_geometry.Γ_Spec.LocallyRingedSpace_adjunction : The adjunction Γ ⊣ Spec from CommRingᵒᵖ to LocallyRingedSpace.
algebraic_geometry.Γ_Spec.adjunction : The adjunction Γ ⊣ Spec from CommRingᵒᵖ to Scheme.

noncomputable def algebraic_geometry.LocallyRingedSpace.Γ_to_stalk (X : algebraic_geometry.LocallyRingedSpace) (x : ↥X) :

algebraic_geometry.LocallyRingedSpace.Γ.obj (opposite.op X) ⟶ X.to_SheafedSpace.to_PresheafedSpace.presheaf.stalk x

The map from the global sections to a stalk.

Equations

X.Γ_to_stalk x = X.to_SheafedSpace.to_PresheafedSpace.presheaf.germ ⟨x, trivial⟩

noncomputable def algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_fun (X : algebraic_geometry.LocallyRingedSpace) :

↥X → prime_spectrum ↥(algebraic_geometry.LocallyRingedSpace.Γ.obj (opposite.op X))

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

Equations

X.to_Γ_Spec_fun = λ (x : ↥X), ⇑(prime_spectrum.comap (X.Γ_to_stalk x)) (local_ring.closed_point ↥(X.to_SheafedSpace.to_PresheafedSpace.presheaf.stalk x))

theorem algebraic_geometry.LocallyRingedSpace.not_mem_prime_iff_unit_in_stalk (X : algebraic_geometry.LocallyRingedSpace) (r : ↥(algebraic_geometry.LocallyRingedSpace.Γ.obj (opposite.op X))) (x : ↥X) :

r ∉ (X.to_Γ_Spec_fun x).as_ideal ↔ is_unit (⇑(X.Γ_to_stalk x) r)

theorem algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_preim_basic_open_eq (X : algebraic_geometry.LocallyRingedSpace) (r : ↥(algebraic_geometry.LocallyRingedSpace.Γ.obj (opposite.op X))) :

X.to_Γ_Spec_fun ⁻¹' (prime_spectrum.basic_open r).carrier = (X.to_RingedSpace.basic_open r).carrier

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

theorem algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_continuous (X : algebraic_geometry.LocallyRingedSpace) :

continuous X.to_Γ_Spec_fun

to_Γ_Spec_fun is continuous.

@[simp]

theorem algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_base_apply (X : algebraic_geometry.LocallyRingedSpace) (ᾰ : ↥X) :

⇑(X.to_Γ_Spec_base) ᾰ = X.to_Γ_Spec_fun ᾰ

noncomputable def algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_base (X : algebraic_geometry.LocallyRingedSpace) :

X.to_Top ⟶ algebraic_geometry.Spec.Top_obj (algebraic_geometry.LocallyRingedSpace.Γ.obj (opposite.op X))

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

Equations

X.to_Γ_Spec_base = {to_fun := X.to_Γ_Spec_fun, continuous_to_fun := _}

@[reducible]

noncomputable def algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_map_basic_open (X : algebraic_geometry.LocallyRingedSpace) (r : ↥(algebraic_geometry.LocallyRingedSpace.Γ.obj (opposite.op X))) :

topological_space.opens ↥X

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

theorem algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_map_basic_open_eq (X : algebraic_geometry.LocallyRingedSpace) (r : ↥(algebraic_geometry.LocallyRingedSpace.Γ.obj (opposite.op X))) :

X.to_Γ_Spec_map_basic_open r = X.to_RingedSpace.basic_open r

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

@[reducible]

noncomputable def algebraic_geometry.LocallyRingedSpace.to_to_Γ_Spec_map_basic_open (X : algebraic_geometry.LocallyRingedSpace) (r : ↥(algebraic_geometry.LocallyRingedSpace.Γ.obj (opposite.op X))) :

X.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op ⊤) ⟶ X.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op (X.to_Γ_Spec_map_basic_open r))

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

theorem algebraic_geometry.LocallyRingedSpace.is_unit_res_to_Γ_Spec_map_basic_open (X : algebraic_geometry.LocallyRingedSpace) (r : ↥(algebraic_geometry.LocallyRingedSpace.Γ.obj (opposite.op X))) :

is_unit (⇑(X.to_to_Γ_Spec_map_basic_open r) r)

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

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

Equations

X.to_Γ_Spec_c_app r = is_localization.away.lift r _

Characterization of the sheaf hom on basic opens, direction ← (next lemma) is used at various places, but → is not used in this file.

theorem algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_c_app_spec (X : algebraic_geometry.LocallyRingedSpace) (r : ↥(algebraic_geometry.LocallyRingedSpace.Γ.obj (opposite.op X))) :

algebraic_geometry.structure_sheaf.to_open ↥(algebraic_geometry.LocallyRingedSpace.Γ.obj (opposite.op X)) (prime_spectrum.basic_open r) ≫ X.to_Γ_Spec_c_app r = X.to_to_Γ_Spec_map_basic_open r

The sheaf hom on all basic opens, commuting with restrictions.

Equations

X.to_Γ_Spec_c_basic_opens = {app := λ (r : (category_theory.induced_category (topological_space.opens (prime_spectrum ↥(algebraic_geometry.LocallyRingedSpace.Γ.obj (opposite.op X)))) prime_spectrum.basic_open)ᵒᵖ), X.to_Γ_Spec_c_app (opposite.unop r), naturality' := _}

noncomputable def algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_SheafedSpace (X : algebraic_geometry.LocallyRingedSpace) :

X.to_SheafedSpace ⟶ algebraic_geometry.Spec.to_SheafedSpace.obj (opposite.op (algebraic_geometry.LocallyRingedSpace.Γ.obj (opposite.op X)))

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

Equations

X.to_Γ_Spec_SheafedSpace = {base := X.to_Γ_Spec_base, c := ⇑(Top.sheaf.restrict_hom_equiv_hom (algebraic_geometry.Spec.structure_sheaf ↥(algebraic_geometry.LocallyRingedSpace.Γ.obj (opposite.op X))).val ((Top.sheaf.pushforward X.to_Γ_Spec_base).obj X.𝒪) _) X.to_Γ_Spec_c_basic_opens}

@[simp]

theorem algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_SheafedSpace_c (X : algebraic_geometry.LocallyRingedSpace) :

X.to_Γ_Spec_SheafedSpace.c = ⇑(Top.sheaf.restrict_hom_equiv_hom (algebraic_geometry.Spec.structure_sheaf ↥(algebraic_geometry.LocallyRingedSpace.Γ.obj (opposite.op X))).val ((Top.sheaf.pushforward X.to_Γ_Spec_base).obj X.𝒪) _) X.to_Γ_Spec_c_basic_opens

@[simp]

theorem algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_SheafedSpace_base (X : algebraic_geometry.LocallyRingedSpace) :

X.to_Γ_Spec_SheafedSpace.base = X.to_Γ_Spec_base

theorem algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_SheafedSpace_app_eq (X : algebraic_geometry.LocallyRingedSpace) (r : ↥(algebraic_geometry.LocallyRingedSpace.Γ.obj (opposite.op X))) :

X.to_Γ_Spec_SheafedSpace.c.app (opposite.op (prime_spectrum.basic_open r)) = X.to_Γ_Spec_c_app r

theorem algebraic_geometry.LocallyRingedSpace.to_stalk_stalk_map_to_Γ_Spec (X : algebraic_geometry.LocallyRingedSpace) (x : ↥X) :

algebraic_geometry.structure_sheaf.to_stalk ↥(opposite.unop (opposite.op (algebraic_geometry.LocallyRingedSpace.Γ.obj (opposite.op X)))) (⇑(X.to_Γ_Spec_SheafedSpace.base) x) ≫ algebraic_geometry.PresheafedSpace.stalk_map X.to_Γ_Spec_SheafedSpace x = X.Γ_to_stalk x

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

@[simp]

theorem algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_val_base (X : algebraic_geometry.LocallyRingedSpace) :

X.to_Γ_Spec.val.base = X.to_Γ_Spec_base

noncomputable def algebraic_geometry.LocallyRingedSpace.to_Γ_Spec (X : algebraic_geometry.LocallyRingedSpace) :

X ⟶ algebraic_geometry.Spec.LocallyRingedSpace_obj (algebraic_geometry.LocallyRingedSpace.Γ.obj (opposite.op X))

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

Equations

X.to_Γ_Spec = {val := X.to_Γ_Spec_SheafedSpace, prop := _}

theorem algebraic_geometry.LocallyRingedSpace.comp_ring_hom_ext {X : algebraic_geometry.LocallyRingedSpace} {R : CommRing} {f : R ⟶ algebraic_geometry.LocallyRingedSpace.Γ.obj (opposite.op X)} {β : X ⟶ algebraic_geometry.Spec.LocallyRingedSpace_obj R} (w : X.to_Γ_Spec.val.base ≫ (algebraic_geometry.Spec.LocallyRingedSpace_map f).val.base = β.val.base) (h : ∀ (r : ↥R), f ≫ X.to_SheafedSpace.to_PresheafedSpace.presheaf.map (category_theory.hom_of_le le_top).op = algebraic_geometry.structure_sheaf.to_open ↥R (prime_spectrum.basic_open r) ≫ β.val.c.app (opposite.op (prime_spectrum.basic_open r))) :

X.to_Γ_Spec ≫ algebraic_geometry.Spec.LocallyRingedSpace_map f = β

theorem algebraic_geometry.LocallyRingedSpace.Γ_Spec_left_triangle (X : algebraic_geometry.LocallyRingedSpace) :

algebraic_geometry.to_Spec_Γ (algebraic_geometry.LocallyRingedSpace.Γ.obj (opposite.op X)) ≫ X.to_Γ_Spec.val.c.app (opposite.op ⊤) = 𝟙 (algebraic_geometry.LocallyRingedSpace.Γ.obj (opposite.op X))

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

noncomputable def algebraic_geometry.identity_to_Γ_Spec :

𝟭 algebraic_geometry.LocallyRingedSpace ⟶ algebraic_geometry.LocallyRingedSpace.Γ.right_op ⋙ algebraic_geometry.Spec.to_LocallyRingedSpace

The unit as a natural transformation.

Equations

algebraic_geometry.identity_to_Γ_Spec = {app := algebraic_geometry.LocallyRingedSpace.to_Γ_Spec, naturality' := algebraic_geometry.identity_to_Γ_Spec._proof_1}

Spec_Γ_identity is iso so these are mutually two-sided inverses.

@[simp]

theorem algebraic_geometry.Γ_Spec.LocallyRingedSpace_adjunction_counit :

algebraic_geometry.Γ_Spec.LocallyRingedSpace_adjunction.counit = category_theory.nat_trans.op algebraic_geometry.Spec_Γ_identity.inv

@[simp]

theorem algebraic_geometry.Γ_Spec.LocallyRingedSpace_adjunction_unit :

algebraic_geometry.Γ_Spec.LocallyRingedSpace_adjunction.unit = algebraic_geometry.identity_to_Γ_Spec

noncomputable def algebraic_geometry.Γ_Spec.LocallyRingedSpace_adjunction :

algebraic_geometry.LocallyRingedSpace.Γ.right_op ⊣ algebraic_geometry.Spec.to_LocallyRingedSpace

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

Equations

algebraic_geometry.Γ_Spec.LocallyRingedSpace_adjunction = category_theory.adjunction.mk_of_unit_counit {unit := algebraic_geometry.identity_to_Γ_Spec, counit := (category_theory.nat_iso.op algebraic_geometry.Spec_Γ_identity).inv, left_triangle' := algebraic_geometry.Γ_Spec.LocallyRingedSpace_adjunction._proof_1, right_triangle' := algebraic_geometry.Γ_Spec.LocallyRingedSpace_adjunction._proof_2}

noncomputable def algebraic_geometry.Γ_Spec.adjunction :

algebraic_geometry.Scheme.Γ.right_op ⊣ algebraic_geometry.Scheme.Spec

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

Equations

algebraic_geometry.Γ_Spec.adjunction = category_theory.adjunction.restrict_fully_faithful algebraic_geometry.Scheme.forget_to_LocallyRingedSpace (𝟭 CommRing ᵒᵖ) algebraic_geometry.Γ_Spec.LocallyRingedSpace_adjunction (category_theory.nat_iso.of_components (λ (X : algebraic_geometry.Scheme), category_theory.iso.refl ((algebraic_geometry.Scheme.forget_to_LocallyRingedSpace ⋙ algebraic_geometry.LocallyRingedSpace.Γ.right_op).obj X)) algebraic_geometry.Γ_Spec.adjunction._proof_1) (category_theory.nat_iso.of_components (λ (X : CommRing ᵒᵖ), category_theory.iso.refl ((𝟭 CommRing ᵒᵖ ⋙ algebraic_geometry.Spec.to_LocallyRingedSpace).obj X)) algebraic_geometry.Γ_Spec.adjunction._proof_2)

theorem algebraic_geometry.Γ_Spec.adjunction_hom_equiv_apply {X : algebraic_geometry.Scheme} {R : CommRing ᵒᵖ} (f : opposite.op (algebraic_geometry.Scheme.Γ.obj (opposite.op X)) ⟶ R) :

⇑(algebraic_geometry.Γ_Spec.adjunction.hom_equiv X R) f = ⇑(algebraic_geometry.Γ_Spec.LocallyRingedSpace_adjunction.hom_equiv X.to_LocallyRingedSpace R) f

theorem algebraic_geometry.Γ_Spec.adjunction_hom_equiv (X : algebraic_geometry.Scheme) (R : CommRing ᵒᵖ) :

algebraic_geometry.Γ_Spec.adjunction.hom_equiv X R = algebraic_geometry.Γ_Spec.LocallyRingedSpace_adjunction.hom_equiv X.to_LocallyRingedSpace R

theorem algebraic_geometry.Γ_Spec.adjunction_hom_equiv_symm_apply {X : algebraic_geometry.Scheme} {R : CommRing ᵒᵖ} (f : X ⟶ algebraic_geometry.Scheme.Spec.obj R) :

⇑((algebraic_geometry.Γ_Spec.adjunction.hom_equiv X R).symm) f = ⇑((algebraic_geometry.Γ_Spec.LocallyRingedSpace_adjunction.hom_equiv X.to_LocallyRingedSpace R).symm) f

@[simp]

theorem algebraic_geometry.Γ_Spec.adjunction_counit_app {R : CommRing ᵒᵖ} :

algebraic_geometry.Γ_Spec.adjunction.counit.app R = algebraic_geometry.Γ_Spec.LocallyRingedSpace_adjunction.counit.app R

@[simp]

theorem algebraic_geometry.Γ_Spec.adjunction_unit_app {X : algebraic_geometry.Scheme} :

algebraic_geometry.Γ_Spec.adjunction.unit.app X = algebraic_geometry.Γ_Spec.LocallyRingedSpace_adjunction.unit.app X.to_LocallyRingedSpace

@[protected, instance]

def algebraic_geometry.Γ_Spec.is_iso_LocallyRingedSpace_adjunction_counit :

category_theory.is_iso algebraic_geometry.Γ_Spec.LocallyRingedSpace_adjunction.counit

@[protected, instance]

def algebraic_geometry.Γ_Spec.is_iso_adjunction_counit :

category_theory.is_iso algebraic_geometry.Γ_Spec.adjunction.counit

Immediate consequences of the adjunction.

@[protected, instance]

noncomputable def algebraic_geometry.Spec.to_LocallyRingedSpace.category_theory.limits.preserves_limits :

category_theory.limits.preserves_limits algebraic_geometry.Spec.to_LocallyRingedSpace

Spec preserves limits.

Equations

algebraic_geometry.Spec.to_LocallyRingedSpace.category_theory.limits.preserves_limits = algebraic_geometry.Γ_Spec.LocallyRingedSpace_adjunction.right_adjoint_preserves_limits

@[protected, instance]

noncomputable def algebraic_geometry.Spec.preserves_limits :

category_theory.limits.preserves_limits algebraic_geometry.Scheme.Spec

Equations

algebraic_geometry.Spec.preserves_limits = algebraic_geometry.Γ_Spec.adjunction.right_adjoint_preserves_limits

@[protected, instance]

noncomputable def algebraic_geometry.Spec.to_LocallyRingedSpace.category_theory.full :

category_theory.full algebraic_geometry.Spec.to_LocallyRingedSpace

Spec is a full functor.

Equations

algebraic_geometry.Spec.to_LocallyRingedSpace.category_theory.full = category_theory.R_full_of_counit_is_iso algebraic_geometry.Γ_Spec.LocallyRingedSpace_adjunction

@[protected, instance]

noncomputable def algebraic_geometry.Spec.full :

category_theory.full algebraic_geometry.Scheme.Spec

Equations

algebraic_geometry.Spec.full = category_theory.R_full_of_counit_is_iso algebraic_geometry.Γ_Spec.adjunction

@[protected, instance]

def algebraic_geometry.Spec.to_LocallyRingedSpace.category_theory.faithful :

category_theory.faithful algebraic_geometry.Spec.to_LocallyRingedSpace

Spec is a faithful functor.

@[protected, instance]

def algebraic_geometry.Spec.faithful :

category_theory.faithful algebraic_geometry.Scheme.Spec

@[protected, instance]

noncomputable def algebraic_geometry.Spec.to_LocallyRingedSpace.category_theory.is_right_adjoint :

category_theory.is_right_adjoint algebraic_geometry.Spec.to_LocallyRingedSpace

Equations

algebraic_geometry.Spec.to_LocallyRingedSpace.category_theory.is_right_adjoint = {left := algebraic_geometry.LocallyRingedSpace.Γ.right_op, adj := algebraic_geometry.Γ_Spec.LocallyRingedSpace_adjunction}

@[protected, instance]

noncomputable def algebraic_geometry.Scheme.Spec.category_theory.is_right_adjoint :

category_theory.is_right_adjoint algebraic_geometry.Scheme.Spec

Equations

algebraic_geometry.Scheme.Spec.category_theory.is_right_adjoint = {left := algebraic_geometry.Scheme.Γ.right_op, adj := algebraic_geometry.Γ_Spec.adjunction}

@[protected, instance]

noncomputable def algebraic_geometry.Spec.to_LocallyRingedSpace.category_theory.reflective :

category_theory.reflective algebraic_geometry.Spec.to_LocallyRingedSpace

Equations

algebraic_geometry.Spec.to_LocallyRingedSpace.category_theory.reflective = category_theory.reflective.mk

@[protected, instance]

noncomputable def algebraic_geometry.Spec.reflective :

category_theory.reflective algebraic_geometry.Scheme.Spec

Equations

algebraic_geometry.Spec.reflective = category_theory.reflective.mk