transporting categorical limits across equivalences

Stream: Is there code for X?

[Eric Wieser]

In #7125, I found myself writing (or struggling to write) a huge pile of boilerplate to transfer the following across docs#CategoryTheory.Equivalence s:

• Limits.IsZero
• Limits.HasZeroObject
• Limits.HasZeroMorphisms
• Limits.Cone
• Limits.BinaryBicone
• Limits.BinaryBicone.IsBilimit
• Limits.BinaryBiproductData
• Limits.HasBinaryBiproduct

Am I missing existing results for these elsewhere?

[Eric Wieser]

(i.e., perhaps we have them for IsEquivalence instead?)

[Joël Riou]

It seems that some of your constructions (taking a colimit cocone for F ⋙ e.functor and trying to get a colimit cocone for F) could be obtained by first for applying e.inverse (use isColimitOfPreserves), so that you get a colimit cocone for (F ⋙ e.functor) ⋙ e.inverse and then using the iso between F and (F ⋙ e.functor) ⋙ e.inverse and a definition like IsColimit.precomposeHomEquiv.

[Joël Riou]

(You may also have a look at the file CategoryTheory.Adjunction.Limits which shows how to transport HasColimitsOfShape (rather than IsColimit) in both directions of an equivalence.)

[Eric Wieser]

Thanks! While looking around a bit here I created #10532, though it probably won't actually help me

[Eric Wieser]

I had another look at this, and split off the rather messy #11100