feat(algebraic_geometry): Isomorphisms of presheafed space. (#10461)

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

src/algebraic_geometry/Spec.lean

@@ -103,7 +103,7 @@ end
 lemma Spec.SheafedSpace_map_comp {R S T : CommRing} (f : R ⟶ S) (g : S ⟶ T) :
   Spec.SheafedSpace_map (f ≫ g) = Spec.SheafedSpace_map g ≫ Spec.SheafedSpace_map f :=
 PresheafedSpace.ext _ _ (Spec.Top_map_comp f g) $ nat_trans.ext _ _ $ funext $ λ U,
-by { dsimp, rw category.comp_id, erw comap_comp f g, refl }
+by { dsimp, rw category_theory.functor.map_id, rw category.comp_id, erw comap_comp f g, refl }
 
 /--
 Spec, as a contravariant functor from commutative rings to sheafed spaces.

src/algebraic_geometry/presheafed_space.lean

@@ -68,7 +68,7 @@ structure hom (X Y : PresheafedSpace C) :=
 
 @[ext] lemma ext {X Y : PresheafedSpace C} (α β : hom X Y)
   (w : α.base = β.base)
-  (h : α.c ≫ eq_to_hom (by rw w) = β.c) :
+  (h : α.c ≫ (whisker_right (eq_to_hom (by rw w)) _) = β.c) :
   α = β :=
 begin
   cases α, cases β,
@@ -113,13 +113,32 @@ instance category_of_PresheafedSpaces : category (PresheafedSpace C) :=
 { hom := hom,
   id := id,
   comp := λ X Y Z f g, comp f g,
-  id_comp' := λ X Y f, by { ext1,
-    { rw comp_c, erw eq_to_hom_map, simp, apply comp_id }, apply id_comp },
-  comp_id' := λ X Y f, by { ext1,
-    { rw comp_c, erw congr_hom (presheaf.id_pushforward _) f.c,
-      simp, erw eq_to_hom_trans_assoc, simp }, apply comp_id },
-  assoc' := λ W X Y Z f g h, by { ext1,
-    repeat {rw comp_c}, simpa, refl } }
+  id_comp' := λ X Y f, begin
+    ext1,
+    { rw comp_c,
+      erw eq_to_hom_map,
+      simp only [eq_to_hom_refl, assoc, whisker_right_id'],
+      erw [comp_id, comp_id] },
+    apply id_comp
+  end,
+  comp_id' := λ X Y f, begin
+    ext1,
+    { rw comp_c,
+      erw congr_hom (presheaf.id_pushforward _) f.c,
+      simp only [comp_id, functor.id_map, eq_to_hom_refl, assoc, whisker_right_id'],
+      erw eq_to_hom_trans_assoc,
+      simp only [id_comp, eq_to_hom_refl],
+      erw comp_id },
+    apply comp_id
+  end,
+  assoc' := λ W X Y Z f g h, begin
+    ext1,
+    repeat {rw comp_c},
+    simp only [eq_to_hom_refl, assoc, functor.map_comp, whisker_right_id'],
+    erw comp_id,
+    congr,
+    refl
+  end }
 
 end
 
@@ -132,13 +151,19 @@ lemma id_c (X : PresheafedSpace C) :
   ((𝟙 X) : X ⟶ X).c = eq_to_hom (presheaf.pushforward.id_eq X.presheaf).symm := rfl
 
 @[simp] lemma id_c_app (X : PresheafedSpace C) (U) :
-  ((𝟙 X) : X ⟶ X).c.app U = eq_to_hom (by { induction U using opposite.rec, cases U, refl }) :=
+  ((𝟙 X) : X ⟶ X).c.app U = X.presheaf.map
+    (eq_to_hom (by { induction U using opposite.rec, cases U, refl })) :=
 by { induction U using opposite.rec, cases U, simp only [id_c], dsimp, simp, }
 
 @[simp] lemma comp_base {X Y Z : PresheafedSpace C} (f : X ⟶ Y) (g : Y ⟶ Z) :
   (f ≫ g).base = f.base ≫ g.base := rfl
 
-@[simp] lemma comp_c_app {X Y Z : PresheafedSpace C} (α : X ⟶ Y) (β : Y ⟶ Z) (U) :
+-- The `reassoc` attribute was added despite the LHS not being a composition of two homs,
+-- for the reasons explained in the docstring.
+/-- Sometimes rewriting with `comp_c_app` doesn't work because of dependent type issues.
+In that case, `erw comp_c_app_assoc` might make progress.
+The lemma `comp_c_app_assoc` is also better suited for rewrites in the opposite direction. -/
+@[reassoc, simp] lemma comp_c_app {X Y Z : PresheafedSpace C} (α : X ⟶ Y) (β : Y ⟶ Z) (U) :
   (α ≫ β).c.app U = (β.c).app U ≫ (α.c).app (op ((opens.map (β.base)).obj (unop U))) := rfl
 
 lemma congr_app {X Y : PresheafedSpace C} {α β : X ⟶ Y} (h : α = β) (U) :
@@ -156,6 +181,75 @@ def forget : PresheafedSpace C ⥤ Top :=
 
 end
 
+section iso
+
+variables {X Y : PresheafedSpace C}
+
+/--
+An isomorphism of PresheafedSpaces is a homeomorphism of the underlying space, and a
+natural transformation between the sheaves.
+-/
+@[simps hom inv]
+def iso_of_components (H : X.1 ≅ Y.1) (α : H.hom _* X.2 ≅ Y.2) : X ≅ Y :=
+{ hom := { base := H.hom, c := α.inv },
+  inv := { base := H.inv,
+    c := presheaf.to_pushforward_of_iso H α.hom },
+  hom_inv_id' := by { ext, { simp, erw category.id_comp, simpa }, simp },
+  inv_hom_id' :=
+  begin
+    ext x,
+    induction x using opposite.rec,
+    simp only [comp_c_app, whisker_right_app, presheaf.to_pushforward_of_iso_app,
+      nat_trans.comp_app, eq_to_hom_app, id_c_app, category.assoc],
+    erw [← α.hom.naturality],
+    have := nat_trans.congr_app (α.inv_hom_id) (op x),
+    cases x,
+    rw nat_trans.comp_app at this,
+    convert this,
+    { dsimp, simp },
+    { simp },
+    { simp }
+  end }
+
+/-- Isomorphic PresheafedSpaces have natural isomorphic presheaves. -/
+@[simps]
+def sheaf_iso_of_iso (H : X ≅ Y) : Y.2 ≅ H.hom.base _* X.2 :=
+{ hom := H.hom.c,
+  inv := presheaf.pushforward_to_of_iso ((forget _).map_iso H).symm H.inv.c,
+  hom_inv_id' :=
+  begin
+    ext U,
+    have := congr_app H.inv_hom_id U,
+    simp only [comp_c_app, id_c_app,
+      eq_to_hom_map, eq_to_hom_trans] at this,
+    generalize_proofs h at this,
+    simpa using congr_arg (λ f, f ≫ eq_to_hom h.symm) this,
+  end,
+  inv_hom_id' :=
+  begin
+    ext U,
+    simp only [presheaf.pushforward_to_of_iso_app, nat_trans.comp_app, category.assoc,
+      nat_trans.id_app, H.hom.c.naturality],
+    have := congr_app H.hom_inv_id ((opens.map H.hom.base).op.obj U),
+    generalize_proofs h at this,
+    simpa using congr_arg (λ f, f ≫ X.presheaf.map (eq_to_hom h.symm)) this
+  end }
+
+instance base_is_iso_of_iso (f : X ⟶ Y) [is_iso f] : is_iso f.base :=
+is_iso.of_iso ((forget _).map_iso (as_iso f))
+
+instance c_is_iso_of_iso (f : X ⟶ Y) [is_iso f] : is_iso f.c :=
+is_iso.of_iso (sheaf_iso_of_iso (as_iso f))
+
+/-- This could be used in conjunction with `category_theory.nat_iso.is_iso_of_is_iso_app`. -/
+lemma is_iso_of_components (f : X ⟶ Y) [is_iso f.base] [is_iso f.c] : is_iso f :=
+begin
+  convert is_iso.of_iso (iso_of_components (as_iso f.base) (as_iso f.c).symm),
+  ext, { simpa }, { simp },
+end
+
+end iso
+
 section restrict
 
 /--
@@ -249,9 +343,9 @@ def restrict_top_iso (X : PresheafedSpace C) :
 { hom := X.of_restrict _,
   inv := X.to_restrict_top,
   hom_inv_id' := ext _ _ (concrete_category.hom_ext _ _ $ λ ⟨x, _⟩, rfl) $
-    by { erw comp_c, rw X.of_restrict_top_c, simpa },
+    by { erw comp_c, rw X.of_restrict_top_c, ext, simp },
   inv_hom_id' := ext _ _ rfl $
-    by { erw comp_c, rw X.of_restrict_top_c, simpa } }
+    by { erw comp_c, rw X.of_restrict_top_c, ext, simpa [-eq_to_hom_refl] } }
 
 end restrict
 

src/algebraic_geometry/presheafed_space/has_colimits.lean

@@ -265,7 +265,7 @@ def colimit_cocone_is_colimit (F : J ⥤ PresheafedSpace C) : is_colimit (colimi
       dsimp,
       have w := congr_arg op (functor.congr_obj (congr_arg opens.map t) (unop U)),
       rw nat_trans.congr (limit.π (pushforward_diagram_to_colimit F).left_op j) w,
-      simpa }
+      simp }
   end, }
 
 /--

src/category_theory/limits/has_limits.lean

@@ -785,7 +785,7 @@ colimit.desc (E ⋙ F) ((colimit.cocone F).whisker E)
   colimit.ι (E ⋙ F) k ≫ colimit.pre F E = colimit.ι F (E.obj k) :=
 by { erw is_colimit.fac, refl, }
 
-@[simp] lemma colimit.pre_desc (c : cocone F) :
+@[simp, reassoc] lemma colimit.pre_desc (c : cocone F) :
   colimit.pre F E ≫ colimit.desc F c = colimit.desc (E ⋙ F) (c.whisker E) :=
 by ext; rw [←assoc, colimit.ι_pre]; simp
 

src/topology/category/Top/opens.lean

@@ -231,6 +231,15 @@ rfl
      eq_to_hom (congr_fun (congr_arg functor.obj (congr_arg map h.symm)) U) :=
 rfl
 
+/-- A homeomorphism of spaces gives an equivalence of categories of open sets. -/
+@[simps] def map_map_iso {X Y : Top.{u}} (H : X ≅ Y) : opens Y ≌ opens X :=
+{ functor := map H.hom,
+  inverse := map H.inv,
+  unit_iso := nat_iso.of_components (λ U, eq_to_iso (by simp [map, set.preimage_preimage]))
+    (by { intros _ _ _, simp }),
+  counit_iso := nat_iso.of_components (λ U, eq_to_iso (by simp [map, set.preimage_preimage]))
+    (by { intros _ _ _, simp }) }
+
 end topological_space.opens
 
 /--

src/topology/sheaves/presheaf.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Mario Carneiro, Reid Barton, Andrew Yang
 -/
 import category_theory.limits.kan_extension
+import category_theory.adjunction
 import topology.category.Top.opens
 
 /-!
@@ -184,17 +185,15 @@ end
 namespace pullback
 variables {X Y : Top.{v}} (ℱ : Y.presheaf C)
 
-local attribute [reassoc] colimit.pre_desc
-
 /-- The pullback along the identity is isomorphic to the original presheaf. -/
 def id : pullback_obj (𝟙 _) ℱ ≅ ℱ :=
 nat_iso.of_components
   (λ U, pullback_obj_obj_of_image_open (𝟙 _) ℱ (unop U) (by simpa using U.unop.2) ≪≫
     ℱ.map_iso (eq_to_iso (by simp)))
   (λ U V i,
   begin
-      ext, simp[-eq_to_hom_map,-eq_to_iso_map],
-      erw category_theory.limits.colimit.pre_desc_assoc,
+      ext, simp [-eq_to_hom_map,-eq_to_iso_map],
+      erw colimit.pre_desc_assoc,
       erw colimit.ι_desc_assoc,
       erw colimit.ι_desc_assoc,
       dsimp, simp only [←ℱ.map_comp], congr
@@ -231,17 +230,85 @@ begin
     erw h (opens.op_map_id_obj U), simpa },
   { intros, apply pushforward.id_eq },
 end
-variables [has_colimits C]
+
+section iso
+
+/-- A homeomorphism of spaces gives an equivalence of categories of presheaves. -/
+@[simps] def presheaf_equiv_of_iso {X Y : Top} (H : X ≅ Y) :
+  X.presheaf C ≌ Y.presheaf C :=
+equivalence.congr_left (opens.map_map_iso H).symm.op
+
+variable {C}
+
+/--
+If `H : X ≅ Y` is a homeomorphism,
+then given an `H _* ℱ ⟶ 𝒢`, we may obtain an `ℱ ⟶ H ⁻¹ _* 𝒢`.
+-/
+def to_pushforward_of_iso {X Y : Top} (H : X ≅ Y) {ℱ : X.presheaf C} {𝒢 : Y.presheaf C}
+  (α : H.hom _* ℱ ⟶ 𝒢) : ℱ ⟶ H.inv _* 𝒢 :=
+(presheaf_equiv_of_iso _ H).to_adjunction.hom_equiv ℱ 𝒢 α
+
+@[simp]
+lemma to_pushforward_of_iso_app {X Y : Top} (H₁ : X ≅ Y) {ℱ : X.presheaf C} {𝒢 : Y.presheaf C}
+  (H₂ : H₁.hom _* ℱ ⟶ 𝒢) (U : (opens X)ᵒᵖ) :
+(to_pushforward_of_iso H₁ H₂).app U =
+  ℱ.map (eq_to_hom (by simp [opens.map, set.preimage_preimage])) ≫
+  H₂.app (op ((opens.map H₁.inv).obj (unop U))) :=
+begin
+  delta to_pushforward_of_iso,
+  simp only [equiv.to_fun_as_coe, nat_trans.comp_app, equivalence.equivalence_mk'_unit,
+    eq_to_hom_map, presheaf_equiv_of_iso_unit_iso_hom_app_app, equivalence.to_adjunction,
+    equivalence.equivalence_mk'_counit, presheaf_equiv_of_iso_inverse_map_app,
+    adjunction.mk_of_unit_counit_hom_equiv_apply],
+  congr
+end
+
+/--
+If `H : X ≅ Y` is a homeomorphism,
+then given an `H _* ℱ ⟶ 𝒢`, we may obtain an `ℱ ⟶ H ⁻¹ _* 𝒢`.
+-/
+def pushforward_to_of_iso {X Y : Top} (H₁ : X ≅ Y) {ℱ : Y.presheaf C} {𝒢 : X.presheaf C}
+  (H₂ : ℱ ⟶ H₁.hom _* 𝒢) : H₁.inv _* ℱ ⟶ 𝒢 :=
+((presheaf_equiv_of_iso _ H₁.symm).to_adjunction.hom_equiv ℱ 𝒢).symm H₂
+
+@[simp]
+lemma pushforward_to_of_iso_app {X Y : Top} (H₁ : X ≅ Y) {ℱ : Y.presheaf C} {𝒢 : X.presheaf C}
+  (H₂ : ℱ ⟶ H₁.hom _* 𝒢) (U : (opens X)ᵒᵖ) :
+(pushforward_to_of_iso H₁ H₂).app U =
+  H₂.app (op ((opens.map H₁.inv).obj (unop U))) ≫
+  𝒢.map (eq_to_hom (by simp [opens.map, set.preimage_preimage])) :=
+by simpa [pushforward_to_of_iso, equivalence.to_adjunction]
+
+end iso
+
+variables (C) [has_colimits C]
 
 /-- Pullback a presheaf on `Y` along a continuous map `f : X ⟶ Y`, obtaining a presheaf
 on `X`. -/
-@[simps]
+@[simps map_app]
 def pullback {X Y : Top.{v}} (f : X ⟶ Y) : Y.presheaf C ⥤ X.presheaf C := Lan (opens.map f).op
 
+@[simp] lemma pullback_obj_eq_pullback_obj {C} [category C] [has_colimits C] {X Y : Top.{v}}
+  (f : X ⟶ Y) (ℱ : Y.presheaf C) : (pullback C f).obj ℱ = pullback_obj f ℱ := rfl
+
 /-- The pullback and pushforward along a continuous map are adjoint to each other. -/
 @[simps unit_app_app counit_app_app]
 def pushforward_pullback_adjunction {X Y : Top.{v}} (f : X ⟶ Y) :
   pullback C f ⊣ pushforward C f := Lan.adjunction _ _
 
+/-- Pulling back along a homeomorphism is the same as pushing forward along its inverse. -/
+def pullback_hom_iso_pushforward_inv {X Y : Top.{v}} (H : X ≅ Y) :
+  pullback C H.hom ≅ pushforward C H.inv :=
+adjunction.left_adjoint_uniq
+  (pushforward_pullback_adjunction C H.hom)
+  (presheaf_equiv_of_iso C H.symm).to_adjunction
+
+/-- Pulling back along the inverse of a homeomorphism is the same as pushing forward along it. -/
+def pullback_inv_iso_pushforward_hom {X Y : Top.{v}} (H : X ≅ Y) :
+  pullback C H.inv ≅ pushforward C H.hom :=
+adjunction.left_adjoint_uniq
+  (pushforward_pullback_adjunction C H.inv)
+  (presheaf_equiv_of_iso C H).to_adjunction
+
 end presheaf
 end Top