From 5e8abb78d8e909ce39ac02b5c7a203e6810cb589 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Sat, 14 Sep 2024 02:37:52 +0000 Subject: [PATCH] feat(CategoryTheory/EqToHom): simp lemmas for heq + eqToHom (#16779) Some basic lemmas for working with `HEq` in `eqToHom` composites. Co-Authored-By: Emily Riehl and Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Co-authored-by: Mario Carneiro --- .../FundamentalGroupoid/InducedMaps.lean | 4 +- Mathlib/CategoryTheory/EqToHom.lean | 54 ++++++++++++++++--- 2 files changed, 49 insertions(+), 9 deletions(-) diff --git a/Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean b/Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean index c47f77c73c988..d00c54679772a 100644 --- a/Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean +++ b/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] diff --git a/Mathlib/CategoryTheory/EqToHom.lean b/Mathlib/CategoryTheory/EqToHom.lean index 2c70a5bfcb94d..b9a92d8d2782b 100644 --- a/Mathlib/CategoryTheory/EqToHom.lean +++ b/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 :=