From 332029ee16836fa46236ca2a52b29658a71a4f38 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Sun, 4 Feb 2024 17:06:40 +0100 Subject: [PATCH 1/3] Extract --- .../CategoryTheory/Comma/StructuredArrow.lean | 22 +++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/Mathlib/CategoryTheory/Comma/StructuredArrow.lean b/Mathlib/CategoryTheory/Comma/StructuredArrow.lean index faf7dc7e3ccbe..4e2baa2a4abdb 100644 --- a/Mathlib/CategoryTheory/Comma/StructuredArrow.lean +++ b/Mathlib/CategoryTheory/Comma/StructuredArrow.lean @@ -147,6 +147,17 @@ lemma homMk'_mk_comp (f : S ⟶ T.obj Y) (g : Y ⟶ Y') (g' : Y' ⟶ Y'') : homMk' (mk f) (g ≫ g') = homMk' (mk f) g ≫ homMk' (mk (f ≫ T.map g)) g' ≫ eqToHom (by simp) := homMk'_comp _ _ _ +/-- Variant of `homMk'` where both objects are application of `mk`. -/ +@[simps] +def mkPostcomp (f : S ⟶ T.obj Y) (g : Y ⟶ Y') : mk f ⟶ mk (f ≫ T.map g) where + left := eqToHom (by ext) + right := g + +lemma mkPostcomp_id (f : S ⟶ T.obj Y) : mkPostcomp f (𝟙 Y) = eqToHom (by aesop_cat) := by aesop_cat +lemma mkPostcomp_comp (f : S ⟶ T.obj Y) (g : Y ⟶ Y') (g' : Y' ⟶ Y'') : + mkPostcomp f (g ≫ g') = mkPostcomp f g ≫ mkPostcomp (f ≫ T.map g) g' ≫ eqToHom (by simp) := by + aesop_cat + /-- To construct an isomorphism of structured arrows, we need an isomorphism of the objects underlying the target, and to check that the triangle commutes. @@ -476,6 +487,17 @@ lemma homMk'_mk_comp (f : S.obj Y ⟶ T) (g : Y' ⟶ Y) (g' : Y'' ⟶ Y') : homMk' (mk f) (g' ≫ g) = eqToHom (by simp) ≫ homMk' (mk (S.map g ≫ f)) g' ≫ homMk' (mk f) g := homMk'_comp _ _ _ +/-- Variant of `homMk'` where both objects are applications of `mk`. -/ +@[simps] +def mkPrecomp (f : S.obj Y ⟶ T) (g : Y' ⟶ Y) : mk (S.map g ≫ f) ⟶ mk f where + left := g + right := eqToHom (by ext) + +lemma mkPrecomp_id (f : S.obj Y ⟶ T) : mkPrecomp f (𝟙 Y) = eqToHom (by aesop_cat) := by aesop_cat +lemma mkPrecomp_comp (f : S.obj Y ⟶ T) (g : Y' ⟶ Y) (g' : Y'' ⟶ Y') : + mkPrecomp f (g' ≫ g) = eqToHom (by simp) ≫ mkPrecomp (S.map g ≫ f) g' ≫ mkPrecomp f g := by + aesop_cat + /-- To construct an isomorphism of costructured arrows, we need an isomorphism of the objects underlying the source, and to check that the triangle commutes. From a866a824337c5bb351be26f0c1d75bdb1728355e Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Sun, 4 Feb 2024 17:07:30 +0100 Subject: [PATCH 2/3] Fix typo --- Mathlib/CategoryTheory/Comma/StructuredArrow.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/Comma/StructuredArrow.lean b/Mathlib/CategoryTheory/Comma/StructuredArrow.lean index 4e2baa2a4abdb..df2e961e7816b 100644 --- a/Mathlib/CategoryTheory/Comma/StructuredArrow.lean +++ b/Mathlib/CategoryTheory/Comma/StructuredArrow.lean @@ -147,7 +147,7 @@ lemma homMk'_mk_comp (f : S ⟶ T.obj Y) (g : Y ⟶ Y') (g' : Y' ⟶ Y'') : homMk' (mk f) (g ≫ g') = homMk' (mk f) g ≫ homMk' (mk (f ≫ T.map g)) g' ≫ eqToHom (by simp) := homMk'_comp _ _ _ -/-- Variant of `homMk'` where both objects are application of `mk`. -/ +/-- Variant of `homMk'` where both objects are applications of `mk`. -/ @[simps] def mkPostcomp (f : S ⟶ T.obj Y) (g : Y ⟶ Y') : mk f ⟶ mk (f ≫ T.map g) where left := eqToHom (by ext) From abd55c87942197b20d9029d08dd2274e137cee02 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Sun, 4 Feb 2024 17:46:54 +0100 Subject: [PATCH 3/3] Remove unnecessary eqToHom as pointed out in code review --- .../CategoryTheory/Comma/StructuredArrow.lean | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/Mathlib/CategoryTheory/Comma/StructuredArrow.lean b/Mathlib/CategoryTheory/Comma/StructuredArrow.lean index df2e961e7816b..bf1765a01c766 100644 --- a/Mathlib/CategoryTheory/Comma/StructuredArrow.lean +++ b/Mathlib/CategoryTheory/Comma/StructuredArrow.lean @@ -112,7 +112,7 @@ and to check that the triangle commutes. @[simps] def homMk {f f' : StructuredArrow S T} (g : f.right ⟶ f'.right) (w : f.hom ≫ T.map g = f'.hom := by aesop_cat) : f ⟶ f' where - left := eqToHom (by ext) + left := 𝟙 _ right := g w := by dsimp @@ -127,7 +127,7 @@ attribute [-simp, nolint simpNF] homMk_left structured arrows given by `(X ⟶ T(Y)) ⟶ (X ⟶ T(Y) ⟶ T(Y'))`. -/ @[simps] def homMk' (f : StructuredArrow S T) (g : f.right ⟶ Y') : f ⟶ mk (f.hom ≫ T.map g) where - left := eqToHom (by ext) + left := 𝟙 _ right := g #align category_theory.structured_arrow.hom_mk' CategoryTheory.StructuredArrow.homMk' @@ -150,7 +150,7 @@ lemma homMk'_mk_comp (f : S ⟶ T.obj Y) (g : Y ⟶ Y') (g' : Y' ⟶ Y'') : /-- Variant of `homMk'` where both objects are applications of `mk`. -/ @[simps] def mkPostcomp (f : S ⟶ T.obj Y) (g : Y ⟶ Y') : mk f ⟶ mk (f ≫ T.map g) where - left := eqToHom (by ext) + left := 𝟙 _ right := g lemma mkPostcomp_id (f : S ⟶ T.obj Y) : mkPostcomp f (𝟙 Y) = eqToHom (by aesop_cat) := by aesop_cat @@ -166,7 +166,7 @@ and to check that the triangle commutes. def isoMk {f f' : StructuredArrow S T} (g : f.right ≅ f'.right) (w : f.hom ≫ T.map g.hom = f'.hom := by aesop_cat) : f ≅ f' := - Comma.isoMk (eqToIso (by ext)) g (by simpa [eqToHom_map] using w.symm) + Comma.isoMk (eqToIso (by ext)) g (by simpa using w.symm) #align category_theory.structured_arrow.iso_mk CategoryTheory.StructuredArrow.isoMk /- Porting note : it appears the simp lemma is not getting generated but the linter @@ -456,8 +456,7 @@ and to check that the triangle commutes. def homMk {f f' : CostructuredArrow S T} (g : f.left ⟶ f'.left) (w : S.map g ≫ f'.hom = f.hom := by aesop_cat) : f ⟶ f' where left := g - right := eqToHom (by ext) - w := by simpa [eqToHom_map] using w + right := 𝟙 _ #align category_theory.costructured_arrow.hom_mk CategoryTheory.CostructuredArrow.homMk /- Porting note : it appears the simp lemma is not getting generated but the linter @@ -469,7 +468,7 @@ attribute [-simp, nolint simpNF] homMk_right_down_down @[simps] def homMk' (f : CostructuredArrow S T) (g : Y' ⟶ f.left) : mk (S.map g ≫ f.hom) ⟶ f where left := g - right := eqToHom (by ext) + right := 𝟙 _ lemma homMk'_id (f : CostructuredArrow S T) : homMk' f (𝟙 f.left) = eqToHom (by aesop_cat) := by ext @@ -491,7 +490,7 @@ lemma homMk'_mk_comp (f : S.obj Y ⟶ T) (g : Y' ⟶ Y) (g' : Y'' ⟶ Y') : @[simps] def mkPrecomp (f : S.obj Y ⟶ T) (g : Y' ⟶ Y) : mk (S.map g ≫ f) ⟶ mk f where left := g - right := eqToHom (by ext) + right := 𝟙 _ lemma mkPrecomp_id (f : S.obj Y ⟶ T) : mkPrecomp f (𝟙 Y) = eqToHom (by aesop_cat) := by aesop_cat lemma mkPrecomp_comp (f : S.obj Y ⟶ T) (g : Y' ⟶ Y) (g' : Y'' ⟶ Y') : @@ -505,7 +504,7 @@ and to check that the triangle commutes. @[simps!] def isoMk {f f' : CostructuredArrow S T} (g : f.left ≅ f'.left) (w : S.map g.hom ≫ f'.hom = f.hom := by aesop_cat) : f ≅ f' := - Comma.isoMk g (eqToIso (by ext)) (by simpa [eqToHom_map] using w) + Comma.isoMk g (eqToIso (by ext)) (by simpa using w) #align category_theory.costructured_arrow.iso_mk CategoryTheory.CostructuredArrow.isoMk /- Porting note : it appears the simp lemma is not getting generated but the linter