chore(CategoryTheory/Comma/Arrow): use to_dual (leanprover-community#40862)

This PR uses `to_dual` to dualize the `Arrow` category.

Theorems `isIso_of_isIso` and `isIso_of_isIso'` did not have a dual, and had stronger iff forms, and weren't used, so I decided to remove them (or mark private).

I skipped the parts involving `eqToHom`, since `eqToHom` hasn't been tagged with `to_dual` yet.

Author: JovanGerb

Mathlib/CategoryTheory/Comma/Arrow.lean

@@ -33,7 +33,10 @@ variable (T) in
 squares in `T`. -/
 def Arrow := Comma (𝟭 T) (𝟭 T)
 
+to_dual_name_hint Left Right
+
 /-- The type of morphisms in the category `Arrow T`. -/
+@[to_dual self (reorder := f g)]
 protected def Arrow.Hom (f g : Arrow T) := CommaMorphism f g
 
 instance : Quiver (Arrow T) where
@@ -45,43 +48,31 @@ instance : Category (Arrow T) :=
 namespace Arrow
 
 /-- The left object of an arrow. -/
+@[to_dual /-- The right object of an arrow. -/]
 abbrev left (X : Arrow T) : T := Comma.left X
 
-/-- The right object of an arrow. -/
-abbrev right (X : Arrow T) : T := Comma.right X
-
 /-- Given `X : Arrow T`, this is the morphism `X.left ⟶ X.right`. -/
 abbrev hom (X : Arrow T) : X.left ⟶ X.right := Comma.hom X
 
 /-- The left part of a morphism in the category of arrows. -/
+@[to_dual /-- The right part of a morphism in the category of arrows. -/]
 abbrev Hom.left {X Y : Arrow T} (f : X ⟶ Y) : X.left ⟶ Y.left := CommaMorphism.left f
 
-/-- The right part of a morphism in the category of arrows. -/
-abbrev Hom.right {X Y : Arrow T} (f : X ⟶ Y) : X.right ⟶ Y.right := CommaMorphism.right f
-
-@[ext]
+@[ext, to_dual self (reorder := X Y, h₁ h₂)]
 lemma hom_ext {X Y : Arrow T} (f g : X ⟶ Y) (h₁ : f.left = g.left) (h₂ : f.right = g.right) :
     f = g :=
   CommaMorphism.ext h₁ h₂
 
-@[simp]
+@[to_dual (attr := simp)]
 theorem id_left (f : Arrow T) : Arrow.Hom.left (𝟙 f) = 𝟙 f.left :=
   rfl
 
-@[simp]
-theorem id_right (f : Arrow T) : Arrow.Hom.right (𝟙 f) = 𝟙 f.right :=
-  rfl
-
-@[simp, reassoc]
+@[to_dual (reorder := f g) (attr := simp, reassoc)]
 theorem comp_left {X Y Z : Arrow T} (f : X ⟶ Y) (g : Y ⟶ Z) :
     (f ≫ g).left = f.left ≫ g.left := rfl
 
-@[simp, reassoc]
-theorem comp_right {X Y Z : Arrow T} (f : X ⟶ Y) (g : Y ⟶ Z) :
-    (f ≫ g).right = f.right ≫ g.right := rfl
-
 /-- An object in the arrow category is simply a morphism in `T`. -/
-@[simps]
+@[simps, to_dual self]
 def mk {X Y : T} (f : X ⟶ Y) : Arrow T where
   left := X
   right := Y
@@ -92,38 +83,41 @@ theorem mk_eq (f : Arrow T) : Arrow.mk f.hom = f := by
   cases f
   rfl
 
+@[to_dual none]
 lemma mk_surjective (f : Arrow T) :
     ∃ (X Y : T) (g : X ⟶ Y), f = Arrow.mk g :=
   ⟨_, _, f.hom, rfl⟩
 
+@[to_dual self]
 theorem mk_injective (A B : T) :
     Function.Injective (Arrow.mk : (A ⟶ B) → Arrow T) := fun f g h => by
   cases h
   rfl
 
+@[to_dual self]
 theorem mk_inj (A B : T) {f g : A ⟶ B} : Arrow.mk f = Arrow.mk g ↔ f = g :=
   (mk_injective A B).eq_iff
 
+@[to_dual self]
 instance {X Y : T} : CoeOut (X ⟶ Y) (Arrow T) where
   coe := mk
 
-@[reassoc (attr := simp high)]
+@[to_dual none, reassoc (attr := simp high)]
 theorem w {f g : Arrow T} (sq : f ⟶ g) : sq.left ≫ g.hom = f.hom ≫ sq.right :=
   CommaMorphism.w sq
 
-@[reassoc]
-lemma Hom.w {f g : Arrow T} (sq : f ⟶ g) : sq.left ≫ g.hom = f.hom ≫ sq.right := by
-  simp
+@[to_dual none, reassoc]
+alias Hom.w := w
 
+@[to_dual]
 theorem hom.congr_left {f g : Arrow T} {φ₁ φ₂ : f ⟶ g} (h : φ₁ = φ₂) : φ₁.left = φ₂.left := by
   rw [h]
 
-theorem hom.congr_right {f g : Arrow T} {φ₁ φ₂ : f ⟶ g} (h : φ₁ = φ₂) : φ₁.right = φ₂.right := by
-  simp [h]
-
+@[to_dual none]
 theorem iso_w {f g : Arrow T} (e : f ≅ g) : g.hom = e.inv.left ≫ f.hom ≫ e.hom.right := by
   simp [← Arrow.comp_right]
 
+@[to_dual none]
 theorem iso_w' {W X Y Z : T} {f : W ⟶ X} {g : Y ⟶ Z} (e : Arrow.mk f ≅ Arrow.mk g) :
     g = e.inv.left ≫ f ≫ e.hom.right :=
   iso_w e
@@ -171,6 +165,14 @@ def homMk {f g : Arrow T} (u : f.left ⟶ g.left) (v : f.right ⟶ g.right)
   right := v
   w := w
 
+/-- `homMk''` is the dual of `homMk`, which we need for `to_dual`.
+Please avoid using this directly. -/
+@[to_dual existing homMk]
+abbrev homMk'' {f g : Arrow T} (u : g.right ⟶ f.right) (v : g.left ⟶ f.left)
+    (w : g.hom ≫ u = v ≫ f.hom := by cat_disch) : g ⟶ f :=
+  homMk v u
+attribute [to_dual none] homMk_left homMk_right
+
 /-- We can also build a morphism in the arrow category out of any commutative square in `T`. -/
 @[simps]
 def homMk' {X Y : T} {f : X ⟶ Y} {P Q : T} {g : P ⟶ Q} (u : X ⟶ P) (v : Y ⟶ Q)
@@ -180,24 +182,33 @@ def homMk' {X Y : T} {f : X ⟶ Y} {P Q : T} {g : P ⟶ Q} (u : X ⟶ P) (v : Y
   right := v
   w := w
 
+/-- `homMk'''` is the dual of `homMk'`, which we need for `to_dual`.
+Please avoid using this directly. -/
+@[to_dual existing homMk']
+abbrev homMk''' {X Y : T} {f : Y ⟶ X} {P Q : T} {g : Q ⟶ P} (u : P ⟶ X) (v : Q ⟶ Y)
+    (w : g ≫ u = v ≫ f := by cat_disch) : mk g ⟶ mk f :=
+  homMk' v u
+attribute [to_dual none] homMk'_left
+
 set_option backward.defeqAttrib.useBackward true in
-@[reassoc]
+@[to_dual none, reassoc]
 theorem w_mk_left {X Y : T} {f : X ⟶ Y} {g : Arrow T} (sq : mk f ⟶ g) :
     dsimp% sq.left ≫ g.hom = f ≫ sq.right :=
   sq.w
 
 set_option backward.defeqAttrib.useBackward true in
-@[reassoc (attr := simp)]
+@[to_dual none, reassoc (attr := simp)]
 theorem w_mk_right {f : Arrow T} {X Y : T} {g : X ⟶ Y} (sq : f ⟶ mk g) :
     dsimp% sq.left ≫ g = f.hom ≫ sq.right :=
   sq.w
 
 set_option backward.defeqAttrib.useBackward true in
-@[reassoc]
+@[to_dual none, reassoc]
 theorem w_mk {X Y X' Y' : T} {f : X ⟶ Y} {g : X' ⟶ Y'} (sq : mk f ⟶ mk g) :
     dsimp% sq.left ≫ g = f ≫ sq.right :=
   sq.w
 
+@[to_dual self (reorder := f g, 6 7)]
 theorem isIso_of_isIso_left_of_isIso_right {f g : Arrow T} (ff : f ⟶ g) [IsIso ff.left]
     [IsIso ff.right] : IsIso ff where
   out := ⟨homMk (inv ff.left) (inv ff.right), by cat_disch⟩
@@ -210,59 +221,70 @@ def isoMk {f g : Arrow T} (l : f.left ≅ g.left) (r : f.right ≅ g.right)
     (h : l.hom ≫ g.hom = f.hom ≫ r.hom := by cat_disch) : f ≅ g :=
   Comma.isoMk l r h
 
+/-- `isoMk''` is the dual of `isoMk`, which we need for `to_dual`.
+Please avoid using this directly. -/
+@[to_dual existing isoMk]
+abbrev isoMk'' {f g : Arrow T} (l : f.right ≅ g.right) (r : f.left ≅ g.left)
+    (h : g.hom ≫ l.inv = r.inv ≫ f.hom := by cat_disch) : f ≅ g :=
+  isoMk r l (by rwa [Iso.comp_inv_eq, Category.assoc, Iso.eq_inv_comp] at h)
+attribute [to_dual none] isoMk_hom_left isoMk_hom_right isoMk_inv_left isoMk_inv_right
+
 /-- A variant of `Arrow.isoMk` that creates an iso between two `Arrow.mk`s with a better type
 signature. -/
 abbrev isoMk' {W X Y Z : T} (f : W ⟶ X) (g : Y ⟶ Z) (e₁ : W ≅ Y) (e₂ : X ≅ Z)
     (h : e₁.hom ≫ g = f ≫ e₂.hom := by cat_disch) : Arrow.mk f ≅ Arrow.mk g :=
   Arrow.isoMk e₁ e₂ h
 
+/-- `isoMk'''` is the dual of `isoMk'`, which we need for `to_dual`.
+Please avoid using this directly. -/
+@[to_dual existing isoMk']
+abbrev isoMk''' {W X Y Z : T} (f : X ⟶ W) (g : Z ⟶ Y) (e₁ : W ≅ Y)
+  (e₂ : X ≅ Z) (h : g ≫ e₁.inv = e₂.inv ≫ f := by cat_disch) : mk f ≅ mk g :=
+  isoMk' f g e₂ e₁ (by rwa [Iso.comp_inv_eq, Category.assoc, Iso.eq_inv_comp] at h)
+
 section
 
 variable {f g : Arrow T} (sq : f ⟶ g)
 
+@[to_dual]
 instance isIso_left [IsIso sq] : IsIso sq.left :=
   ⟨(inv sq).left, by simp [← comp_left]⟩
 
-instance isIso_right [IsIso sq] : IsIso sq.right :=
-  ⟨(inv sq).right, by simp [← comp_right]⟩
-
-lemma isIso_of_isIso' {f g : Arrow T} (sq : f ⟶ g) [IsIso sq] [IsIso f.hom] :
+@[to_dual none]
+private lemma isIso_of_isIso' {f g : Arrow T} (sq : f ⟶ g) [IsIso sq] [IsIso f.hom] :
     IsIso g.hom := by
   rw [iso_w (asIso sq)]
   infer_instance
 
-lemma isIso_of_isIso {X Y : T} {f : X ⟶ Y} {g : Arrow T} (sq : mk f ⟶ g) [IsIso sq] [IsIso f] :
-    IsIso g.hom := by
-  have : IsIso (mk f).hom := by assumption
-  apply isIso_of_isIso' sq
-
+@[to_dual none]
 lemma isIso_hom_iff_isIso_hom_of_isIso {f g : Arrow T} (sq : f ⟶ g) [IsIso sq] :
     IsIso f.hom ↔ IsIso g.hom :=
   ⟨fun _ => isIso_of_isIso' sq, fun _ => isIso_of_isIso' (inv sq)⟩
 
+@[to_dual none]
 lemma isIso_iff_isIso_of_isIso {W X Y Z : T} {f : W ⟶ X} {g : Y ⟶ Z} (sq : mk f ⟶ mk g) [IsIso sq] :
     IsIso f ↔ IsIso g :=
   isIso_hom_iff_isIso_hom_of_isIso sq
 
+@[to_dual none]
 lemma isIso_hom_iff_isIso_of_isIso {Y Z : T} {f : Arrow T} {g : Y ⟶ Z} (sq : f ⟶ mk g) [IsIso sq] :
     IsIso f.hom ↔ IsIso g :=
   isIso_hom_iff_isIso_hom_of_isIso sq
 
-@[simp]
+@[to_dual (attr := simp, push ←)]
 theorem inv_left [IsIso sq] : (inv sq).left = inv sq.left :=
   IsIso.eq_inv_of_hom_inv_id (by simp [← comp_left])
 
-@[simp]
-theorem inv_right [IsIso sq] : (inv sq).right = inv sq.right :=
-  IsIso.eq_inv_of_hom_inv_id (by simp [← comp_right])
-
+@[to_dual none]
 theorem left_hom_inv_right [IsIso sq] : sq.left ≫ g.hom ≫ inv sq.right = f.hom := by
   simp only [← Category.assoc, IsIso.comp_inv_eq, w]
 
+@[to_dual none]
 theorem inv_left_hom_right [IsIso sq] : inv sq.left ≫ f.hom ≫ sq.right = g.hom := by
   simp only [w, IsIso.inv_comp_eq]
 
 set_option backward.defeqAttrib.useBackward true in
+@[to_dual epi_right]
 instance mono_left [Mono sq] : Mono sq.left where
   right_cancellation {Z} φ ψ h := by
     let aux : (Z ⟶ f.left) → (Arrow.mk (𝟙 Z) ⟶ f) := fun φ =>
@@ -276,34 +298,14 @@ instance mono_left [Mono sq] : Mono sq.left where
     · exact h
     · simp [this, ← Arrow.w_mk_right, reassoc_of% h]
 
-set_option backward.defeqAttrib.useBackward true in
-instance epi_right [Epi sq] : Epi sq.right where
-  left_cancellation {Z} φ ψ h := by
-    let aux : (g.right ⟶ Z) → (g ⟶ Arrow.mk (𝟙 Z)) := fun φ =>
-      Arrow.homMk (g.hom ≫ φ) φ
-    change (aux φ).right = (aux ψ).right
-    congr 1
-    rw [← cancel_epi sq]
-    ext
-    · simp only [comp_left, comp_left, aux, mk_left, homMk_left, w_assoc, h]
-    · exact h
-
-@[reassoc (attr := simp)]
+@[to_dual (attr := reassoc (attr := simp))]
 lemma hom_inv_id_left (e : f ≅ g) : e.hom.left ≫ e.inv.left = 𝟙 _ := by
   rw [← comp_left, e.hom_inv_id, id_left]
 
-@[reassoc (attr := simp)]
+@[to_dual (attr := reassoc (attr := simp))]
 lemma inv_hom_id_left (e : f ≅ g) : e.inv.left ≫ e.hom.left = 𝟙 _ := by
   rw [← comp_left, e.inv_hom_id, id_left]
 
-@[reassoc (attr := simp)]
-lemma hom_inv_id_right (e : f ≅ g) : e.hom.right ≫ e.inv.right = 𝟙 _ := by
-  rw [← comp_right, e.hom_inv_id, id_right]
-
-@[reassoc (attr := simp)]
-lemma inv_hom_id_right (e : f ≅ g) : e.inv.right ≫ e.hom.right = 𝟙 _ := by
-  rw [← comp_right, e.inv_hom_id, id_right]
-
 end
 
 /-- Given a square from an arrow `i` to an isomorphism `p`, express the source part of `sq`
@@ -338,15 +340,10 @@ def squareToSnd {X Y Z : C} {i : Arrow C} {f : X ⟶ Y} {g : Y ⟶ Z} (sq : i 
   Arrow.homMk (sq.left ≫ f) (sq.right) (by simp [w_mk sq])
 
 /-- The functor sending an arrow to its source. -/
-@[simps!]
+@[to_dual (attr := simps!) /-- The functor sending an arrow to its target. -/]
 def leftFunc : Arrow C ⥤ C :=
   Comma.fst _ _
 
-/-- The functor sending an arrow to its target. -/
-@[simps!]
-def rightFunc : Arrow C ⥤ C :=
-  Comma.snd _ _
-
 set_option backward.defeqAttrib.useBackward true in
 /-- The natural transformation from `leftFunc` to `rightFunc`, given by the arrow itself. -/
 @[simps]
@@ -365,7 +362,9 @@ set_option backward.defeqAttrib.useBackward true in
 @[simps]
 def mapArrow (F : C ⥤ D) : Arrow C ⥤ Arrow D where
   obj a := Arrow.mk (F.map a.hom)
-  map f := Arrow.homMk (F.map f.left) (F.map f.right) (by simp [← Functor.map_comp])
+  map {X Y} f := Arrow.homMk (F.map f.left) (F.map f.right) (by simp [← Functor.map_comp])
+
+attribute [to_dual self (reorder := X Y)] mapArrow_map
 
 variable (C D)
 
@@ -375,7 +374,9 @@ a functor `F : C ⥤ D` to `F.mapArrow`. -/
 @[simps]
 def mapArrowFunctor : (C ⥤ D) ⥤ (Arrow C ⥤ Arrow D) where
   obj F := F.mapArrow
-  map τ := { app f := Arrow.homMk (τ.app _) (τ.app _) }
+  map {X Y} τ := { app f := Arrow.homMk (τ.app _) (τ.app _) }
+
+attribute [to_dual self (reorder := X Y)] mapArrowFunctor_map_app
 
 variable {C D}
 
@@ -431,6 +432,7 @@ def Arrow.discreteEquiv (S : Type u) : Arrow (Discrete S) ≃ S where
 
 /-- Extensionality lemma for functors `C ⥤ D` which uses as an assumption
 that the induced maps `Arrow C → Arrow D` coincide. -/
+@[to_dual self]
 lemma Arrow.functor_ext {F G : C ⥤ D} (h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
     F.mapArrow.obj (Arrow.mk f) = G.mapArrow.obj (Arrow.mk f)) :
     F = G :=