chore(topology/sheaves): depend less on rfl (#3994)

Another backport from the `prop_limits` branch.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/category_theory/limits/shapes/types.lean

@@ -37,10 +37,16 @@ namespace category_theory.limits.types
 
 /-- A restatement of `types.lift_π_apply` that uses `pi.π` and `pi.lift`. -/
 @[simp]
-lemma lift_π_apply' {β : Type u} (f : β → Type u) {P : Type u} (s : Π b, P ⟶ f b) (b : β) (x : P) :
+lemma pi_lift_π_apply {β : Type u} (f : β → Type u) {P : Type u} (s : Π b, P ⟶ f b) (b : β) (x : P) :
   (pi.π f b : (∏ f) → f b) (@pi.lift β _ _ f _ P s x) = s b x :=
 congr_fun (limit.lift_π (fan.mk s) b) x
 
+/-- A restatement of `types.map_π_apply` that uses `pi.π` and `pi.map`. -/
+@[simp]
+lemma pi_map_π_apply {β : Type u} {f g : β → Type u} (α : Π j, f j ⟶ g j) (b : β) (x) :
+  (pi.π g b : (∏ g) → g b) (pi.map α x) = α b ((pi.π f b : (∏ f) → f b) x) :=
+map_π_apply _ _ _
+
 /-- The category of types has `punit` as a terminal object. -/
 def types_has_terminal : has_terminal (Type u) :=
 { has_limit := λ F,

src/category_theory/limits/types.lean

@@ -67,11 +67,21 @@ end
 -- TODO: are there other limits lemmas that should have `_apply` versions?
 -- Can we generate these like with `@[reassoc]`?
 -- PROJECT: prove these for any concrete category where the forgetful functor preserves limits?
+
+@[simp] lemma limit_w_apply {F : J ⥤ Type u} {j j' : J} {x : limit F} (f : j ⟶ j') :
+  F.map f (limit.π F j x) = limit.π F j' x :=
+congr_fun (limit.w F f) x
+
 @[simp]
 lemma lift_π_apply (F : J ⥤ Type u) (s : cone F) (j : J) (x : s.X) :
   limit.π F j (limit.lift F s x) = s.π.app j x :=
 congr_fun (limit.lift_π s j) x
 
+@[simp]
+lemma map_π_apply {F G : J ⥤ Type u} (α : F ⟶ G) (j : J) (x) :
+  limit.π G j (lim.map α x) = α.app j (limit.π F j x) :=
+congr_fun (limit.map_π α j) x
+
 /--
 A quotient type implementing the colimit of a functor `F : J ⥤ Type u`,
 as pairs `⟨j, x⟩` where `x : F.obj j`, modulo the equivalence relation generated by
@@ -115,11 +125,28 @@ lemma colimit_equiv_quot_symm_apply (F : J ⥤ Type u) (j : J) (x : F.obj j) :
   (colimit_equiv_quot F).symm (quot.mk _ ⟨j, x⟩) = colimit.ι F j x :=
 rfl
 
+@[simp] lemma colimit_w_apply {F : J ⥤ Type u} {j j' : J} {x : F.obj j} (f : j ⟶ j') :
+  colimit.ι F j' (F.map f x) = colimit.ι F j x :=
+congr_fun (colimit.w F f) x
+
 @[simp]
 lemma ι_desc_apply (F : J ⥤ Type u) (s : cocone F) (j : J) (x : F.obj j) :
   colimit.desc F s (colimit.ι F j x) = s.ι.app j x :=
 congr_fun (colimit.ι_desc s j) x
 
+@[simp]
+lemma ι_map_apply {F G : J ⥤ Type u} (α : F ⟶ G) (j : J) (x) :
+  colim.map α (colimit.ι F j x) = colimit.ι G j (α.app j x) :=
+congr_fun (colimit.ι_map α j) x
+
+lemma colimit_sound
+  {F : J ⥤ Type u} {j j' : J} {x : F.obj j} {x' : F.obj j'} (f : j ⟶ j') (w : F.map f x = x') :
+  colimit.ι F j x = colimit.ι F j' x' :=
+begin
+  rw [←w],
+  simp,
+end
+
 lemma jointly_surjective (F : J ⥤ Type u) {t : cocone F} (h : is_colimit t)
   (x : t.X) : ∃ j y, t.ι.app j y = x :=
 begin
@@ -226,8 +253,9 @@ begin
     exact relation.eqv_gen_iff_of_equivalence (filtered_colimit.r_equiv F) }
 end
 
-lemma colimit_eq_iff {i j : J} {xi : F.obj i} {xj : F.obj j} :
-  colimit.ι F i xi = colimit.ι F j xj ↔ ∃ k (f : i ⟶ k) (g : j ⟶ k), F.map f xi = F.map g xj :=
+lemma colimit_eq_iff_aux {i j : J} {xi : F.obj i} {xj : F.obj j} :
+  (colimit_cocone F).ι.app i xi = (colimit_cocone F).ι.app j xj ↔
+    ∃ k (f : i ⟶ k) (g : j ⟶ k), F.map f xi = F.map g xj :=
 begin
   change quot.mk _ _ = quot.mk _ _ ↔ _,
   rw [quot.eq, ←filtered_colimit.r_eq],
@@ -237,14 +265,18 @@ end
 variables {t} (ht : is_colimit t)
 lemma is_colimit_eq_iff {i j : J} {xi : F.obj i} {xj : F.obj j} :
   t.ι.app i xi = t.ι.app j xj ↔ ∃ k (f : i ⟶ k) (g : j ⟶ k), F.map f xi = F.map g xj :=
-let t' := colimit.cocone F,
-    e : t' ≅ t := is_colimit.unique_up_to_iso (colimit.is_colimit F) ht,
+let t' := colimit_cocone F,
+    e : t' ≅ t := is_colimit.unique_up_to_iso (colimit_cocone_is_colimit F) ht,
     e' : t'.X ≅ t.X := (cocones.forget _).map_iso e in
 begin
-  refine iff.trans _ (colimit_eq_iff F),
+  refine iff.trans _ (colimit_eq_iff_aux F),
   convert equiv.apply_eq_iff_eq e'.to_equiv _ _; rw ←e.hom.w; refl
 end
 
+lemma colimit_eq_iff {i j : J} {xi : F.obj i} {xj : F.obj j} :
+  colimit.ι F i xi = colimit.ι F j xj ↔ ∃ k (f : i ⟶ k) (g : j ⟶ k), F.map f xi = F.map g xj :=
+is_colimit_eq_iff _ (colimit.is_colimit F)
+
 end filtered_colimit
 
 variables {α β : Type u} (f : α ⟶ β)

src/topology/sheaves/local_predicate.lean

@@ -167,10 +167,30 @@ from the sheaf condition diagram for functions satisfying a local predicate
 to the sheaf condition diagram for arbitrary functions,
 given by forgetting that the local predicate holds.
 -/
+@[simps]
 def diagram_subtype {ι : Type v} (U : ι → opens X) :
   diagram (subpresheaf_to_Types P) U ⟶ diagram (presheaf_to_Types X T) U :=
 { app := λ j, walking_parallel_pair.rec_on j (pi.map (λ i f, f.1)) (pi.map (λ p f, f.1)),
-  naturality' := by rintro ⟨_|_⟩ ⟨_|_⟩ f; cases f; refl, }
+  naturality' :=
+  begin
+    rintro ⟨_|_⟩ ⟨_|_⟩ ⟨⟩,
+    { refl, },
+    { dsimp [left_res, subpresheaf_to_Types, presheaf_to_Types],
+      simp only [limit.lift_map],
+      ext1 ⟨i₁,i₂⟩,
+      simp only [limit.lift_π, cones.postcompose_obj_π, discrete.nat_trans_app, limit.map_π_assoc,
+        fan.mk_π_app, nat_trans.comp_app, category.assoc],
+      ext,
+      simp only [types_comp_apply, subtype.val_eq_coe], },
+    { dsimp [right_res, subpresheaf_to_Types, presheaf_to_Types],
+      simp only [limit.lift_map],
+      ext1 ⟨i₁,i₂⟩,
+      simp only [limit.lift_π, cones.postcompose_obj_π, discrete.nat_trans_app, limit.map_π_assoc,
+        fan.mk_π_app, nat_trans.comp_app, category.assoc],
+      ext,
+      simp only [types_comp_apply, subtype.val_eq_coe], },
+    { refl, },
+  end}
 
 /--
 The functions satisfying a local predicate satisfy the sheaf condition.
@@ -220,7 +240,11 @@ begin
     intros s,
     ext i f : 2,
     apply subtype.coe_injective,
-    exact congr_fun (((to_Types X T U).fac _ walking_parallel_pair.zero) =≫ pi.π _ i) _, },
+    convert congr_fun
+      ((to_Types X T U).fac
+        ((cones.postcompose (diagram_subtype P.to_prelocal_predicate U)).obj s)
+        walking_parallel_pair.zero =≫
+      pi.π (λ (i : ι), (X.presheaf_to_Types T).obj (op (U i))) i) f, },
   { -- Similarly for proving the uniqueness condition, after a certain amount of bookkeeping.
     intros s m w,
     ext f : 1,
@@ -239,12 +263,14 @@ begin
       intro i,
       simp only [category.assoc, limit.map_π],
       ext f' ⟨x, mem⟩,
-      refl, },
+      dsimp [res, subpresheaf_to_Types, presheaf_to_Types],
+      simp, },
     { apply limit.hom_ext,
       intro i,
       simp only [category.assoc, limit.map_π],
       ext f' ⟨x, mem⟩,
-      refl, }, },
+      dsimp [res, left_res, subpresheaf_to_Types, presheaf_to_Types],
+      simp, }, },
 end
 
 end subpresheaf_to_Types
@@ -290,7 +316,7 @@ begin
   rcases w t with ⟨U, f, h, rfl⟩,
   fsplit,
   { exact (subsheaf_to_Types P).presheaf.germ ⟨x, U.2⟩ ⟨f, h⟩, },
-  { exact stalk_to_fiber_germ _ _ _ ⟨f, h⟩, }
+  { exact stalk_to_fiber_germ _ U.1 ⟨x, U.2⟩ ⟨f, h⟩, }
 end
 
 /--
@@ -307,23 +333,23 @@ begin
   -- We promise to provide all the ingredients of the proof later:
   let Q :
     ∃ (W : (open_nhds x)ᵒᵖ) (s : Π w : (unop W).1, T w) (hW : P.pred s),
-      tU = quot.mk _ ⟨W, ⟨s, hW⟩⟩ ∧ tV = quot.mk _ ⟨W, ⟨s, hW⟩⟩ := _,
+      tU = (subsheaf_to_Types P).presheaf.germ ⟨x, (unop W).2⟩ ⟨s, hW⟩ ∧
+      tV = (subsheaf_to_Types P).presheaf.germ ⟨x, (unop W).2⟩ ⟨s, hW⟩ := _,
   { choose W s hW e using Q,
     exact e.1.trans e.2.symm, },
   -- Then use induction to pick particular representatives of `tU tV : stalk x`
-  induction tU,
-  induction tV,
+  obtain ⟨U, ⟨fU, hU⟩, rfl⟩ := types.jointly_surjective' tU,
+  obtain ⟨V, ⟨fV, hV⟩, rfl⟩ := types.jointly_surjective' tV,
   { -- Decompose everything into its constituent parts:
     dsimp,
-    rcases tU with ⟨U, ⟨fU, hU⟩⟩,
-    rcases tV with ⟨V, ⟨fV, hV⟩⟩,
+    simp only [stalk_to_fiber, types.ι_desc_apply] at h,
     specialize w (unop U) (unop V) fU hU fV hV h,
     rcases w with ⟨W, iU, iV, w⟩,
     -- and put it back together again in the correct order.
     refine ⟨(op W), (λ w, fU (iU w : (unop U).1)), P.res _ _ hU, _⟩,
-    exact ⟨quot.sound ⟨iU.op, subtype.eq rfl⟩, quot.sound ⟨iV.op, subtype.eq (funext w)⟩⟩, },
-  { refl, }, -- proof irrelevance
-  { refl, }, -- proof irrelevance
+    rcases W with ⟨W, m⟩,
+    exact ⟨types.colimit_sound iU.op (subtype.eq rfl),
+           types.colimit_sound iV.op (subtype.eq (funext w).symm)⟩, },
 end
 
 /--

src/topology/sheaves/stalks.lean

@@ -53,14 +53,15 @@ lemma germ_exist (F : X.presheaf (Type v)) (x : X) (t : stalk F x) :
 begin
   obtain ⟨U, s, rfl⟩ := types.jointly_surjective' t,
   refine ⟨(unop U).1, (unop U).2, s, _⟩,
-  apply quot.sound,
   revert s,
   rw [(show U = op (unop U), from rfl)],
   generalize : unop U = V, clear U,
   intro s,
   cases V,
-  dsimp,
-  exact ⟨(𝟙 _).op, by { erw category_theory.functor.map_id, refl, }⟩,
+  fapply types.colimit_sound,
+  { exact (𝟙 _).op, },
+  { erw category_theory.functor.map_id,
+    refl, },
 end
 
 @[simp] lemma germ_res (F : X.presheaf C) {U V : opens X} (i : U ⟶ V) (x : U) :