feat(CategoryTheory/Limits/Cones): use to_dual (#35031)

This PR uses `to_dual` to generate `Cocone` from `Cone`.

Notes:
- Sadly, it is not possible to translate `cones : Cᵒᵖ ⥤ Type max u₁ v₃` and `cocones : C ⥤ Type max u₁ v₃` (and similarly `yoneda` and `coyoneda`), because one version has `ᵒᵖ` in the type and the other doesn't. To allow dualizing `Cone.extend`, I've inlined the definition of `Cone.extensions`.

- This PR makes many changes in other files where `to_dual` tags were missing. Only the minimal necessary changes have been made. Those files may be extended with more `to_dual` tags in future PRs.

- `Cone.extendIso` and `Cocone.extendIso` weren't compatible for `to_dual` because they were the other way around. I chose to swap the direction of the isomorphisms in `Cone.extendIso`. Similarly `precomposeEquivalence` and `postComposeEquivalence` weren't compatible. I chose to swap the direction of an isomorphism in `precomposeEquivalence`. These changes required a few adaptations in `Mathlib.CategoryTheory.Limits.IsLimit` and elsewhere.

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Author: JovanGerb

Mathlib/CategoryTheory/Category/Basic.lean

@@ -127,6 +127,7 @@ class CategoryStruct (obj : Type u) : Type max u (v + 1) extends Quiver.{v} obj
   comp : ∀ {X Y Z : obj}, (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
 
 attribute [trans, to_dual self (reorder := X Z, 6 7)] CategoryStruct.comp
+attribute [to_dual self (reorder := comp (X Z, 4 5))] CategoryStruct.mk
 
 initialize_simps_projections CategoryStruct (-toQuiver_Hom, -Hom)
 
@@ -244,6 +245,15 @@ attribute [simp, grind _=_] Category.assoc
 
 initialize_simps_projections Category (-Hom)
 
+/-- `Category.mk'` is the dual of `Category.mk`, which we need for `to_dual`.
+Please avoid using this directly. -/
+@[to_dual existing mk]
+abbrev Category.mk' {obj : Type u} [CategoryStruct.{v} obj]
+    (id_comp : ∀ {X Y : obj} (f : Y ⟶ X), f ≫ 𝟙 X = f)
+    (comp_id : ∀ {X Y : obj} (f : Y ⟶ X), 𝟙 Y ≫ f = f)
+    (assoc : ∀ {W X Y Z : obj} (f : X ⟶ W) (g : Y ⟶ X) (h : Z ⟶ Y), h ≫ g ≫ f = (h ≫ g) ≫ f) :
+    Category.{v, u} obj where
+
 example {C} [Category C] {X Y : C} (f : X ⟶ Y) : 𝟙 X ≫ f = f := by simp
 example {C} [Category C] {X Y : C} (f : X ⟶ Y) : f ≫ 𝟙 Y = f := by simp
 

Mathlib/CategoryTheory/Equivalence.lean

@@ -403,35 +403,23 @@ functor. -/
 def funInvIdAssoc (e : C ≌ D) (F : C ⥤ E) : e.functor ⋙ e.inverse ⋙ F ≅ F :=
   (Functor.associator _ _ _).symm ≪≫ isoWhiskerRight e.unitIso.symm F ≪≫ F.leftUnitor
 
-@[simp]
+@[to_dual (attr := simp) funInvIdAssoc_inv_app]
 theorem funInvIdAssoc_hom_app (e : C ≌ D) (F : C ⥤ E) (X : C) :
     (funInvIdAssoc e F).hom.app X = F.map (e.unitInv.app X) := by
   dsimp [funInvIdAssoc]
   simp
 
-@[simp]
-theorem funInvIdAssoc_inv_app (e : C ≌ D) (F : C ⥤ E) (X : C) :
-    (funInvIdAssoc e F).inv.app X = F.map (e.unit.app X) := by
-  dsimp [funInvIdAssoc]
-  simp
-
 /-- Composing a functor with both functors of an equivalence yields a naturally isomorphic
 functor. -/
 def invFunIdAssoc (e : C ≌ D) (F : D ⥤ E) : e.inverse ⋙ e.functor ⋙ F ≅ F :=
   (Functor.associator _ _ _).symm ≪≫ isoWhiskerRight e.counitIso F ≪≫ F.leftUnitor
 
-@[simp]
+@[to_dual (attr := simp) invFunIdAssoc_inv_app]
 theorem invFunIdAssoc_hom_app (e : C ≌ D) (F : D ⥤ E) (X : D) :
     (invFunIdAssoc e F).hom.app X = F.map (e.counit.app X) := by
   dsimp [invFunIdAssoc]
   simp
 
-@[simp]
-theorem invFunIdAssoc_inv_app (e : C ≌ D) (F : D ⥤ E) (X : D) :
-    (invFunIdAssoc e F).inv.app X = F.map (e.counitInv.app X) := by
-  dsimp [invFunIdAssoc]
-  simp
-
 /-- If `C` is equivalent to `D`, then `C ⥤ E` is equivalent to `D ⥤ E`. -/
 @[simps! functor inverse unitIso_hom_app unitIso_inv_app counitIso_hom_app counitIso_inv_app]
 def congrLeft (e : C ≌ D) : C ⥤ E ≌ D ⥤ E where

Mathlib/CategoryTheory/Functor/Basic.lean

@@ -57,6 +57,7 @@ attribute [simp] Functor.map_id Functor.map_comp
 attribute [grind =] Functor.map_id
 attribute [grind _=_] Functor.map_comp
 attribute [to_dual self] Functor.map Functor.map_comp
+attribute [to_dual self (reorder := map (X Y), map_comp (X Z, f g))] Functor.mk
 
 -- Note: We manually add this lemma which could be generated by `reassoc`,
 -- since we will import this file into `Mathlib/Tactic/CategoryTheory/Reassoc.lean`.

Mathlib/CategoryTheory/Functor/FullyFaithful.lean

@@ -45,16 +45,20 @@ namespace Functor
 class Full (F : C ⥤ D) : Prop where
   map_surjective {X Y : C} : Function.Surjective (F.map (X := X) (Y := Y))
 
+attribute [to_dual self] Full.map_surjective Full.mk
+
 /-- A functor `F : C ⥤ D` is faithful if for each `X Y : C`, `F.map` is injective. -/
 @[stacks 001C]
 class Faithful (F : C ⥤ D) : Prop where
   /-- `F.map` is injective for each `X Y : C`. -/
   map_injective : ∀ {X Y : C}, Function.Injective (F.map : (X ⟶ Y) → (F.obj X ⟶ F.obj Y)) := by
     cat_disch
 
+attribute [to_dual self] Faithful.map_injective Faithful.mk
+
 variable {X Y : C}
 
-@[grind inj]
+@[grind inj, to_dual self]
 theorem map_injective (F : C ⥤ D) [Faithful F] :
     Function.Injective <| (F.map : (X ⟶ Y) → (F.obj X ⟶ F.obj Y)) :=
   Faithful.map_injective
@@ -72,10 +76,11 @@ theorem map_surjective (F : C ⥤ D) [Full F] :
   Full.map_surjective
 
 /-- The choice of a preimage of a morphism under a full functor. -/
+@[to_dual self]
 noncomputable def preimage (F : C ⥤ D) [Full F] (f : F.obj X ⟶ F.obj Y) : X ⟶ Y :=
   (F.map_surjective f).choose
 
-@[simp]
+@[simp, to_dual self]
 theorem map_preimage (F : C ⥤ D) [Full F] {X Y : C} (f : F.obj X ⟶ F.obj Y) :
     F.map (preimage F f) = f :=
   (F.map_surjective f).choose_spec

Mathlib/CategoryTheory/Functor/ReflectsIso/Basic.lean

@@ -39,6 +39,8 @@ class Functor.ReflectsIsomorphisms (F : C ⥤ D) : Prop where
   /-- For any `f`, if `F.map f` is an iso, then so was `f`. -/
   reflects : ∀ {A B : C} (f : A ⟶ B) [IsIso (F.map f)], IsIso f
 
+attribute [to_dual self] Functor.ReflectsIsomorphisms.reflects Functor.ReflectsIsomorphisms.mk
+
 /-- If `F` reflects isos and `F.map f` is an iso, then `f` is an iso. -/
 theorem isIso_of_reflects_iso {A B : C} (f : A ⟶ B) (F : C ⥤ D) [IsIso (F.map f)]
     [F.ReflectsIsomorphisms] : IsIso f :=

Mathlib/CategoryTheory/Iso.lean

@@ -272,16 +272,16 @@ instance Iso.isIso_inv (e : X ≅ Y) : IsIso e.inv := e.symm.isIso_hom
 
 open IsIso
 
-/-- Reinterpret a morphism `f` with an `IsIso f` instance as an `Iso`. -/
-@[to_dual none]
+/-- Reinterpret a morphism `f : X ⟶ Y` with an `IsIso f` instance as `X ≅ Y`. -/
+@[to_dual asIso' /-- Reinterpret a morphism `f : X ⟶ Y` with an `IsIso f` instance as `Y ≅ X`. -/]
 noncomputable def asIso (f : X ⟶ Y) [IsIso f] : X ≅ Y :=
   ⟨f, inv f, hom_inv_id f, inv_hom_id f⟩
 
-@[simp, to_dual none]
+@[to_dual (attr := simp) asIso'_hom]
 theorem asIso_hom (f : X ⟶ Y) [IsIso f] : (asIso f).hom = f :=
   rfl
 
-@[simp, to_dual none]
+@[to_dual (attr := simp) asIso'_inv]
 theorem asIso_inv (f : X ⟶ Y) [IsIso f] : (asIso f).inv = inv f :=
   rfl