chore(CategoryTheory/Comma): API separation for StructuredArrow (#37809)

The categories of `StructuredArrow` and `Over` are a particular case of a comma category involving the identity functor or a constant functor. We introduce abbreviations which no longer involve terms like `(𝟭 _).obj _`. This allows to remove some `set_option backward.isDefEq.respectTransparency false`. This is a follow up to #37764.

Author: joelriou

Mathlib/Algebra/Category/Ring/Under/Basic.lean

@@ -143,7 +143,7 @@ variable (S) in
 def tensorProdObjIsoPushoutObj (A : Under R) :
     mkUnder S (S ⊗[R] A) ≅ (Under.pushout (ofHom <| algebraMap R S)).obj A :=
   Under.isoMk (CommRingCat.isPushout_tensorProduct R S A).flip.isoPushout <| by
-    simp only [Functor.const_obj_obj, Under.pushout_obj, Functor.id_obj, Under.mk_right,
+    simp only [Under.pushout_obj, Under.mk_right,
       mkUnder_hom, AlgHom.toRingHom_eq_coe, IsPushout.inr_isoPushout_hom, Under.mk_hom]
     rfl
 

Mathlib/AlgebraicGeometry/AffineTransitionLimit.lean

@@ -218,7 +218,7 @@ This is the underlying cone, and it is limiting as witnessed by `isLimitOpensCon
 @[simps] noncomputable
 def opensCone (i : I) (U : (D.obj i).Opens) : Cone (opensDiagram D i U) where
   pt := c.π.app i ⁻¹ᵁ U
-  π.app j := (c.π.app j.left).resLE _ _ (by rw [← Scheme.Hom.comp_preimage, c.w]; rfl)
+  π.app j := (c.π.app j.left).resLE _ _ (by rw [← Scheme.Hom.comp_preimage, c.w])
 
 attribute [local instance] CategoryTheory.isConnected_of_hasTerminal
 
@@ -251,8 +251,7 @@ instance [∀ {i j} (f : i ⟶ j), IsAffineHom (D.map f)] {i : I}
     · rintro ⟨⟨_, hU⟩, hV, rfl⟩
       convert hV
       exact Subtype.ext (by simp)
-  · simp only [Functor.id_obj, opensDiagram_obj, Functor.const_obj_obj,
-      Scheme.Opens.opensRange_ι]
+  · simp only [opensDiagram_obj, Scheme.Opens.opensRange_ι]
     rintro x ⟨⟨y, h₁ : (D.map k.hom).base y ∈ U⟩, h₂, e⟩
     obtain rfl : y = (D.map f.left).base x := congr($e)
     dsimp at h₁
@@ -320,7 +319,7 @@ lemma isBasis_preimage_isAffineOpen [IsCofiltered I] [∀ {i j} (f : i ⟶ j), I
       from (c.π.app i ⁻¹ᵁ V).topIso.commRingCatIsoToRingEquiv.symm_apply_eq.mp hs.symm using 3
     simp [Scheme.Hom.app_eq_appLE, Scheme.Hom.resLE_appLE]
   refine ⟨_, ⟨j.left, _, (hV.preimage _).basicOpen s, rfl⟩, ?_⟩
-  simp only [Functor.const_obj_obj, Functor.id_obj, Scheme.preimage_basicOpen] at this ⊢
+  simp only [Functor.const_obj_obj, Scheme.preimage_basicOpen] at this ⊢
   rw [← c.pt.basicOpen_res_eq _ (eqToHom h.symm).op, ← CommRingCat.comp_apply,
     Scheme.Hom.app_eq_appLE, Scheme.Hom.appLE_map, ← this]
   exact ⟨hxr, hrU⟩
@@ -1186,7 +1185,7 @@ lemma Scheme.exists_π_app_comp_eq_of_locallyOfFinitePresentation
     let t𝒱 (j : _) : opensDiagram D i' (𝒱' j) ⟶ (Functor.const (Over i')).obj j.1.1.2.1.2 :=
     { app k := (t.app k.left).resLE _ _ <| by
         refine (Hom.preimage_mono _ (hi' _)).trans ?_
-        simp only [Functor.id_obj, Functor.const_obj_obj, ← Hom.comp_preimage, t.naturality,
+        simp only [Functor.const_obj_obj, ← Hom.comp_preimage, t.naturality,
           Functor.const_obj_map, Category.comp_id, le_refl]
       naturality {k₁ k₂} f₁₂ := by simp [Hom.resLE_comp_resLE] }
     have (j : s) : IsAffine j.1.1.2.1.1 := j.1.1.2.prop.1

Mathlib/AlgebraicGeometry/ColimitsOver.lean

@@ -127,12 +127,14 @@ lemma isPullback {i j : 𝒰.I₀} (hij : i ⟶ j) :
       d.transitionMap hij := by
     apply (isColimitOfPreserves (Over.map _ (d.prop_trans hij)) (d.isColimit i)).hom_ext
     intro a
-    simp only [IsColimit.coconePointsIsoOfNatIso_hom, Iso.trans_hom, Functor.isoWhiskerLeft_hom,
-      iso1, ← Functor.map_comp_assoc, IsColimit.ι_map, Functor.mapCocone_pt,
-      Functor.mapCocone_ι_app, Functor.map_comp, Category.assoc, Adjunction.counit_naturality,
-      cocone_ι_transitionMap]
+    dsimp only [Functor.comp_obj, Functor.id_obj, Functor.mapCocone_pt, Functor.const_obj_obj,
+      Functor.mapCocone_ι_app, Iso.trans_hom, Functor.isoWhiskerLeft_hom, Iso.symm_hom]
+    rw [IsColimit.coconePointsIsoOfNatIso_hom, ← Functor.map_comp_assoc, IsColimit.ι_map,
+      Functor.mapCocone_ι_app, Functor.map_comp, Category.assoc,
+      Adjunction.counit_naturality, cocone_ι_transitionMap]
     ext
-    simp only [Comma.comp_hom, CategoryTheory.Comma.comp_left, ← Category.assoc]
+    dsimp
+    rw [Category.comp_id, ← Category.assoc]
     congr 1
     apply pullback.hom_ext <;> simp
   let iso2 : (d.cocone i).pt.left ≅ pullback (d.cocone j).pt.hom (𝒰.trans hij) :=

Mathlib/AlgebraicGeometry/Cover/Over.lean

@@ -143,8 +143,8 @@ def Cover.pullbackCoverOverProp : W.Cover (precoverage P) where
         ((PreservesPullback.iso (MorphismProperty.Over.forget Q _ _ ⋙ Over.forget S)
           (f.asOverProp S) ((𝒰.f _).asOverProp S)).inv)
         (PreservesPullback.iso_inv_fst _ _ _) x).mp hy
-    · dsimp only
-      rw [← Over.forget_map, MorphismProperty.Comma.toCommaMorphism_eq_hom,
+    · simp only [← CategoryTheory.Over.forget_map]
+      rw [MorphismProperty.Comma.toCommaMorphism_eq_hom,
         ← MorphismProperty.Comma.forget_map, ← Functor.comp_map]
       rw [← PreservesPullback.iso_hom_fst, P.cancel_left_of_respectsIso]
       exact P.pullback_fst _ _ (𝒰.map_prop j)
@@ -175,8 +175,8 @@ def Cover.pullbackCoverOverProp' : W.Cover (precoverage P) where
         ((PreservesPullback.iso (MorphismProperty.Over.forget Q _ _ ⋙ Over.forget S)
           ((𝒰.f _).asOverProp S) (f.asOverProp S)).inv)
         (PreservesPullback.iso_inv_snd _ _ _) x).mp hy
-    · dsimp only
-      rw [← Over.forget_map, MorphismProperty.Comma.toCommaMorphism_eq_hom,
+    · simp only [← CategoryTheory.Over.forget_map]
+      rw [MorphismProperty.Comma.toCommaMorphism_eq_hom,
         ← MorphismProperty.Comma.forget_map, ← Functor.comp_map]
       rw [← PreservesPullback.iso_hom_snd, P.cancel_left_of_respectsIso]
       exact P.pullback_snd _ _ (𝒰.map_prop j)

Mathlib/AlgebraicGeometry/Sites/Small.lean

@@ -58,7 +58,7 @@ lemma Cover.overEquiv_generate_toPresieveOver_eq_ofArrows {X : Over S}
     [𝒰.Over S] : Sieve.overEquiv X (Sieve.generate 𝒰.toPresieveOver) =
       Sieve.ofArrows 𝒰.X 𝒰.f := by
   ext V f
-  simp only [Sieve.overEquiv_iff, Functor.const_obj_obj, Sieve.generate_apply]
+  simp only [Sieve.overEquiv_iff, Sieve.generate_apply]
   constructor
   · rintro ⟨U, h, g, ⟨k⟩, hcomp⟩
     exact ⟨𝒰.X k, h.left, 𝒰.f k, ⟨k⟩, congrArg CommaMorphism.left hcomp⟩

Mathlib/CategoryTheory/Adjunction/Basic.lean

@@ -276,22 +276,21 @@ theorem right_triangle : whiskerLeft G adj.unit ≫ whiskerRight adj.counit G =
 
 @[reassoc (attr := simp)]
 theorem counit_naturality {X Y : D} (f : X ⟶ Y) :
-    F.map (G.map f) ≫ adj.counit.app Y = adj.counit.app X ≫ f :=
+    dsimp% F.map (G.map f) ≫ adj.counit.app Y = adj.counit.app X ≫ f :=
   adj.counit.naturality f
 
 @[reassoc (attr := simp)]
 theorem unit_naturality {X Y : C} (f : X ⟶ Y) :
-    adj.unit.app X ≫ G.map (F.map f) = f ≫ adj.unit.app Y :=
+    dsimp% adj.unit.app X ≫ G.map (F.map f) = f ≫ adj.unit.app Y :=
   (adj.unit.naturality f).symm
 
-set_option backward.isDefEq.respectTransparency false in
 lemma unit_comp_map_eq_iff {A : C} {B : D} (f : F.obj A ⟶ B) (g : A ⟶ G.obj B) :
-    adj.unit.app A ≫ G.map f = g ↔ f = F.map g ≫ adj.counit.app B :=
+    dsimp% adj.unit.app A ≫ G.map f = g ↔ f = F.map g ≫ adj.counit.app B :=
   ⟨fun h => by simp [← h], fun h => by simp [h]⟩
 
 set_option backward.isDefEq.respectTransparency false in
 lemma eq_unit_comp_map_iff {A : C} {B : D} (f : F.obj A ⟶ B) (g : A ⟶ G.obj B) :
-    g = adj.unit.app A ≫ G.map f ↔ F.map g ≫ adj.counit.app B = f :=
+    dsimp% g = adj.unit.app A ≫ G.map f ↔ F.map g ≫ adj.counit.app B = f :=
   ⟨fun h => by simp [h], fun h => by simp [← h]⟩
 
 theorem homEquiv_apply_eq {A : C} {B : D} (f : F.obj A ⟶ B) (g : A ⟶ G.obj B) :

Mathlib/CategoryTheory/Adjunction/Lifting/Left.lean

@@ -86,10 +86,9 @@ def counitCoequalises (h : ∀ X : B, RegularEpi (adj₁.counit.app X)) (X : B)
     refine ⟨((h X).desc' s.π ?_).1, ?_, ?_⟩
     · rw [← cancel_epi (adj₁.counit.app (h X).W)]
       rw [← adj₁.counit_naturality_assoc (h X).left]
-      dsimp only [Functor.comp_obj]
-      rw [← s.condition, ← F.map_comp_assoc, ← U.map_comp, RegularEpi.w, U.map_comp,
+      dsimp
+      rw [← dsimp% s.condition, ← F.map_comp_assoc, ← U.map_comp, RegularEpi.w, U.map_comp,
         F.map_comp_assoc, s.condition, ← adj₁.counit_naturality_assoc (h X).right]
-      simp
     · apply ((h X).desc' s.π _).2
     · intro m hm
       rw [← cancel_epi (adj₁.counit.app X)]
@@ -147,9 +146,10 @@ noncomputable def constructLeftAdjointEquiv (h : ∀ X : B, RegularEpi (adj₁.c
       rw [← (adj₂.homEquiv _ _).injective.eq_iff, eq_comm, adj₂.homEquiv_naturality_left,
         otherMap, assoc, adj₂.homEquiv_naturality_left, ← adj₂.counit_naturality,
         adj₂.homEquiv_naturality_left, adj₂.homEquiv_unit, adj₂.right_triangle_components,
-        comp_id, Functor.comp_map, ← U.map_comp, assoc, ← adj₁.counit_naturality,
-        adj₂.homEquiv_unit, adj₂.homEquiv_unit, F.map_comp, assoc]
-      rfl
+        comp_id, Functor.comp_map, ← U.map_comp, assoc]
+      dsimp
+      rw [← adj₁.counit_naturality]
+      simp [dsimp% adj₂.homEquiv_unit _ _ f ]
     _ ≃ { z : F.obj (U.obj X) ⟶ R.obj Y // _ } := by
       apply (adj₁.homEquiv _ _).symm.subtypeEquiv
       intro g

Mathlib/CategoryTheory/Bicategory/Kan/Adjunction.lean

@@ -237,7 +237,7 @@ def isKanOfWhiskerLeftAdjoint
           bicategory) <| by
     intro s' τ₀'
     let τ' : t.extension ≫ h ⟶ s'.extension := τ₀'.right
-    have Hτ' : t.unit ▷ h ⊗≫ f ◁ τ' = s'.unit := by simpa [bicategoricalComp] using τ₀'.w.symm
+    have Hτ' : t.unit ▷ h ⊗≫ f ◁ τ' = s'.unit := by simpa [bicategoricalComp] using τ₀'.w
     ext
     apply (H' _).hom_ext
     dsimp only [StructuredArrow.homMk_right]