chore(category_theory/sites/*): Adjust some simp lemmas. (#10574)

The primary change is removing some `simp` tags from the definition of `sheafify` and friends, so that the sheafification related constructions are not unfolded to the `plus` constructions.

Also -- added coercion from Sheaves to presheaves, and some `rfl` simp lemmas which help some proofs move along.

Some proofs cleaned up as well.



Co-authored-by: Johan Commelin <johan@commelin.net>

src/category_theory/sites/adjunction.lean

@@ -82,20 +82,17 @@ adjunction.mk_of_hom_equiv
     symmetry,
     apply J.sheafify_lift_unique,
     dsimp [compose_equiv, adjunction.whisker_right],
-    erw [sheafification_map_sheafify_lift, to_sheafify_sheafify_lift],
+    erw [sheafify_map_sheafify_lift, to_sheafify_sheafify_lift],
     ext : 2,
     dsimp,
-    erw nat_trans.comp_app,
     simp,
   end,
   hom_equiv_naturality_right' := begin
     intros X Y Y' f g,
     dsimp [compose_equiv, adjunction.whisker_right],
     ext : 2,
-    erw [nat_trans.comp_app, nat_trans.comp_app, nat_trans.comp_app, nat_trans.comp_app],
     dsimp,
-    erw [nat_trans.comp_app f g],
-    simp only [category.id_comp, category.comp_id, category.assoc, functor.map_comp],
+    simp,
   end }
 
 @[simp]
@@ -153,7 +150,7 @@ lemma adjunction_to_types_hom_equiv_apply {G : Type (max v u) ⥤ D} (adj : G 
   (adj.whisker_right _).hom_equiv _ _ (J.to_sheafify _ ≫ η) := rfl
 
 @[simp]
-lemma adjunction_to_types_hom_equiv_symm_apply' {G : Type (max v u) ⥤ D} (adj : G ⊣ forget D)
+lemma adjunction_to_types_hom_equiv_symm_apply {G : Type (max v u) ⥤ D} (adj : G ⊣ forget D)
   (X : Sheaf J D) (Y : SheafOfTypes J) (η : Y ⟶ (Sheaf_forget J).obj X) :
   ((adjunction_to_types J adj).hom_equiv _ _).symm η =
   J.sheafify_lift (((adj.whisker_right _).hom_equiv _ _).symm η) X.2 := rfl

src/category_theory/sites/compatible_plus.lean

@@ -83,7 +83,7 @@ end) begin
   intros X Y f,
   apply (is_colimit_of_preserves F (colimit.is_colimit (J.diagram P X.unop))).hom_ext,
   intros W,
-  dsimp,
+  dsimp [plus_obj, plus_map],
   simp only [functor.map_comp, category.assoc],
   slice_rhs 1 2
   { erw (is_colimit_of_preserves F (colimit.is_colimit (J.diagram P X.unop))).fac },
@@ -123,18 +123,19 @@ begin
   simp,
 end
 
+@[simp, reassoc]
 lemma plus_comp_iso_whisker_left {F G : D ⥤ E} (η : F ⟶ G) (P : Cᵒᵖ ⥤ D)
   [∀ (X : C), preserves_colimits_of_shape (J.cover X)ᵒᵖ F]
   [∀ (X : C) (W : J.cover X) (P : Cᵒᵖ ⥤ D), preserves_limit (W.index P).multicospan F]
   [∀ (X : C), preserves_colimits_of_shape (J.cover X)ᵒᵖ G]
   [∀ (X : C) (W : J.cover X) (P : Cᵒᵖ ⥤ D), preserves_limit (W.index P).multicospan G] :
-  (J.plus_comp_iso F P).hom ≫ J.plus_map (whisker_left _ η) =
-  whisker_left _ η ≫ (J.plus_comp_iso G P).hom :=
+  whisker_left _ η ≫ (J.plus_comp_iso G P).hom =
+  (J.plus_comp_iso F P).hom ≫ J.plus_map (whisker_left _ η) :=
 begin
   ext X,
   apply (is_colimit_of_preserves F (colimit.is_colimit (J.diagram P X.unop))).hom_ext,
   intros W,
-  dsimp,
+  dsimp [plus_obj, plus_map],
   simp only [ι_plus_comp_iso_hom, ι_colim_map, whisker_left_app, ι_plus_comp_iso_hom_assoc,
     nat_trans.naturality_assoc, grothendieck_topology.diagram_nat_trans_app],
   simp only [← category.assoc],
@@ -145,30 +146,25 @@ begin
 end
 
 /-- The isomorphism between `P⁺ ⋙ F` and `(P ⋙ F)⁺`, functorially in `F`. -/
-@[simps hom inv]
+@[simps hom_app inv_app]
 def plus_functor_whisker_left_iso (P : Cᵒᵖ ⥤ D)
   [∀ (F : D ⥤ E) (X : C), preserves_colimits_of_shape (J.cover X)ᵒᵖ F]
   [∀ (F : D ⥤ E) (X : C) (W : J.cover X) (P : Cᵒᵖ ⥤ D),
     preserves_limit (W.index P).multicospan F] :
   (whiskering_left _ _ E).obj (J.plus_obj P) ≅
   (whiskering_left _ _ _).obj P ⋙ J.plus_functor E :=
 nat_iso.of_components
-(λ X, plus_comp_iso _ _ _)
-begin
-  intros F G η,
-  dsimp only [whiskering_left, functor.comp_map, plus_functor],
-  symmetry,
-  apply plus_comp_iso_whisker_left,
-end
+(λ X, plus_comp_iso _ _ _) $ λ F G η, plus_comp_iso_whisker_left _ _ _
 
+@[simp, reassoc]
 lemma plus_comp_iso_whisker_right {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) :
-  (J.plus_comp_iso F P).hom ≫ J.plus_map (whisker_right η F) =
-  whisker_right (J.plus_map η) F ≫ (J.plus_comp_iso F Q).hom :=
+  whisker_right (J.plus_map η) F ≫ (J.plus_comp_iso F Q).hom =
+  (J.plus_comp_iso F P).hom ≫ J.plus_map (whisker_right η F) :=
 begin
   ext X,
   apply (is_colimit_of_preserves F (colimit.is_colimit (J.diagram P X.unop))).hom_ext,
   intros W,
-  dsimp,
+  dsimp [plus_obj, plus_map],
   simp only [ι_colim_map, whisker_right_app, ι_plus_comp_iso_hom_assoc,
     grothendieck_topology.diagram_nat_trans_app],
   simp only [← category.assoc, ← F.map_comp],
@@ -186,23 +182,17 @@ begin
 end
 
 /-- The isomorphism between `P⁺ ⋙ F` and `(P ⋙ F)⁺`, functorially in `P`. -/
-@[simps hom inv]
+@[simps hom_app inv_app]
 def plus_functor_whisker_right_iso : J.plus_functor D ⋙ (whiskering_right _ _ _).obj F ≅
   (whiskering_right _ _ _).obj F ⋙ J.plus_functor E :=
-nat_iso.of_components (λ P, J.plus_comp_iso _ _)
-begin
-  intros P Q η,
-  dsimp only [whiskering_right, functor.comp_map, plus_functor],
-  symmetry,
-  apply plus_comp_iso_whisker_right,
-end
+nat_iso.of_components (λ P, J.plus_comp_iso _ _) $ λ P Q η, plus_comp_iso_whisker_right _ _ _
 
-@[simp]
+@[simp, reassoc]
 lemma whisker_right_to_plus_comp_plus_comp_iso_hom :
   whisker_right (J.to_plus _) _ ≫ (J.plus_comp_iso F P).hom = J.to_plus _ :=
 begin
   ext,
-  dsimp,
+  dsimp [to_plus],
   simp only [ι_plus_comp_iso_hom, functor.map_comp, category.assoc],
   simp only [← category.assoc],
   congr' 1,
@@ -216,17 +206,10 @@ end
 @[simp]
 lemma to_plus_comp_plus_comp_iso_inv : J.to_plus _ ≫ (J.plus_comp_iso F P).inv =
   whisker_right (J.to_plus _) _ :=
-begin
-  rw iso.comp_inv_eq,
-  simp,
-end
+by simp [iso.comp_inv_eq]
 
 lemma plus_comp_iso_inv_eq_plus_lift (hP : presheaf.is_sheaf J ((J.plus_obj P) ⋙ F)) :
   (J.plus_comp_iso F P).inv = J.plus_lift (whisker_right (J.to_plus _) _) hP :=
-begin
-  apply J.plus_lift_unique,
-  rw iso.comp_inv_eq,
-  simp,
-end
+by { apply J.plus_lift_unique, simp [iso.comp_inv_eq] }
 
 end category_theory.grothendieck_topology

src/category_theory/sites/compatible_sheafification.lean

@@ -114,20 +114,20 @@ begin
   erw category.id_comp,
 end
 
-@[simp]
+@[simp, reassoc]
 lemma whisker_right_to_sheafify_sheafify_comp_iso_hom :
   whisker_right (J.to_sheafify _) _ ≫ (J.sheafify_comp_iso F P).hom = J.to_sheafify _ :=
 begin
   dsimp [sheafify_comp_iso],
   erw [whisker_right_comp, category.assoc],
-  slice_lhs 2 3 { rw ← plus_comp_iso_whisker_right },
-  erw [category.assoc, ← (J.plus_functor _).map_comp,
+  slice_lhs 2 3 { rw plus_comp_iso_whisker_right },
+  rw [category.assoc, ← J.plus_map_comp,
     whisker_right_to_plus_comp_plus_comp_iso_hom, ← category.assoc,
     whisker_right_to_plus_comp_plus_comp_iso_hom],
   refl,
 end
 
-@[simp]
+@[simp, reassoc]
 lemma to_sheafify_comp_sheafify_comp_iso_inv :
   J.to_sheafify _ ≫ (J.sheafify_comp_iso F P).inv = whisker_right (J.to_sheafify _) _ :=
 by { rw iso.comp_inv_eq, simp }

src/category_theory/sites/cover_preserving.lean

@@ -145,6 +145,7 @@ begin
     rintros V f ⟨Z, f', g', h, rfl⟩,
     erw family_of_elements.comp_of_compatible (S.functor_pushforward G)
       hx' (image_mem_functor_pushforward G S h) g',
+    dsimp at ⊢ hy,
     simp [hG₁.apply_map (sheaf_over ℱ X) hx h, ←hy f' h] }
 end
 

src/category_theory/sites/limits.lean

@@ -25,9 +25,9 @@ we show that the cocone obtained by sheafifying the cocone point is a colimit co
 This allows us to show that `Sheaf J D` has colimits (of a certain shape) as soon as `D` does.
 
 -/
-namespace category_theory.Sheaf
+namespace category_theory
+namespace Sheaf
 
-open category_theory
 open category_theory.limits
 open opposite
 
@@ -214,4 +214,5 @@ instance [has_colimits D] : has_colimits (Sheaf J D) := ⟨infer_instance⟩
 
 end colimits
 
-end category_theory.Sheaf
+end Sheaf
+end category_theory

src/category_theory/sites/plus.lean

@@ -82,9 +82,7 @@ by { ext, dsimp, simp }
 variable [∀ (X : C), has_colimits_of_shape (J.cover X)ᵒᵖ D]
 
 /-- The plus construction, associating a presheaf to any presheaf.
-See `plus_functor` below for a functorial version.
--/
-@[simps]
+See `plus_functor` below for a functorial version. -/
 def plus_obj : Cᵒᵖ ⥤ D :=
 { obj := λ X, colimit (J.diagram P X.unop),
   map := λ X Y f, colim_map (J.diagram_pullback P f.unop) ≫ colimit.pre _ _,
@@ -126,12 +124,11 @@ def plus_obj : Cᵒᵖ ⥤ D :=
   end }
 
 /-- An auxiliary definition used in `plus` below. -/
-@[simps]
 def plus_map {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) : J.plus_obj P ⟶ J.plus_obj Q :=
 { app := λ X, colim_map (J.diagram_nat_trans η X.unop),
   naturality' := begin
     intros X Y f,
-    dsimp,
+    dsimp [plus_obj],
     ext,
     simp only [diagram_pullback_app, ι_colim_map, colimit.ι_pre_assoc,
       colimit.ι_pre, ι_colim_map_assoc, category.assoc],
@@ -145,9 +142,9 @@ def plus_map {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) : J.plus_obj P ⟶ J.plus_obj
 @[simp]
 lemma plus_map_id (P : Cᵒᵖ ⥤ D) : J.plus_map (𝟙 P) = 𝟙 _ :=
 begin
-  ext : 2,
-  dsimp only [plus_map],
-  rw J.diagram_nat_trans_id,
+  ext x : 2,
+  dsimp only [plus_map, plus_obj],
+  rw [J.diagram_nat_trans_id, nat_trans.id_app],
   ext,
   dsimp,
   simp,
@@ -179,13 +176,12 @@ variable {D}
 
 /-- The canonical map from `P` to `J.plus.obj P`.
 See `to_plus` for a functorial version. -/
-@[simps]
 def to_plus : P ⟶ J.plus_obj P :=
 { app := λ X, cover.to_multiequalizer (⊤ : J.cover X.unop) P ≫
     colimit.ι (J.diagram P X.unop) (op ⊤),
   naturality' := begin
     intros X Y f,
-    dsimp,
+    dsimp [plus_obj],
     delta cover.to_multiequalizer,
     simp only [diagram_pullback_app, colimit.ι_pre, ι_colim_map_assoc, category.assoc],
     dsimp only [functor.op, unop_op],
@@ -199,12 +195,12 @@ def to_plus : P ⟶ J.plus_obj P :=
     simp,
   end }
 
-@[simp]
+@[simp, reassoc]
 lemma to_plus_naturality {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) :
   η ≫ J.to_plus Q = J.to_plus _ ≫ J.plus_map η :=
 begin
   ext,
-  dsimp,
+  dsimp [to_plus, plus_map],
   delta cover.to_multiequalizer,
   simp only [ι_colim_map, category.assoc],
   simp_rw ← category.assoc,
@@ -229,7 +225,7 @@ variable {D}
 lemma plus_map_to_plus : J.plus_map (J.to_plus P) = J.to_plus (J.plus_obj P) :=
 begin
   ext X S,
-  dsimp,
+  dsimp [to_plus, plus_obj, plus_map],
   delta cover.to_multiequalizer,
   simp only [ι_colim_map],
   let e : S.unop ⟶ ⊤ := hom_of_le (order_top.le_top _),
@@ -278,11 +274,15 @@ end
 def iso_to_plus (hP : presheaf.is_sheaf J P) : P ≅ J.plus_obj P :=
 by letI := is_iso_to_plus_of_is_sheaf J P hP; exact as_iso (J.to_plus P)
 
+@[simp]
+lemma iso_to_plus_hom (hP : presheaf.is_sheaf J P) : (J.iso_to_plus P hP).hom = J.to_plus P := rfl
+
 /-- Lift a morphism `P ⟶ Q` to `P⁺ ⟶ Q` when `Q` is a sheaf. -/
 def plus_lift {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (hQ : presheaf.is_sheaf J Q) :
   J.plus_obj P ⟶ Q :=
 J.plus_map η ≫ (J.iso_to_plus Q hQ).inv
 
+@[simp, reassoc]
 lemma to_plus_plus_lift {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (hQ : presheaf.is_sheaf J Q) :
   J.to_plus P ≫ J.plus_lift η hQ = η :=
 begin
@@ -297,14 +297,9 @@ lemma plus_lift_unique {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (hQ : presheaf.is_sh
   (γ : J.plus_obj P ⟶ Q) (hγ : J.to_plus P ≫ γ = η) : γ = J.plus_lift η hQ :=
 begin
   dsimp only [plus_lift],
-  symmetry,
-  rw [iso.comp_inv_eq, ← hγ],
-  rw plus_map_comp,
-  dsimp only [iso_to_plus, as_iso],
-  rw to_plus_naturality,
-  congr' 1,
-  dsimp only [plus_functor, to_plus_nat_trans],
-  rw [J.plus_map_to_plus P],
+  rw [iso.eq_comp_inv, ← hγ, plus_map_comp],
+  dsimp,
+  simp,
 end
 
 lemma plus_hom_ext {P Q : Cᵒᵖ ⥤ D} (η γ : J.plus_obj P ⟶ Q) (hQ : presheaf.is_sheaf J Q)
@@ -316,4 +311,21 @@ begin
   apply plus_lift_unique, exact h
 end
 
+@[simp]
+lemma iso_to_plus_inv (hP : presheaf.is_sheaf J P) : (J.iso_to_plus P hP).inv =
+  J.plus_lift (𝟙 _) hP :=
+begin
+  apply J.plus_lift_unique,
+  rw [iso.comp_inv_eq, category.id_comp],
+  refl,
+end
+
+@[simp]
+lemma plus_map_plus_lift {P Q R : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (γ : Q ⟶ R) (hR : presheaf.is_sheaf J R) :
+  J.plus_map η ≫ J.plus_lift γ hR = J.plus_lift (η ≫ γ) hR :=
+begin
+  apply J.plus_lift_unique,
+  rw [← category.assoc, ← J.to_plus_naturality, category.assoc, J.to_plus_plus_lift],
+end
+
 end category_theory.grothendieck_topology

src/category_theory/sites/sheaf.lean

@@ -109,13 +109,25 @@ def Sheaf : Type* :=
 {P : Cᵒᵖ ⥤ A // presheaf.is_sheaf J P}
 
 /-- The inclusion functor from sheaves to presheaves. -/
-@[simps {rhs_md := semireducible}, derive [full, faithful]]
+@[simps map {rhs_md := semireducible}, derive [full, faithful]]
 def Sheaf_to_presheaf : Sheaf J A ⥤ (Cᵒᵖ ⥤ A) :=
 full_subcategory_inclusion (presheaf.is_sheaf J)
 
+namespace Sheaf
+
+@[simp] lemma id_app (X : Sheaf J A) (B : Cᵒᵖ) : (𝟙 X : X ⟶ X).app B = 𝟙 _ := rfl
+@[simp] lemma comp_app {X Y Z : Sheaf J A} (f : X ⟶ Y) (g : Y ⟶ Z) (B : Cᵒᵖ) :
+  (f ≫ g).app B = f.app B ≫ g.app B := rfl
+
+instance : has_coe (Sheaf J A) (Cᵒᵖ ⥤ A) := ⟨λ P, P.val⟩
+
+end Sheaf
+
+@[simp] lemma Sheaf_to_presheaf_obj (P : Sheaf J A) : (Sheaf_to_presheaf J A).obj P = P := rfl
+
 /-- The sheaf of sections guaranteed by the sheaf condition. -/
 @[simps] abbreviation sheaf_over {A : Type u₂} [category.{v₂} A] {J : grothendieck_topology C}
-  (ℱ : Sheaf J A) (X : A) : SheafOfTypes J := ⟨ℱ.val ⋙ coyoneda.obj (op X), ℱ.property X⟩
+  (ℱ : Sheaf J A) (X : A) : SheafOfTypes J := ⟨↑ℱ ⋙ coyoneda.obj (op X), ℱ.property X⟩
 
 lemma is_sheaf_iff_is_sheaf_of_type (P : Cᵒᵖ ⥤ Type w) :
   presheaf.is_sheaf J P ↔ presieve.is_sheaf J P :=

src/category_theory/sites/sheaf_of_types.lean

@@ -994,11 +994,25 @@ variables (J : grothendieck_topology C)
 def SheafOfTypes (J : grothendieck_topology C) : Type (max u₁ v₁ (w+1)) :=
 {P : Cᵒᵖ ⥤ Type w // presieve.is_sheaf J P}
 
+namespace SheafOfTypes
+
+@[simp] lemma id_app (X : SheafOfTypes J) (B : Cᵒᵖ) : (𝟙 X : X ⟶ X).app B = 𝟙 _ := rfl
+@[simp] lemma comp_app {X Y Z : SheafOfTypes J} (f : X ⟶ Y) (g : Y ⟶ Z) (B : Cᵒᵖ) :
+  (f ≫ g).app B = f.app B ≫ g.app B := rfl
+
+instance : has_coe (SheafOfTypes.{w} J) (Cᵒᵖ ⥤ Type w) := ⟨λ P, P.val⟩
+
+end SheafOfTypes
+
 /-- The inclusion functor from sheaves to presheaves. -/
-@[simps {rhs_md := semireducible}, derive [full, faithful]]
+@[simps map {rhs_md := semireducible}, derive [full, faithful]]
 def SheafOfTypes_to_presheaf : SheafOfTypes J ⥤ (Cᵒᵖ ⥤ Type w) :=
 full_subcategory_inclusion (presieve.is_sheaf J)
 
+@[simp]
+lemma SheafOfTypes_to_presheaf_obj (P : SheafOfTypes J) :
+  (SheafOfTypes_to_presheaf J).obj P = P := rfl
+
 /--
 The category of sheaves on the bottom (trivial) grothendieck topology is equivalent to the category
 of presheaves.