isomorphism congruence on homs

Stream: Is there code for X?

[Mario Carneiro]

Is there a result like this somewhere in the library?

def CategoryTheory.Iso.equivHomLeft {C : Type u} [Category C]
    {X Y Z : C} (α : X ≅ Y) : (X ⟶ Z) ≃ (Y ⟶ Z) where
  toFun f := α.2 ≫ f
  invFun f := α.1 ≫ f
  left_inv _ := by simp
  right_inv _ := by simp

[Adam Topaz]

I don’t think we do. Why is this useful?

[Mario Carneiro]

it's useful for composing equiv chains involving isomorphisms

[Mario Carneiro]

you could also have one with an iso on the right, or on both sides

[Bhavik Mehta]

You could maybe deduce this from Yoneda (and the result that an iso in type is an equiv)

[Adam Topaz]

Right. Use docs#CategoryTheory.Functor.mapIso with (co)yoneda

[Adam Topaz]

But I’m still not convinced this is too useful

[Mario Carneiro]

it's not too dissimilar from all the congr lemmas in Equiv.Basic

[Bhavik Mehta]

def CategoryTheory.Iso.isoHomLeft {C : Type u}
    {X Y Z : C} (α : X ≅ Y) : (X ⟶ Z) ≅ (Y ⟶ Z) :=
  (yoneda.obj Z).mapIso α.op.symm

[Bhavik Mehta]

def CategoryTheory.Iso.isoHomRight {C : Type u} [Category.{v} C]
    {X Y Z : C} (α : X ≅ Y) : (Z ⟶ X) ≅ (Z ⟶ Y) :=
  (coyoneda.obj (op Z)).mapIso α

and the dual

[Bhavik Mehta]

(and .toEquiv to make them equivs like your original question)

[Mario Carneiro]

unfortunately it's not defeq because you swapped out the equivs for isos

[Bhavik Mehta]

Did I successfully pre-empt you by 8 seconds? :D

[Mario Carneiro]

it works, but it still looks like something that should have a minimal API

[Kim Morrison]

It certainly can't hurt to have this.

[Joël Riou]

Mario Carneiro said:

Is there a result like this somewhere in the library?

def CategoryTheory.Iso.equivHomLeft {C : Type u} [Category C]
    {X Y Z : C} (α : X ≅ Y) : (X ⟶ Z) ≃ (Y ⟶ Z) where
  toFun f := α.2 ≫ f
  invFun f := α.1 ≫ f
  left_inv _ := by simp
  right_inv _ := by simp

I am introducing this in #13926.

[Markus Himmel]

Isn't this just a special case of docs#CategoryTheory.Iso.homCongr ?

[Mario Carneiro]

It is! But I scroll down and notice that isoCongr has left and right versions, so I think it would make sense to have it for homs too

[Mario Carneiro]

(you also get slightly better defeqs since it doesn't put identity compositions on the rhs)