Duplicated lemma

Stream: mathlib4

[Edison Xie]

I found CategoryTheory.Limits.cokernelIsoOfEq and CategoryTheory.Limits.cokernel.congr, are they the same thing in different names?

[Edison Xie]

I mean they are literally the same isomorphism:

example {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {X Y : C}
    (f g : X ⟶ Y) [Limits.HasCokernel f] [Limits.HasCokernel g] (h : f = g) :
    CategoryTheory.Limits.cokernelIsoOfEq h = CategoryTheory.Limits.cokernel.congr f g h := by
  ext; simp

[Robin Carlier]

Yes, this is a duplicate and there is most likely the same with kernels. Which one is most used in the library currently?

[Aaron Liu]

does one of them have better defeqs?

[Aaron Liu]

docs#CategoryTheory.Limits.cokernelIsoOfEq, docs#CategoryTheory.Limits.cokernel.congr

[Edison Xie]

Aaron Liu said:

does one of them have better defeqs?

I think congr has better defeq

[Edison Xie]

also that could be generalized to:

open Limits in
@[simps]
def CategoryTheory.isoCokernelOfIso {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C]
    {X Y Z W : C} (f : X ⟶ Y) (g : Z ⟶ W) (e1 : X ≅ Z) (e2 : Y ≅ W) (h : e1.hom ≫ g = f ≫ e2.hom)
    [HasCokernel f] [HasCokernel g] : cokernel f ≅ cokernel g where
  hom := cokernel.desc _ (e2.hom ≫ cokernel.π g) (by rw [← Category.assoc, ← h]; simp)
  inv := cokernel.desc _ (e2.inv ≫ cokernel.π f) (by
    apply_fun (e1.inv ≫ · ≫ e2.inv) at h
    simp only [Category.assoc, Iso.inv_hom_id_assoc, Iso.hom_inv_id, Category.comp_id] at h
    rw [← Category.assoc, h]
    simp)

[Edison Xie]

Do we want both congr and the thing I wrote or only the thing I wrote since congr then would be isoCokernelOfIso f g (Iso.refl _) (Iso.refl _) (by simp)?

[Edison Xie]

Robin Carlier said:

Yes, this is a duplicate and there is most likely the same with kernels. Which one is most used in the library currently?

congr is never used :rolling_on_the_floor_laughing:

[Edison Xie]

CategoryTheory.Limits.cokernelIsoOfEq is used 14 times apparently

[Joël Riou]

We also have docs#CategoryTheory.Limits.kernel.mapIso

[Edison Xie]

So is docs#CategoryTheory.Limits.cokernel.mapIso also a thing?

[Edison Xie]

Oh it is! Thanks :folded_hands:!