refactor: fixes to material on sheaves and stalks (#4571)

Mostly this is installing the `Opposite.rec'` induction principle as the default `@[eliminator]`, but also many other fixes and removing unnecessary steps from proofs.



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

Mathlib/AlgebraicGeometry/PresheafedSpace.lean

@@ -22,15 +22,7 @@ presheaves.
 -/
 
 
-open CategoryTheory
-
-open TopCat
-
-open TopologicalSpace
-
-open Opposite
-
-open CategoryTheory.Category CategoryTheory.Functor
+open Opposite CategoryTheory CategoryTheory.Category CategoryTheory.Functor TopCat TopologicalSpace
 
 variable (C : Type _) [Category C]
 
@@ -44,7 +36,7 @@ variable (C : Type _) [Category C]
 -- local attribute [tidy] tactic.op_induction'
 -- A possible replacement would be:
 -- attribute [local aesop safe cases (rule_sets [CategoryTheory])] Opposite
--- but this would require further investigation.
+-- but it doesn't seem necessary here.
 
 namespace AlgebraicGeometry
 

Mathlib/AlgebraicGeometry/PresheafedSpace/HasColimits.lean

@@ -40,34 +40,22 @@ noncomputable section
 
 universe v' u' v u
 
-open CategoryTheory
+open CategoryTheory Opposite CategoryTheory.Category CategoryTheory.Functor CategoryTheory.Limits
+  TopCat TopCat.Presheaf TopologicalSpace
 
-open TopCat
-
-open TopCat.Presheaf
-
-open TopologicalSpace
-
-open Opposite
-
-open CategoryTheory.Category
-
-open CategoryTheory.Limits
-
-open CategoryTheory.Functor
-
-variable {J : Type u'} [Category.{v'} J]
-
-variable {C : Type u} [Category.{v} C]
+variable {J : Type u'} [Category.{v'} J] {C : Type u} [Category.{v} C]
 
 namespace AlgebraicGeometry
 
 namespace PresheafedSpace
 
 attribute [local simp] eqToHom_map
 
--- Porting note : `tidy` no longer exist
--- attribute [local tidy] tactic.auto_cases_opens
+-- Porting note: we used to have:
+-- local attribute [tidy] tactic.auto_cases_opens
+-- We would replace this by:
+-- attribute [local aesop safe cases (rule_sets [CategoryTheory])] Opens
+-- although it doesn't appear to help in this file, in any case.
 
 @[simp]
 theorem map_id_c_app (F : J ⥤ PresheafedSpace.{_, _, v} C) (j) (U) :
@@ -76,7 +64,6 @@ theorem map_id_c_app (F : J ⥤ PresheafedSpace.{_, _, v} C) (j) (U) :
         (pushforwardEq (by simp) (F.obj j).presheaf).hom.app
           (op U) := by
   cases U
-  dsimp
   simp [PresheafedSpace.congr_app (F.map_id j)]
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.PresheafedSpace.map_id_c_app AlgebraicGeometry.PresheafedSpace.map_id_c_app
@@ -91,9 +78,7 @@ theorem map_comp_c_app (F : J ⥤ PresheafedSpace.{_, _, v} C) {j₁ j₂ j₃}
             (pushforwardEq (by rw [F.map_comp]; rfl) _).hom.app
               _ := by
   cases U
-  dsimp
-  simp only [PresheafedSpace.congr_app (F.map_comp f g)]
-  dsimp; simp
+  simp [PresheafedSpace.congr_app (F.map_comp f g)]
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.PresheafedSpace.map_comp_c_app AlgebraicGeometry.PresheafedSpace.map_comp_c_app
 
@@ -106,10 +91,8 @@ This is the componentwise diagram for an open set `U` of the colimit of the unde
 def componentwiseDiagram (F : J ⥤ PresheafedSpace.{_, _, v} C) [HasColimit F]
     (U : Opens (Limits.colimit F).carrier) : Jᵒᵖ ⥤ C where
   obj j := (F.obj (unop j)).presheaf.obj (op ((Opens.map (colimit.ι F (unop j)).base).obj U))
-  map {j k} f :=
-    (F.map f.unop).c.app _ ≫
-      (F.obj (unop k)).presheaf.map
-        (eqToHom (by rw [← colimit.w F f.unop, comp_base]; rfl))
+  map {j k} f := (F.map f.unop).c.app _ ≫
+    (F.obj (unop k)).presheaf.map (eqToHom (by rw [← colimit.w F f.unop, comp_base]; rfl))
   map_comp {i j k} f g := by
     dsimp
     simp_rw [map_comp_c_app]
@@ -147,7 +130,7 @@ def pushforwardDiagramToColimit (F : J ⥤ PresheafedSpace.{_, _, v} C) :
   map_id j := by
     apply (opEquiv _ _).injective
     refine NatTrans.ext _ _ (funext fun U => ?_)
-    induction U using Opposite.rec' with
+    induction U with
     | h U =>
       rcases U with ⟨U, hU⟩
       dsimp [comp_obj, forget_obj, Functor.comp_map, forget_map, op_comp, unop_op,
@@ -233,7 +216,7 @@ def colimitCocone (F : J ⥤ PresheafedSpace.{_, _, v} C) : Cocone F where
         · ext x
           exact colimit.w_apply (F ⋙ PresheafedSpace.forget C) f x
         · refine NatTrans.ext _ _ (funext fun U => ?_)
-          induction U using Opposite.rec' with
+          induction U with
           | h U =>
             rcases U with ⟨U, hU⟩
             dsimp
@@ -274,7 +257,6 @@ def descCApp (F : J ⥤ PresheafedSpace.{_, _, v} C) (s : Cocone F) (U : (Opens
     simp
   · dsimp
     rw [PresheafedSpace.congr_app (s.w f.unop).symm U]
-    dsimp
     have w :=
       Functor.congr_obj
         (congr_arg Opens.map (colimit.ι_desc ((PresheafedSpace.forget C).mapCocone s) (unop j)))
@@ -283,7 +265,6 @@ def descCApp (F : J ⥤ PresheafedSpace.{_, _, v} C) (s : Cocone F) (U : (Opens
     replace w := congr_arg op w
     have w' := NatTrans.congr (F.map f.unop).c w
     rw [w']
-    dsimp
     simp
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.PresheafedSpace.colimit_cocone_is_colimit.desc_c_app AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.descCApp
@@ -308,7 +289,7 @@ theorem desc_c_naturality (F : J ⥤ PresheafedSpace.{_, _, v} C) (s : Cocone F)
   simp only [Opens.map_comp_map] at w
   replace w := congr_arg Quiver.Hom.op w
   rw [w]
-  dsimp; simp
+  simp
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.PresheafedSpace.colimit_cocone_is_colimit.desc_c_naturality AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.desc_c_naturality
 
@@ -385,7 +366,6 @@ instance : PreservesColimitsOfShape J (PresheafedSpace.forget.{u, v, v} C) :=
   fapply Cocones.ext
   · rfl
   · intro j
-    dsimp
     simp⟩
 
 /-- When `C` has limits, the category of presheaved spaces with values in `C` itself has colimits.
@@ -404,7 +384,6 @@ instance forgetPreservesColimits [HasLimits C] : PreservesColimits (PresheafedSp
               fapply Cocones.ext
               · rfl
               · intro j
-                dsimp
                 simp) }
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.PresheafedSpace.forget_preserves_colimits AlgebraicGeometry.PresheafedSpace.forgetPreservesColimits

Mathlib/AlgebraicGeometry/SheafedSpace.lean

@@ -29,7 +29,11 @@ open CategoryTheory TopCat TopologicalSpace Opposite CategoryTheory.Limits Categ
 
 variable (C : Type u) [Category.{v} C]
 
--- attribute [local tidy] tactic.op_induction'
+-- Porting note: removed
+-- local attribute [tidy] tactic.op_induction'
+-- as it isn't needed here. If it is useful elsewhere
+-- attribute [local aesop safe cases (rule_sets [CategoryTheory])] Opposite
+-- should suffice.
 
 namespace AlgebraicGeometry
 
@@ -100,7 +104,6 @@ instance forgetToPresheafedSpace_full : Full <| forgetToPresheafedSpace (C := C)
 
 -- Porting note : can't derive `Faithful` functor automatically
 instance forgetToPresheafedSpace_faithful : Faithful <| forgetToPresheafedSpace (C := C) where
-  map_injective h := h
 
 instance is_presheafedSpace_iso {X Y : SheafedSpace.{v} C} (f : X ⟶ Y) [IsIso f] :
     @IsIso (PresheafedSpace C) _ _ _ f :=
@@ -126,12 +129,8 @@ set_option linter.uppercaseLean3 false in
 
 @[simp]
 theorem id_c_app (X : SheafedSpace C) (U) :
-    (𝟙 X : X ⟶ X).c.app U =
-    eqToHom (by induction U using Opposite.rec' with | h U => ?_; cases U; rfl) := by
-  induction U using Opposite.rec' with | h U => ?_
-  cases U
-  simp only [id_c]
-  rw [eqToHom_app]
+    (𝟙 X : X ⟶ X).c.app U = eqToHom (by aesop_cat) := by
+  aesop_cat
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.SheafedSpace.id_c_app AlgebraicGeometry.SheafedSpace.id_c_app
 
@@ -233,7 +232,7 @@ noncomputable instance [HasLimits C] :
         (colimit.isoColimitCocone ⟨_, PresheafedSpace.colimitCoconeIsColimit _⟩).symm⟩⟩
 
 instance [HasLimits C] : HasColimits (SheafedSpace C) :=
-  has_colimits_of_has_colimits_creates_colimits forgetToPresheafedSpace
+  hasColimits_of_hasColimits_createsColimits forgetToPresheafedSpace
 
 noncomputable instance [HasLimits C] : PreservesColimits (forget C) :=
   Limits.compPreservesColimits forgetToPresheafedSpace (PresheafedSpace.forget C)

Mathlib/AlgebraicGeometry/Stalks.lean

@@ -25,21 +25,16 @@ noncomputable section
 
 universe v u v' u'
 
-open CategoryTheory
-
-open CategoryTheory.Limits CategoryTheory.Category CategoryTheory.Functor
-
-open AlgebraicGeometry
-
-open TopologicalSpace
-
-open Opposite
+open Opposite CategoryTheory CategoryTheory.Category CategoryTheory.Functor CategoryTheory.Limits
+  AlgebraicGeometry TopologicalSpace
 
 variable {C : Type u} [Category.{v} C] [HasColimits C]
 
 -- Porting note : no tidy tactic
 -- attribute [local tidy] tactic.op_induction' tactic.auto_cases_opens
-attribute [local aesop safe cases (rule_sets [CategoryTheory])] Opens
+-- this could be replaced by
+-- attribute [local aesop safe cases (rule_sets [CategoryTheory])] Opens
+-- but it doesn't appear to be needed here.
 
 open TopCat.Presheaf
 
@@ -60,7 +55,7 @@ def stalkMap {X Y : PresheafedSpace.{_, _, v} C} (α : X ⟶ Y) (x : X) :
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.PresheafedSpace.stalk_map AlgebraicGeometry.PresheafedSpace.stalkMap
 
-@[simp, elementwise, reassoc]
+@[elementwise (attr := simp), reassoc (attr := simp)]
 theorem stalkMap_germ {X Y : PresheafedSpace.{_, _, v} C} (α : X ⟶ Y) (U : Opens Y)
     (x : (Opens.map α.base).obj U) :
     Y.presheaf.germ ⟨α.base x.1, x.2⟩ ≫ stalkMap α ↑x = α.c.app (op U) ≫ X.presheaf.germ x := by
@@ -94,6 +89,8 @@ theorem restrictStalkIso_hom_eq_germ {U : TopCat} (X : PresheafedSpace.{_, _, v}
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.PresheafedSpace.restrict_stalk_iso_hom_eq_germ AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ
 
+-- We intentionally leave `simp` off the lemmas generated by `elementwise` and `reasssoc`,
+-- as the simpNF linter claims they never apply.
 @[simp, elementwise, reassoc]
 theorem restrictStalkIso_inv_eq_germ {U : TopCat} (X : PresheafedSpace.{_, _, v} C)
     {f : U ⟶ (X : TopCat.{v})} (h : OpenEmbedding f) (V : Opens U) (x : U) (hx : x ∈ V) :
@@ -108,7 +105,7 @@ theorem restrictStalkIso_inv_eq_ofRestrict {U : TopCat} (X : PresheafedSpace.{_,
     {f : U ⟶ (X : TopCat.{v})} (h : OpenEmbedding f) (x : U) :
     (X.restrictStalkIso h x).inv = stalkMap (X.ofRestrict h) x := by
   refine colimit.hom_ext fun V => ?_
-  induction V using Opposite.rec' with | h V => ?_
+  induction V with | h V => ?_
   let i : (h.isOpenMap.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V :=
     homOfLE (Set.image_preimage_subset f _)
   erw [Iso.comp_inv_eq, colimit.ι_map_assoc, colimit.ι_map_assoc, colimit.ι_pre]
@@ -137,7 +134,7 @@ theorem id (X : PresheafedSpace.{_, _, v} C) (x : X) :
   dsimp [stalkMap]
   simp only [stalkPushforward.id]
   erw [← map_comp]
-  convert(stalkFunctor C x).map_id X.presheaf
+  convert (stalkFunctor C x).map_id X.presheaf
   refine NatTrans.ext _ _ <| funext fun x => ?_
   simp only [id_c, id_comp, Pushforward.id_hom_app, op_obj, eqToHom_refl, map_id]
   rfl
@@ -151,7 +148,7 @@ theorem comp {X Y Z : PresheafedSpace.{_, _, v} C} (α : X ⟶ Y) (β : Y ⟶ Z)
         (stalkMap α x : Y.stalk (α.base x) ⟶ X.stalk x) := by
   dsimp [stalkMap, stalkFunctor, stalkPushforward]
   refine colimit.hom_ext fun U => ?_
-  induction U using Opposite.rec' with | h U => ?_
+  induction U with | h U => ?_
   cases U
   simp only [whiskeringLeft_obj_obj, comp_obj, op_obj, unop_op, OpenNhds.inclusion_obj,
     ι_colimMap_assoc, pushforwardObj_obj, Opens.map_comp_obj, whiskerLeft_app, comp_c_app,
@@ -207,8 +204,7 @@ instance isIso {X Y : PresheafedSpace.{_, _, v} C} (α : X ⟶ Y) [IsIso α] (x
       erw [← stalkMap.comp β α (α.base x)]
       rw [congr_hom _ _ (IsIso.inv_hom_id α), stalkMap.id, eqToHom_trans_assoc, eqToHom_refl,
         Category.id_comp]
-    ·
-      rw [Category.assoc, ← stalkMap.comp, congr_hom _ _ (IsIso.hom_inv_id α), stalkMap.id,
+    · rw [Category.assoc, ← stalkMap.comp, congr_hom _ _ (IsIso.hom_inv_id α), stalkMap.id,
         eqToHom_trans_assoc, eqToHom_refl, Category.id_comp]
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.PresheafedSpace.stalk_map.is_iso AlgebraicGeometry.PresheafedSpace.stalkMap.isIso
@@ -230,7 +226,7 @@ theorem stalkSpecializes_stalkMap {X Y : PresheafedSpace.{_, _, v} C}
   -- I had to uglify this
   dsimp [stalkSpecializes, stalkMap, stalkFunctor, stalkPushforward]
   refine colimit.hom_ext fun j => ?_
-  induction j using Opposite.rec' with | h j => ?_
+  induction j with | h j => ?_
   dsimp
   simp only [colimit.ι_desc_assoc, comp_obj, op_obj, unop_op, ι_colimMap_assoc, colimit.map_desc,
     OpenNhds.inclusion_obj, pushforwardObj_obj, whiskerLeft_app, OpenNhds.map_obj, whiskerRight_app,

Mathlib/CategoryTheory/Limits/Cones.lean

@@ -605,7 +605,6 @@ def whiskeringEquivalence (e : K ≌ J) : Cocone F ≌ Cocone (e.functor ⋙ F)
         Cocones.ext (Iso.refl _)
           (by
             intro k
-            dsimp
             simpa [e.counitInv_app_functor k] using s.w (e.unit.app k)))
       (by aesop_cat)
 #align category_theory.limits.cocones.whiskering_equivalence CategoryTheory.Limits.Cocones.whiskeringEquivalence
@@ -673,19 +672,13 @@ def functorialityEquivalence (e : C ≌ D) : Cocone F ≌ Cocone (F ⋙ e.functo
       NatIso.ofComponents (fun c => Cocones.ext (e.unitIso.app _) (by aesop_cat)) (by aesop_cat)
     counitIso :=
       NatIso.ofComponents
-        (fun c =>
-          Cocones.ext (e.counitIso.app _)
+        (fun c => Cocones.ext (e.counitIso.app _)
             (by
-              -- Unfortunately this doesn't work by `tidy`.
+              -- Unfortunately this doesn't work by `aesop_cat`.
               -- In this configuration `simp` reaches a dead-end and needs help.
               intro j
-              dsimp
-              simp only [← Equivalence.counitInv_app_functor, Iso.inv_hom_id_app, map_comp,
-                Equivalence.fun_inv_map, assoc, id_comp, Iso.inv_hom_id_app_assoc]
-              dsimp; simp))-- See note [dsimp, simp].
-      fun {c} {c'} f => by
-        apply CoconeMorphism.ext
-        simp
+              simp [← Equivalence.counitInv_app_functor]))
+      (by aesop_cat)
   }
 #align category_theory.limits.cocones.functoriality_equivalence CategoryTheory.Limits.Cocones.functorialityEquivalence
 
@@ -935,11 +928,7 @@ def coconeEquivalenceOpConeOp : Cocone F ≌ (Cone F.op)ᵒᵖ where
             apply ConeMorphism.w } }
   unitIso :=
     NatIso.ofComponents
-      (fun c =>
-        Cocones.ext (Iso.refl _)
-          (by
-            dsimp
-            simp))
+      (fun c => Cocones.ext (Iso.refl _) (by simp))
       fun {X} {Y} f => by
       apply CoconeMorphism.ext
       simp
@@ -949,17 +938,9 @@ def coconeEquivalenceOpConeOp : Cocone F ≌ (Cone F.op)ᵒᵖ where
         induction c using Opposite.rec'
         dsimp
         apply Iso.op
-        exact
-          Cones.ext (Iso.refl _)
-            (by
-              dsimp
-              simp))
+        exact Cones.ext (Iso.refl _) (by simp))
       fun {X} {Y} f =>
-      Quiver.Hom.unop_inj
-        (ConeMorphism.ext _ _
-          (by
-            dsimp
-            simp))
+      Quiver.Hom.unop_inj (ConeMorphism.ext _ _ (by simp))
   functor_unitIso_comp c := by
     apply Quiver.Hom.unop_inj
     apply ConeMorphism.ext

Mathlib/CategoryTheory/Limits/Creates.lean

@@ -172,10 +172,10 @@ theorem hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape (F : C ⥤ D)
 #align category_theory.has_limits_of_shape_of_has_limits_of_shape_creates_limits_of_shape CategoryTheory.hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape
 
 /-- If `F` creates limits, and `D` has all limits, then `C` has all limits. -/
-theorem has_limits_of_has_limits_creates_limits (F : C ⥤ D) [HasLimitsOfSize.{w, w'} D]
+theorem hasLimits_of_hasLimits_createsLimits (F : C ⥤ D) [HasLimitsOfSize.{w, w'} D]
     [CreatesLimitsOfSize.{w, w'} F] : HasLimitsOfSize.{w, w'} C :=
   ⟨fun _ _ => hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape F⟩
-#align category_theory.has_limits_of_has_limits_creates_limits CategoryTheory.has_limits_of_has_limits_creates_limits
+#align category_theory.has_limits_of_has_limits_creates_limits CategoryTheory.hasLimits_of_hasLimits_createsLimits
 
 -- Interface to the `CreatesColimit` class.
 /-- `liftColimit t` is the cocone for `K` given by lifting the colimit `t` for `K ⋙ F`. -/
@@ -213,10 +213,10 @@ theorem hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape (F : C 
 #align category_theory.has_colimits_of_shape_of_has_colimits_of_shape_creates_colimits_of_shape CategoryTheory.hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape
 
 /-- If `F` creates colimits, and `D` has all colimits, then `C` has all colimits. -/
-theorem has_colimits_of_has_colimits_creates_colimits (F : C ⥤ D) [HasColimitsOfSize.{w, w'} D]
+theorem hasColimits_of_hasColimits_createsColimits (F : C ⥤ D) [HasColimitsOfSize.{w, w'} D]
     [CreatesColimitsOfSize.{w, w'} F] : HasColimitsOfSize.{w, w'} C :=
   ⟨fun _ _ => hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape F⟩
-#align category_theory.has_colimits_of_has_colimits_creates_colimits CategoryTheory.has_colimits_of_has_colimits_creates_colimits
+#align category_theory.has_colimits_of_has_colimits_creates_colimits CategoryTheory.hasColimits_of_hasColimits_createsColimits
 
 instance (priority := 10) reflectsLimitsOfShapeOfCreatesLimitsOfShape (F : C ⥤ D)
     [CreatesLimitsOfShape J F] : ReflectsLimitsOfShape J F where