feat(CategoryTheory/EqToHom): simp lemmas for heq + eqToHom (#16779)

Some basic lemmas for working with `HEq` in `eqToHom` composites.

Co-Authored-By: Emily Riehl <[email protected]> and Pietro Monticone <[email protected]>



Co-authored-by: Mario Carneiro <[email protected]>

Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean

@@ -96,7 +96,7 @@ private theorem end_path : f x₁ = g x₃ := by convert hfg 1 <;> simp only [Pa
 
 theorem eq_path_of_eq_image :
     (πₘ f).map ⟦p⟧ = hcast (start_path hfg) ≫ (πₘ g).map ⟦q⟧ ≫ hcast (end_path hfg).symm := by
-  rw [Functor.conj_eqToHom_iff_heq
+  rw [conj_eqToHom_iff_heq
     ((πₘ f).map ⟦p⟧) ((πₘ g).map ⟦q⟧)
     (FundamentalGroupoid.ext <| start_path hfg)
     (FundamentalGroupoid.ext <| end_path hfg)]
@@ -178,7 +178,7 @@ theorem evalAt_eq (x : X) : ⟦H.evalAt x⟧ = hcast (H.apply_zero x).symm ≫
     (πₘ H.uliftMap).map (prodToProdTopI uhpath01 (𝟙 (fromTop x))) ≫
       hcast (H.apply_one x).symm.symm := by
   dsimp only [prodToProdTopI, uhpath01, hcast]
-  refine (@Functor.conj_eqToHom_iff_heq (πₓ Y) _ _ _ _ _ _ _ _
+  refine (@conj_eqToHom_iff_heq (πₓ Y) _ _ _ _ _ _ _ _
     (FundamentalGroupoid.ext <| H.apply_one x).symm).mpr ?_
   simp only [id_eq_path_refl, prodToProdTop_map, Path.Homotopic.prod_lift, map_eq, ←
     Path.Homotopic.map_lift]

Mathlib/CategoryTheory/EqToHom.lean

@@ -51,6 +51,18 @@ theorem eqToHom_trans {X Y Z : C} (p : X = Y) (q : Y = Z) :
   cases q
   simp
 
+/-- Two morphisms are conjugate via eqToHom if and only if they are heterogeneously equal.
+Note this used to be in the Functor namespace, where it doesn't belong. -/
+theorem conj_eqToHom_iff_heq {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) (h : W = Y) (h' : X = Z) :
+    f = eqToHom h ≫ g ≫ eqToHom h'.symm ↔ HEq f g := by
+  cases h
+  cases h'
+  simp
+
+theorem conj_eqToHom_iff_heq' {C} [Category C] {W X Y Z : C}
+    (f : W ⟶ X) (g : Y ⟶ Z) (h : W = Y) (h' : Z = X) :
+    f = eqToHom h ≫ g ≫ eqToHom h' ↔ HEq f g := conj_eqToHom_iff_heq _ _ _ h'.symm
+
 theorem comp_eqToHom_iff {X Y Y' : C} (p : Y = Y') (f : X ⟶ Y) (g : X ⟶ Y') :
     f ≫ eqToHom p = g ↔ f = g ≫ eqToHom p.symm :=
   { mp := fun h => h ▸ by simp
@@ -61,6 +73,41 @@ theorem eqToHom_comp_iff {X X' Y : C} (p : X = X') (f : X ⟶ Y) (g : X' ⟶ Y)
   { mp := fun h => h ▸ by simp
     mpr := fun h => h ▸ by simp [whisker_eq _ h] }
 
+theorem eqToHom_comp_heq {C} [Category C] {W X Y : C}
+    (f : Y ⟶ X) (h : W = Y) : HEq (eqToHom h ≫ f) f := by
+  rw [← conj_eqToHom_iff_heq _ _ h rfl, eqToHom_refl, Category.comp_id]
+
+@[simp] theorem eqToHom_comp_heq_iff {C} [Category C] {W X Y Z Z' : C}
+    (f : Y ⟶ X) (g : Z ⟶ Z') (h : W = Y) :
+    HEq (eqToHom h ≫ f) g ↔ HEq f g :=
+  ⟨(eqToHom_comp_heq ..).symm.trans, (eqToHom_comp_heq ..).trans⟩
+
+@[simp] theorem heq_eqToHom_comp_iff {C} [Category C] {W X Y Z Z' : C}
+    (f : Y ⟶ X) (g : Z ⟶ Z') (h : W = Y) :
+    HEq g (eqToHom h ≫ f) ↔ HEq g f :=
+  ⟨(·.trans (eqToHom_comp_heq ..)), (·.trans (eqToHom_comp_heq ..).symm)⟩
+
+theorem comp_eqToHom_heq {C} [Category C] {X Y Z : C}
+    (f : X ⟶ Y) (h : Y = Z) : HEq (f ≫ eqToHom h) f := by
+  rw [← conj_eqToHom_iff_heq' _ _ rfl h, eqToHom_refl, Category.id_comp]
+
+@[simp] theorem comp_eqToHom_heq_iff {C} [Category C] {W X Y Z Z' : C}
+    (f : X ⟶ Y) (g : Z ⟶ Z') (h : Y = W) :
+    HEq (f ≫ eqToHom h) g ↔ HEq f g :=
+  ⟨(comp_eqToHom_heq ..).symm.trans, (comp_eqToHom_heq ..).trans⟩
+
+@[simp] theorem heq_comp_eqToHom_iff {C} [Category C] {W X Y Z Z' : C}
+    (f : X ⟶ Y) (g : Z ⟶ Z') (h : Y = W) :
+    HEq g (f ≫ eqToHom h) ↔ HEq g f :=
+  ⟨(·.trans (comp_eqToHom_heq ..)), (·.trans (comp_eqToHom_heq ..).symm)⟩
+
+theorem heq_comp {C} [Category C] {X Y Z X' Y' Z' : C}
+    {f : X ⟶ Y} {g : Y ⟶ Z} {f' : X' ⟶ Y'} {g' : Y' ⟶ Z'}
+    (eq1 : X = X') (eq2 : Y = Y') (eq3 : Z = Z')
+    (H1 : HEq f f') (H2 : HEq g g') :
+    HEq (f ≫ g) (f' ≫ g') := by
+  cases eq1; cases eq2; cases eq3; cases H1; cases H2; rfl
+
 variable {β : Sort*}
 
 /-- We can push `eqToHom` to the left through families of morphisms. -/
@@ -197,13 +244,6 @@ lemma ext_of_iso {F G : C ⥤ D} (e : F ≅ G) (hobj : ∀ X, F.obj X = G.obj X)
     rw [← cancel_mono (e.hom.app Y), e.hom.naturality f, happ, happ, Category.assoc,
     Category.assoc, eqToHom_trans, eqToHom_refl, Category.comp_id])
 
-/-- Two morphisms are conjugate via eqToHom if and only if they are heterogeneously equal. -/
-theorem conj_eqToHom_iff_heq {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) (h : W = Y) (h' : X = Z) :
-    f = eqToHom h ≫ g ≫ eqToHom h'.symm ↔ HEq f g := by
-  cases h
-  cases h'
-  simp
-
 /-- Proving equality between functors using heterogeneous equality. -/
 theorem hext {F G : C ⥤ D} (h_obj : ∀ X, F.obj X = G.obj X)
     (h_map : ∀ (X Y) (f : X ⟶ Y), HEq (F.map f) (G.map f)) : F = G :=