feat(*): Prerequisites for the Spec gamma adjunction (#11209)

Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

Author: erdOne

src/algebraic_geometry/Scheme.lean

@@ -53,6 +53,9 @@ protected abbreviation sheaf (X : Scheme) := X.to_SheafedSpace.sheaf
 def forget_to_LocallyRingedSpace : Scheme ⥤ LocallyRingedSpace :=
   induced_functor _
 
+@[simp] lemma forget_to_LocallyRingedSpace_preimage {X Y : Scheme} (f : X ⟶ Y) :
+  Scheme.forget_to_LocallyRingedSpace.preimage f = f := rfl
+
 /-- The forgetful functor from `Scheme` to `Top`. -/
 @[simps]
 def forget_to_Top : Scheme ⥤ Top :=

src/algebraic_geometry/Spec.lean

@@ -6,6 +6,8 @@ Authors: Scott Morrison, Justus Springer
 import algebraic_geometry.locally_ringed_space
 import algebraic_geometry.structure_sheaf
 import data.equiv.transfer_instance
+import topology.sheaves.sheaf_condition.sites
+import topology.sheaves.functors
 
 /-!
 # $Spec$ as a functor to locally ringed spaces.
@@ -31,7 +33,6 @@ natural transformation in `Spec_Γ_naturality`, and realized as a natural isomor
 
 TODO: provide the unit, and prove the triangle identities.
 
-
 -/
 
 noncomputable theory
@@ -132,6 +133,20 @@ lemma Spec.to_PresheafedSpace_obj_op (R : CommRing) :
 lemma Spec.to_PresheafedSpace_map_op (R S : CommRing) (f : R ⟶ S) :
   Spec.to_PresheafedSpace.map f.op = Spec.SheafedSpace_map f := rfl
 
+lemma Spec.basic_open_hom_ext {X : RingedSpace} {R : CommRing} {α β : X ⟶ Spec.SheafedSpace_obj R}
+  (w : α.base = β.base) (h : ∀ r : R, let U := prime_spectrum.basic_open r in
+    (to_open R U ≫ α.c.app (op U)) ≫ X.presheaf.map (eq_to_hom (by rw w)) =
+     to_open R U ≫ β.c.app (op U)) : α = β :=
+begin
+  ext1,
+  { apply ((Top.sheaf.pushforward β.base).obj X.sheaf).hom_ext _
+      prime_spectrum.is_basis_basic_opens,
+    intro r,
+    apply (structure_sheaf.to_basic_open_epi R r).1,
+    simpa using h r },
+  exact w,
+end
+
 /--
 The spectrum of a commutative ring, as a `LocallyRingedSpace`.
 -/
@@ -209,7 +224,7 @@ Spec, as a contravariant functor from commutative rings to locally ringed spaces
 section Spec_Γ
 open algebraic_geometry.LocallyRingedSpace
 
-/-- The morphism `R ⟶ Γ(Spec R)` given by `algebraic_geometry.structure_sheaf.to_open`.  -/
+/-- The counit morphism `R ⟶ Γ(Spec R)` given by `algebraic_geometry.structure_sheaf.to_open`.  -/
 @[simps] def to_Spec_Γ (R : CommRing) : R ⟶ Γ.obj (op (Spec.to_LocallyRingedSpace.obj (op R))) :=
 structure_sheaf.to_open R ⊤
 
@@ -220,7 +235,7 @@ lemma Spec_Γ_naturality {R S : CommRing} (f : R ⟶ S) :
   f ≫ to_Spec_Γ S = to_Spec_Γ R ≫ Γ.map (Spec.to_LocallyRingedSpace.map f.op).op :=
 by { ext, symmetry, apply localization.local_ring_hom_to_map }
 
-/-- The counit of the adjunction `Γ ⊣ Spec` is an isomorphism. -/
+/-- The counit (`Spec_Γ_identity.inv.op`) of the adjunction `Γ ⊣ Spec` is an isomorphism. -/
 @[simps] def Spec_Γ_identity : Spec.to_LocallyRingedSpace.right_op ⋙ Γ ≅ 𝟭 _ :=
 iso.symm $ nat_iso.of_components (λ R, as_iso (to_Spec_Γ R) : _) (λ _ _, Spec_Γ_naturality)
 

src/algebraic_geometry/locally_ringed_space.lean

@@ -135,6 +135,13 @@ forget_to_SheafedSpace ⋙ SheafedSpace.forget _
 @[simp] lemma comp_val {X Y Z : LocallyRingedSpace} (f : X ⟶ Y) (g : Y ⟶ Z) :
   (f ≫ g).val = f.val ≫ g.val := rfl
 
+@[simp] lemma comp_val_c {X Y Z : LocallyRingedSpace} (f : X ⟶ Y) (g : Y ⟶ Z) :
+  (f ≫ g).val.c = g.val.c ≫ (presheaf.pushforward _ g.val.base).map f.val.c := rfl
+
+lemma comp_val_c_app {X Y Z : LocallyRingedSpace} (f : X ⟶ Y) (g : Y ⟶ Z) (U : (opens Z)ᵒᵖ) :
+  (f ≫ g).val.c.app U = g.val.c.app U ≫ f.val.c.app (op $ (opens.map g.val.base).obj U.unop) :=
+rfl
+
 /--
 Given two locally ringed spaces `X` and `Y`, an isomorphism between `X` and `Y` as _sheafed_
 spaces can be lifted to a morphism `X ⟶ Y` as locally ringed spaces.

src/algebraic_geometry/prime_spectrum/basic.lean

@@ -508,6 +508,10 @@ rfl
   comap (g.comp f) = (comap f).comp (comap g) :=
 rfl
 
+lemma comap_comp_apply (f : R →+* S) (g : S →+* S') (x : prime_spectrum S') :
+  prime_spectrum.comap (g.comp f) x = (prime_spectrum.comap f) (prime_spectrum.comap g x) :=
+rfl
+
 @[simp] lemma preimage_comap_zero_locus (s : set R) :
   (comap f) ⁻¹' (zero_locus s) = zero_locus (f '' s) :=
 preimage_comap_zero_locus_aux f s
@@ -770,8 +774,12 @@ def closed_point : prime_spectrum R :=
 
 variable {R}
 
-lemma local_hom_iff_comap_closed_point {S : Type v} [comm_ring S] [local_ring S]
-  {f : R →+* S} : is_local_ring_hom f ↔ prime_spectrum.comap f (closed_point S) = closed_point R :=
+lemma is_local_ring_hom_iff_comap_closed_point {S : Type v} [comm_ring S] [local_ring S]
+  (f : R →+* S) : is_local_ring_hom f ↔ prime_spectrum.comap f (closed_point S) = closed_point R :=
 by { rw [(local_hom_tfae f).out 0 4, subtype.ext_iff], refl }
 
+@[simp] lemma comap_closed_point {S : Type v} [comm_ring S] [local_ring S] (f : R →+* S)
+  [is_local_ring_hom f] : prime_spectrum.comap f (closed_point S) = closed_point R :=
+(is_local_ring_hom_iff_comap_closed_point f).mp infer_instance
+
 end local_ring

src/algebraic_geometry/ringed_space.lean

@@ -122,6 +122,11 @@ begin
   { intro h, exact ⟨x, h, rfl⟩ },
 end
 
+@[simp]
+lemma mem_top_basic_open (f : X.presheaf.obj (op ⊤)) (x : X) :
+  x ∈ X.basic_open f ↔ is_unit (X.presheaf.germ ⟨x, show x ∈ (⊤ : opens X), by trivial⟩ f) :=
+mem_basic_open X f ⟨x, _⟩
+
 lemma basic_open_subset {U : opens X} (f : X.presheaf.obj (op U)) : X.basic_open f ⊆ U :=
 by { rintros _ ⟨x, hx, rfl⟩, exact x.2 }
 

src/algebraic_geometry/stalks.lean

@@ -36,7 +36,7 @@ namespace algebraic_geometry.PresheafedSpace
 /--
 The stalk at `x` of a `PresheafedSpace`.
 -/
-def stalk (X : PresheafedSpace C) (x : X) : C := X.presheaf.stalk x
+abbreviation stalk (X : PresheafedSpace C) (x : X) : C := X.presheaf.stalk x
 
 /--
 A morphism of presheafed spaces induces a morphism of stalks.

src/algebraic_geometry/structure_sheaf.lean

@@ -812,6 +812,29 @@ def basic_open_iso (f : R) : (structure_sheaf R).1.obj (op (basic_open f)) ≅
   CommRing.of (localization.away f) :=
 (as_iso (show CommRing.of _ ⟶ _, from to_basic_open R f)).symm
 
+/-- Stalk of the structure sheaf at a prime p as localization of R -/
+lemma is_localization.to_stalk (p : prime_spectrum R) :
+  @is_localization.at_prime _ _ _ _ (to_stalk R p).to_algebra p.as_ideal _ :=
+begin
+  convert (is_localization.is_localization_iff_of_ring_equiv _ (stalk_iso R p).symm
+    .CommRing_iso_to_ring_equiv).mp localization.is_localization,
+  erw iso.eq_comp_inv,
+  exact to_stalk_comp_stalk_to_fiber_ring_hom R p,
+end
+
+/-- Sections of the structure sheaf of Spec R on a basic open as localization of R -/
+lemma is_localization.to_basic_open (r : R) :
+  @is_localization.away _ _ r _ _ (to_open R (basic_open r)).to_algebra :=
+begin
+  convert (is_localization.is_localization_iff_of_ring_equiv _ (basic_open_iso R r).symm
+    .CommRing_iso_to_ring_equiv).mp localization.is_localization,
+  exact (localization_to_basic_open R r).symm
+end
+
+instance to_basic_open_epi (r : R) : epi (to_open R (basic_open r)) :=
+⟨λ S f g h, by { refine is_localization.ring_hom_ext _ _,
+  swap 5, exact is_localization.to_basic_open R r, exact h }⟩
+
 @[elementwise] lemma to_global_factors : to_open R ⊤ =
   (CommRing.of_hom (algebra_map R (localization.away (1 : R)))) ≫ (to_basic_open R (1 : R)) ≫
   (structure_sheaf R).1.map (eq_to_hom (basic_open_one.symm)).op :=

src/category_theory/adjunction/basic.lean

@@ -99,6 +99,10 @@ section
 
 variables {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) {X' X : C} {Y Y' : D}
 
+lemma hom_equiv_id (X : C) : adj.hom_equiv X _ (𝟙 _) = adj.unit.app X := by simp
+
+lemma hom_equiv_symm_id (X : D) : (adj.hom_equiv _ X).symm (𝟙 _) = adj.counit.app X := by simp
+
 @[simp, priority 10] lemma hom_equiv_naturality_left_symm (f : X' ⟶ X) (g : X ⟶ G.obj Y) :
   (adj.hom_equiv X' Y).symm (f ≫ g) = F.map f ≫ (adj.hom_equiv X Y).symm g :=
 by rw [hom_equiv_counit, F.map_comp, assoc, adj.hom_equiv_counit.symm]

src/topology/sheaves/presheaf.lean

@@ -76,6 +76,11 @@ by rw h
     ℱ.map (begin dsimp [functor.op], apply quiver.hom.op, apply eq_to_hom, rw h, end) :=
 by simp [pushforward_eq]
 
+lemma pushforward_eq'_hom_app
+  {X Y : Top.{v}} {f g : X ⟶ Y} (h : f = g) (ℱ : X.presheaf C) (U) :
+  nat_trans.app (eq_to_hom (pushforward_eq' h ℱ)) U = ℱ.map (eq_to_hom (by rw h)) :=
+by simpa
+
 @[simp]
 lemma pushforward_eq_rfl {X Y : Top.{v}} (f : X ⟶ Y) (ℱ : X.presheaf C) (U) :
   (pushforward_eq (rfl : f = f) ℱ).hom.app (op U) = 𝟙 _ :=
@@ -223,11 +228,15 @@ def pushforward {X Y : Top.{v}} (f : X ⟶ Y) : X.presheaf C ⥤ Y.presheaf C :=
 { obj := pushforward_obj f,
   map := @pushforward_map _ _ X Y f }
 
+@[simp]
+lemma pushforward_map_app' {X Y : Top.{v}} (f : X ⟶ Y)
+  {ℱ 𝒢 : X.presheaf C} (α : ℱ ⟶ 𝒢) {U : (opens Y)ᵒᵖ} :
+  ((pushforward C f).map α).app U = α.app (op $ (opens.map f).obj U.unop) := rfl
+
 lemma id_pushforward {X : Top.{v}} : pushforward C (𝟙 X) = 𝟭 (X.presheaf C) :=
 begin
   apply category_theory.functor.ext,
-  { intros, ext U, have h := f.congr,
-    erw h (opens.op_map_id_obj U), simpa },
+  { intros, ext U, have h := f.congr, erw h (opens.op_map_id_obj U), simpa },
   { intros, apply pushforward.id_eq },
 end