chore(category_theory/adjunction/*): making arguments implicit in adj…

…uction.comp and two small lemmas about mates (#15062)

Working on adjunctions between monads and comonads, I noticed that adjunction.comp was defined with having the functors of one of the adjunctions explicit as well as the adjunction. However in the library, only `adjunction.comp _ _` ever appears. Thus I found it natural to make these two arguments implicit, so that composition of adjunctions can now be written as `adj1.comp adj2` instead of `adj1.comp _ _ adj2`. 

Furthermore, I provide two lemmas about mates of natural transformations to and from the identity functor. The application I have in mind is to the unit/counit of a monad/comonad in case of an adjunction of monads and comonads, as studied already by Eilenberg and Moore.  



Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>

src/category_theory/adjunction/basic.lean

@@ -326,7 +326,7 @@ def left_adjoint_of_nat_iso {F G : C ⥤ D} (h : F ≅ G) [r : is_left_adjoint F
   adj := of_nat_iso_left r.adj h }
 
 section
-variables {E : Type u₃} [ℰ : category.{v₃} E] (H : D ⥤ E) (I : E ⥤ D)
+variables {E : Type u₃} [ℰ : category.{v₃} E] {H : D ⥤ E} {I : E ⥤ D}
 
 /--
 Composition of adjunctions.
@@ -344,13 +344,13 @@ def comp (adj₁ : F ⊣ G) (adj₂ : H ⊣ I) : F ⋙ H ⊣ I ⋙ G :=
 instance left_adjoint_of_comp {E : Type u₃} [ℰ : category.{v₃} E] (F : C ⥤ D) (G : D ⥤ E)
   [Fl : is_left_adjoint F] [Gl : is_left_adjoint G] : is_left_adjoint (F ⋙ G) :=
 { right := Gl.right ⋙ Fl.right,
-  adj := comp _ _ Fl.adj Gl.adj }
+  adj := Fl.adj.comp Gl.adj }
 
 /-- If `F` and `G` are right adjoints then `F ⋙ G` is a right adjoint too. -/
 instance right_adjoint_of_comp {E : Type u₃} [ℰ : category.{v₃} E] {F : C ⥤ D} {G : D ⥤ E}
   [Fr : is_right_adjoint F] [Gr : is_right_adjoint G] : is_right_adjoint (F ⋙ G) :=
 { left := Gr.left ⋙ Fr.left,
-  adj := comp _ _ Gr.adj Fr.adj }
+  adj := Gr.adj.comp Fr.adj }
 
 end
 

src/category_theory/adjunction/mates.lean

@@ -193,6 +193,21 @@ begin
     adj₂.counit_naturality, adj₂.left_triangle_components_assoc, assoc],
 end
 
+lemma transfer_nat_trans_self_adjunction_id {L R : C ⥤ C} (adj : L ⊣ R) (f : 𝟭 C ⟶ L) (X : C) :
+  (transfer_nat_trans_self adj adjunction.id f).app X = f.app (R.obj X) ≫ adj.counit.app X :=
+begin
+  dsimp [transfer_nat_trans_self, transfer_nat_trans, adjunction.id],
+  simp only [comp_id, id_comp],
+end
+
+lemma transfer_nat_trans_self_adjunction_id_symm {L R : C ⥤ C} (adj : L ⊣ R) (g : R ⟶ 𝟭 C)
+  (X : C) : ((transfer_nat_trans_self adj adjunction.id).symm g).app X =
+  adj.unit.app X ≫ (g.app (L.obj X)) :=
+begin
+  dsimp [transfer_nat_trans_self, transfer_nat_trans, adjunction.id],
+  simp only [comp_id, id_comp],
+end
+
 lemma transfer_nat_trans_self_symm_comp (f g) :
   (transfer_nat_trans_self adj₂ adj₁).symm f ≫ (transfer_nat_trans_self adj₃ adj₂).symm g =
     (transfer_nat_trans_self adj₃ adj₁).symm (g ≫ f) :=

src/category_theory/adjunction/over.lean

@@ -38,7 +38,7 @@ Note that the binary products assumption is necessary: the existence of a right
 `over.forget X` is equivalent to the existence of each binary product `X ⨯ -`.
 -/
 def forget_adj_star [has_binary_products C] : over.forget X ⊣ star X :=
-(coalgebra_equiv_over X).symm.to_adjunction.comp _ _ (adj _)
+(coalgebra_equiv_over X).symm.to_adjunction.comp (adj _)
 
 /--
 Note that the binary products assumption is necessary: the existence of a right adjoint to

src/category_theory/closed/functor.lean

@@ -133,8 +133,8 @@ attribute [instance] cartesian_closed_functor.comparison_iso
 
 lemma frobenius_morphism_mate (h : L ⊣ F) (A : C) :
   transfer_nat_trans_self
-    (h.comp _ _ (exp.adjunction A))
-    ((exp.adjunction (F.obj A)).comp _ _ h)
+    (h.comp (exp.adjunction A))
+    ((exp.adjunction (F.obj A)).comp h)
     (frobenius_morphism F h A) = exp_comparison F A :=
   begin
     rw ←equiv.eq_symm_apply,

src/category_theory/limits/over.lean

@@ -95,7 +95,7 @@ def pullback_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
   pullback (f ≫ g) ≅ pullback g ⋙ pullback f :=
 adjunction.right_adjoint_uniq
   (map_pullback_adj _)
-  (((map_pullback_adj _).comp _ _ (map_pullback_adj _)).of_nat_iso_left
+  (((map_pullback_adj _).comp (map_pullback_adj _)).of_nat_iso_left
     (over.map_comp _ _).symm)
 
 instance pullback_is_right_adjoint {A B : C} (f : A ⟶ B) :

src/category_theory/sites/adjunction.lean

@@ -98,7 +98,7 @@ abbreviation compose_and_sheafify_from_types (G : Type (max v u) ⥤ D) :
 is the forgetful functor to sheaves of types. -/
 def adjunction_to_types {G : Type (max v u) ⥤ D} (adj : G ⊣ forget D) :
   compose_and_sheafify_from_types J G ⊣ Sheaf_forget J :=
-adjunction.comp _ _ ((Sheaf_equiv_SheafOfTypes J).symm.to_adjunction) (adjunction J adj)
+((Sheaf_equiv_SheafOfTypes J).symm.to_adjunction).comp (adjunction J adj)
 
 @[simp]
 lemma adjunction_to_types_unit_app_val {G : Type (max v u) ⥤ D} (adj : G ⊣ forget D)

src/category_theory/sites/cover_preserving.lean

@@ -249,7 +249,7 @@ end
 /-- The pushforward functor is left adjoint to the pullback functor. -/
 def sites.pullback_pushforward_adjunction {G : C ⥤ D} (hG₁ : compatible_preserving K G)
   (hG₂ : cover_preserving J K G) : sites.pushforward A J K G ⊣ sites.pullback A hG₁ hG₂ :=
-((Lan.adjunction A G.op).comp _ _ (sheafification_adjunction K A)).restrict_fully_faithful
+((Lan.adjunction A G.op).comp (sheafification_adjunction K A)).restrict_fully_faithful
   (Sheaf_to_presheaf J A) (𝟭 _)
   (nat_iso.of_components (λ _, iso.refl _)
     (λ _ _ _,(category.comp_id _).trans (category.id_comp _).symm))

src/category_theory/subobject/mono_over.lean

@@ -388,7 +388,7 @@ end
 /-- `exists` is adjoint to `pullback` when images exist -/
 def exists_pullback_adj (f : X ⟶ Y) [has_pullbacks C] : «exists» f ⊣ pullback f :=
 adjunction.restrict_fully_faithful (forget X) (𝟭 _)
-  ((over.map_pullback_adj f).comp _ _ image_forget_adj)
+  ((over.map_pullback_adj f).comp image_forget_adj)
   (iso.refl _)
   (iso.refl _)