[Merged by Bors] - refactor(topology+algebraic_geometry): prove and make use of equalities to simplify definitions

src/algebraic_geometry/Scheme.lean

@@ -34,7 +34,7 @@ for some `R : CommRing`.
 -/
 structure Scheme extends X : LocallyRingedSpace :=
 (local_affine : ∀ x : X, ∃ (U : open_nhds x) (R : CommRing),
-  nonempty (X.restrict _ U.open_embedding ≅ Spec.to_LocallyRingedSpace.obj (op R)))
+  nonempty (X.restrict U.open_embedding ≅ Spec.to_LocallyRingedSpace.obj (op R)))
 
 namespace Scheme
 
@@ -109,10 +109,10 @@ lemma Γ_def : Γ = (induced_functor Scheme.to_LocallyRingedSpace).op ⋙ Locall
 lemma Γ_obj_op (X : Scheme) : Γ.obj (op X) = X.presheaf.obj (op ⊤) := rfl
 
 @[simp] lemma Γ_map {X Y : Schemeᵒᵖ} (f : X ⟶ Y) :
-  Γ.map f = f.unop.1.c.app (op ⊤) ≫ (unop Y).presheaf.map (opens.le_map_top _ _).op := rfl
+  Γ.map f = f.unop.1.c.app (op ⊤) := rfl
 
 lemma Γ_map_op {X Y : Scheme} (f : X ⟶ Y) :
-  Γ.map f.op = f.1.c.app (op ⊤) ≫ X.presheaf.map (opens.le_map_top _ _).op := rfl
+  Γ.map f.op = f.1.c.app (op ⊤) := rfl
 
 -- PROJECTS:
 -- 1. Construct `Spec ≫ Γ ≅ functor.id _`.

src/algebraic_geometry/Spec.lean

@@ -103,19 +103,13 @@ begin
   dsimp,
   erw [PresheafedSpace.id_c_app, comap_id], swap,
     { rw [Spec.Top_map_id, topological_space.opens.map_id_obj_unop] },
-  rw [eq_to_hom_op, eq_to_hom_map, eq_to_hom_trans],
-  refl,
+  simpa,
 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,
-begin
-  dsimp,
-  erw [Top.presheaf.pushforward.comp_inv_app, ← category.assoc, category.comp_id,
-    (structure_sheaf T).1.map_id, category.comp_id, comap_comp],
-  refl,
-end
+by { dsimp, rw category.comp_id, erw comap_comp f g, refl }
 
 /--
 Spec, as a contravariant functor from commutative rings to sheafed spaces.

src/algebraic_geometry/locally_ringed_space.lean

@@ -32,7 +32,7 @@ namespace algebraic_geometry
 such that all the stalks are local rings.
 
 A morphism of locally ringed spaces is a morphism of ringed spaces
-such that the morphims induced on stalks are local ring homomorphisms. -/
+such that the morphisms induced on stalks are local ring homomorphisms. -/
 @[nolint has_inhabited_instance]
 structure LocallyRingedSpace extends SheafedSpace CommRing :=
 (local_ring : ∀ x, local_ring (presheaf.stalk x))
@@ -166,24 +166,24 @@ instance : reflects_isomorphisms forget_to_SheafedSpace :=
 The restriction of a locally ringed space along an open embedding.
 -/
 @[simps]
-def restrict {U : Top} (X : LocallyRingedSpace) (f : U ⟶ X.to_Top)
+def restrict {U : Top} (X : LocallyRingedSpace) {f : U ⟶ X.to_Top}
   (h : open_embedding f) : LocallyRingedSpace :=
 { local_ring :=
   begin
     intro x,
     dsimp at *,
     -- We show that the stalk of the restriction is isomorphic to the original stalk,
     apply @ring_equiv.local_ring _ _ _ (X.local_ring (f x)),
-    exact (X.to_PresheafedSpace.restrict_stalk_iso f h x).symm.CommRing_iso_to_ring_equiv,
+    exact (X.to_PresheafedSpace.restrict_stalk_iso h x).symm.CommRing_iso_to_ring_equiv,
   end,
-  .. X.to_SheafedSpace.restrict f h }
+  .. X.to_SheafedSpace.restrict h }
 
 /--
 The restriction of a locally ringed space `X` to the top subspace is isomorphic to `X` itself.
 -/
 def restrict_top_iso (X : LocallyRingedSpace) :
-  X.restrict (opens.inclusion ⊤) (opens.open_embedding ⊤) ≅ X :=
-@iso_of_SheafedSpace_iso (X.restrict (opens.inclusion ⊤) (opens.open_embedding ⊤)) X
+  X.restrict (opens.open_embedding ⊤) ≅ X :=
+@iso_of_SheafedSpace_iso (X.restrict (opens.open_embedding ⊤)) X
   X.to_SheafedSpace.restrict_top_iso
 
 /--
@@ -199,10 +199,10 @@ lemma Γ_def : Γ = forget_to_SheafedSpace.op ⋙ SheafedSpace.Γ := rfl
 lemma Γ_obj_op (X : LocallyRingedSpace) : Γ.obj (op X) = X.presheaf.obj (op ⊤) := rfl
 
 @[simp] lemma Γ_map {X Y : LocallyRingedSpaceᵒᵖ} (f : X ⟶ Y) :
-  Γ.map f = f.unop.1.c.app (op ⊤) ≫ (unop Y).presheaf.map (opens.le_map_top _ _).op := rfl
+  Γ.map f = f.unop.1.c.app (op ⊤) := rfl
 
 lemma Γ_map_op {X Y : LocallyRingedSpace} (f : X ⟶ Y) :
-  Γ.map f.op = f.1.c.app (op ⊤) ≫ X.presheaf.map (opens.le_map_top _ _).op := rfl
+  Γ.map f.op = f.1.c.app (op ⊤) := rfl
 
 end LocallyRingedSpace
 

src/algebraic_geometry/presheafed_space.lean

@@ -67,26 +67,37 @@ structure hom (X Y : PresheafedSpace C) :=
 
 @[ext] lemma ext {X Y : PresheafedSpace C} (α β : hom X Y)
   (w : α.base = β.base)
-  (h : α.c ≫ (whisker_right (nat_trans.op (opens.map_iso _ _ w).inv) X.presheaf) = β.c) :
+  (h : α.c ≫ eq_to_hom (by rw w) = β.c) :
   α = β :=
 begin
   cases α, cases β,
   dsimp [presheaf.pushforward_obj] at *,
   tidy, -- TODO including `injections` would make tidy work earlier.
 end
+
+lemma ext' {X Y : PresheafedSpace C} (α β : hom X Y)
+  (w : α.base = β.base)
+  (h : α.c == β.c) :
+  α = β :=
+by { cases α, cases β, congr, exacts [w,h] }
+
 .
 
 /-- The identity morphism of a `PresheafedSpace`. -/
 def id (X : PresheafedSpace C) : hom X X :=
 { base := 𝟙 (X : Top.{v}),
-  c := (functor.left_unitor _).inv ≫ whisker_right (nat_trans.op (opens.map_id X.carrier).hom) _ }
+  c := eq_to_hom (presheaf.pushforward.id_eq X.presheaf).symm }
 
 instance hom_inhabited (X : PresheafedSpace C) : inhabited (hom X X) := ⟨id X⟩
 
 /-- Composition of morphisms of `PresheafedSpace`s. -/
 def comp {X Y Z : PresheafedSpace C} (α : hom X Y) (β : hom Y Z) : hom X Z :=
 { base := α.base ≫ β.base,
-  c := β.c ≫ (whisker_left (opens.map β.base).op α.c) ≫ (Top.presheaf.pushforward.comp _ _ _).inv }
+  c := β.c ≫ (presheaf.pushforward β.base).map α.c }
+
+lemma comp_c {X Y Z : PresheafedSpace C} (α : hom X Y) (β : hom Y Z) :
+  (comp α β).c = β.c ≫ (presheaf.pushforward β.base).map α.c := rfl
+
 
 variables (C)
 
@@ -101,47 +112,23 @@ 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,
-  begin
-    ext1, swap,
-    { dsimp, simp only [id_comp] },  -- See note [dsimp, simp].
-    { ext U, induction U using opposite.rec, cases U,
-      dsimp,
-      simp only [presheaf.pushforward.comp_inv_app, opens.map_iso_inv_app],
-      dsimp,
-      simp only [comp_id, comp_id, map_id], },
-  end,
-  comp_id' := λ X Y f,
-  begin
-    ext1, swap,
-    { dsimp, simp only [comp_id] },
-    { ext U, induction U using opposite.rec, cases U,
-      dsimp,
-      simp only [presheaf.pushforward.comp_inv_app, opens.map_iso_inv_app],
-      dsimp,
-      simp only [id_comp, comp_id, map_id], }
-  end,
-  assoc' := λ W X Y Z f g h,
-  begin
-     ext1, swap,
-     refl,
-     { ext U, induction U using opposite.rec, cases U,
-       dsimp,
-       simp only [assoc, presheaf.pushforward.comp_inv_app, opens.map_iso_inv_app],
-       dsimp,
-       simp only [comp_id, id_comp, map_id], }
-  end }
+  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 } }
 
 end
 
 variables {C}
 
 @[simp] lemma id_base (X : PresheafedSpace C) :
-  ((𝟙 X) : X ⟶ X).base = (𝟙 (X : Top.{v})) := rfl
+  ((𝟙 X) : X ⟶ X).base = 𝟙 (X : Top.{v}) := rfl
 
 lemma id_c (X : PresheafedSpace C) :
-  ((𝟙 X) : X ⟶ X).c =
-  (functor.left_unitor _).inv ≫ whisker_right (nat_trans.op (opens.map_id X.carrier).hom) _ := rfl
+  ((𝟙 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 }) :=
@@ -151,8 +138,7 @@ by { induction U using opposite.rec, cases U, simp only [id_c], dsimp, simp, }
   (f ≫ g).base = f.base ≫ g.base := rfl
 
 @[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))) ≫
-    (Top.presheaf.pushforward.comp _ _ _).inv.app U := rfl
+  (α ≫ β).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) :
   α.c.app U = β.c.app U ≫ X.presheaf.map (eq_to_hom (by subst h)) :=
@@ -174,84 +160,77 @@ The restriction of a presheafed space along an open embedding into the space.
 -/
 @[simps]
 def restrict {U : Top} (X : PresheafedSpace C)
-  (f : U ⟶ (X : Top.{v})) (h : open_embedding f) : PresheafedSpace C :=
+  {f : U ⟶ (X : Top.{v})} (h : open_embedding f) : PresheafedSpace C :=
 { carrier := U,
   presheaf := h.is_open_map.functor.op ⋙ X.presheaf }
 
 /--
 The map from the restriction of a presheafed space.
 -/
 def of_restrict {U : Top} (X : PresheafedSpace C)
-  (f : U ⟶ (X : Top.{v})) (h : open_embedding f) :
-  X.restrict f h ⟶ X :=
+  {f : U ⟶ (X : Top.{v})} (h : open_embedding f) :
+  X.restrict h ⟶ X :=
 { base := f,
-  c := { app := λ V, X.presheaf.map $
-      ((h.is_open_map.adjunction.hom_equiv _ _).symm (𝟙 $ (opens.map f).obj $ unop V)).op,
-    naturality':= λ U V f, show _ = _ ≫ X.presheaf.map _,
+  c := { app := λ V, X.presheaf.map (h.is_open_map.adjunction.counit.app V.unop).op,
+    naturality' := λ U V f, show _ = _ ≫ X.presheaf.map _,
       by { rw [← map_comp, ← map_comp], refl } } }
 
+lemma restrict_top_presheaf (X : PresheafedSpace C) :
+  (X.restrict (opens.open_embedding ⊤)).presheaf =
+  (opens.inclusion_top_iso X.carrier).inv _* X.presheaf :=
+by { dsimp, rw opens.inclusion_top_functor X.carrier, refl }
+
+lemma of_restrict_top_c (X : PresheafedSpace C) :
+  ∃ h, (X.of_restrict (opens.open_embedding ⊤)).c = eq_to_hom h :=
+  /- another approach would be to prove the left hand side
+     is a natural isoomorphism, but I encountered a universe
+     issue when `apply nat_iso.is_iso_of_is_iso_app`. -/
+begin
+  fsplit, { rw [restrict_top_presheaf, ←presheaf.pushforward.comp_eq],
+    erw iso.inv_hom_id, rw presheaf.pushforward.id_eq },
+  ext U, change X.presheaf.map _ = _, convert eq_to_hom_map _ _ using 1,
+  congr, simpa,
+  { induction U using opposite.rec, dsimp, congr, ext,
+    exact ⟨ λ h, ⟨⟨x,trivial⟩,h,rfl⟩, λ ⟨⟨_,_⟩,h,rfl⟩, h ⟩ },
+    /- or `rw [opens.inclusion_top_functor, ←comp_obj, ←opens.map_comp_eq],
+           erw iso.inv_hom_id, cases U, refl` after `dsimp` -/
+end
+
 /--
 The map to the restriction of a presheafed space along the canonical inclusion from the top
 subspace.
 -/
 @[simps]
 def to_restrict_top (X : PresheafedSpace C) :
-  X ⟶ X.restrict (opens.inclusion ⊤) (opens.open_embedding ⊤) :=
-{ base := ⟨λ x, ⟨x, trivial⟩, continuous_def.2 $ λ U ⟨S, hS, hSU⟩, hSU ▸ hS⟩,
-  c := { app := λ U, X.presheaf.map $ (hom_of_le $ λ x hxU, ⟨⟨x, trivial⟩, hxU, rfl⟩ :
-      (opens.map (⟨λ x, ⟨x, trivial⟩, continuous_def.2 $ λ U ⟨S, hS, hSU⟩, hSU ▸ hS⟩ :
-          X.1 ⟶ (opens.to_Top X.1).obj ⊤)).obj (unop U) ⟶
-        (opens.open_embedding ⊤).is_open_map.functor.obj (unop U)).op,
-    naturality':= λ U V f, show X.presheaf.map _ ≫ _ = _ ≫ X.presheaf.map _,
-      by { rw [← map_comp, ← map_comp], refl } } }
+  X ⟶ X.restrict (opens.open_embedding ⊤) :=
+{ base := (opens.inclusion_top_iso X.carrier).inv,
+  c := eq_to_hom (restrict_top_presheaf X) }
 
 /--
 The isomorphism from the restriction to the top subspace.
 -/
 @[simps]
 def restrict_top_iso (X : PresheafedSpace C) :
-  X.restrict (opens.inclusion ⊤) (opens.open_embedding ⊤) ≅ X :=
-{ hom := X.of_restrict _ _,
+  X.restrict (opens.open_embedding ⊤) ≅ X :=
+{ hom := X.of_restrict _,
   inv := X.to_restrict_top,
   hom_inv_id' := ext _ _ (concrete_category.hom_ext _ _ $ λ ⟨x, _⟩, rfl) $
-    nat_trans.ext _ _ $ funext $ λ U, by { induction U using opposite.rec,
-      dsimp only [nat_trans.comp_app, comp_c_app, to_restrict_top, of_restrict,
-          whisker_right_app, comp_base, nat_trans.op_app, opens.map_iso_inv_app],
-      erw [presheaf.pushforward.comp_inv_app, comp_id, ← X.presheaf.map_comp,
-          ← X.presheaf.map_comp, id_c_app],
-      exact X.presheaf.map_id _ },
-  inv_hom_id' := ext _ _ rfl $ nat_trans.ext _ _ $ funext $ λ U, by {
-    induction U using opposite.rec,
-    dsimp only [nat_trans.comp_app, comp_c_app, of_restrict, to_restrict_top,
-        whisker_right_app, comp_base, nat_trans.op_app, opens.map_iso_inv_app],
-    erw [← X.presheaf.map_comp, ← X.presheaf.map_comp, ← X.presheaf.map_comp, id_c_app],
-    convert eq_to_hom_map X.presheaf _,
-    erw [op_obj, id_base, opens.map_id_obj], refl } }
+    by { erw comp_c, rw X.of_restrict_top_c.some_spec, simpa },
+  inv_hom_id' := ext _ _ rfl $
+    by { erw comp_c, rw X.of_restrict_top_c.some_spec, simpa } }
 
 /--
 The global sections, notated Gamma.
 -/
 @[simps]
 def Γ : (PresheafedSpace C)ᵒᵖ ⥤ C :=
 { obj := λ X, (unop X).presheaf.obj (op ⊤),
-  map := λ X Y f, f.unop.c.app (op ⊤) ≫ (unop Y).presheaf.map (opens.le_map_top _ _).op,
-  map_id' := λ X, begin
-    induction X using opposite.rec,
-    erw [unop_id_op, id_c_app, eq_to_hom_refl, id_comp],
-    exact X.presheaf.map_id _
-  end,
-  map_comp' := λ X Y Z f g, begin
-    rw [unop_comp, comp_c_app],
-    simp_rw category.assoc,
-    erw [nat_trans.naturality_assoc, presheaf.pushforward.comp_inv_app, id_comp,
-        category_theory.functor.comp_map, ← map_comp],
-    refl
-  end }
+  map := λ X Y f, f.unop.c.app (op ⊤) }
 
 lemma Γ_obj_op (X : PresheafedSpace C) : Γ.obj (op X) = X.presheaf.obj (op ⊤) := rfl
 
 lemma Γ_map_op {X Y : PresheafedSpace C} (f : X ⟶ Y) :
-  Γ.map f.op = f.c.app (op ⊤) ≫ X.presheaf.map (opens.le_map_top _ _).op := rfl
+  Γ.map f.op = f.c.app (op ⊤) := rfl
 
 end PresheafedSpace
 
@@ -294,8 +273,7 @@ A natural transformation induces a natural transformation between the `map_presh
 def on_presheaf {F G : C ⥤ D} (α : F ⟶ G) : G.map_presheaf ⟶ F.map_presheaf :=
 { app := λ X,
   { base := 𝟙 _,
-    c := whisker_left X.presheaf α ≫ (functor.left_unitor _).inv ≫
-           whisker_right (nat_trans.op (opens.map_id X.carrier).hom) _ }, }
+    c := whisker_left X.presheaf α ≫ eq_to_hom (presheaf.pushforward.id_eq _).symm } }
 
 -- TODO Assemble the last two constructions into a functor
 --   `(C ⥤ D) ⥤ (PresheafedSpace C ⥤ PresheafedSpace D)`

src/algebraic_geometry/presheafed_space/has_colimits.lean

@@ -164,8 +164,7 @@ def colimit_cocone (F : J ⥤ PresheafedSpace C) : cocone F :=
         congr,
         dsimp,
         simp only [id_comp],
-        rw ←is_iso.inv_comp_eq,
-        simp, refl, }
+        simpa, }
     end, }, }
 
 namespace colimit_cocone_is_colimit
@@ -196,7 +195,7 @@ begin
     replace w := congr_arg op w,
     have w' := nat_trans.congr (F.map f.unop).c w,
     rw w',
-    dsimp, simp, dsimp, simp, refl, },
+    dsimp, simp, dsimp, simp, },
 end
 
 lemma desc_c_naturality (F : J ⥤ PresheafedSpace C) (s : cocone F)
@@ -265,7 +264,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,
-      simp, dsimp, simp, }
+      simpa }
   end, }
 
 /--