Preserving binary coprods of preserving arbitrary coprods

Stream: new members

[Brendan Seamas Murphy]

I have a functor F : C ⥤ D and I know for any J : Type and f : J → C that limits.preserves_colimit (discrete.functor f) F. How can I get that for all X, Y : C, limits.preserves_colimit (category_theory.limits.pair X Y) F? I.e., how can I deduce that F preserves binary coproducts from the fact that it preserves arbitrary coproducts?

[Adam Topaz]

typeclass search doesn't get it?

[Adam Topaz]

it should

[Brendan Seamas Murphy]

oh hm my preserves_colimit wasn't an instance, I'll try making it one and then seeing if typeclass search gets it

[Brendan Seamas Murphy]

Seems like it still doesn't work

[Adam Topaz]

can you give me a #mwe ?

[Brendan Seamas Murphy]

(the specific thing I'm doing is that I've shown singular homology preserves coproducts using AB4 stuff and I want to compute H_k(S^0))

[Brendan Seamas Murphy]

Sure, although it'll take a minute

[Brendan Seamas Murphy]

Also my copy of mathlib is currently at revision 168d6ba8e13d66a5fa26131eeb24aceefc749dee, in case the instance you're thinking of was added recently

[Adam Topaz]

BAH it seems to be missing. How annoying!

[Brendan Seamas Murphy]

rip! I'll add it in my project now and then it'll get merged in eventually

[Adam Topaz]

Keep in mind that it's always better to open many small PRs as opposed to a few large ones! This would be an easy PR you could open right away.

[Brendan Seamas Murphy]

Related question: does mathlib have that the binary coproduct of two initial objects is an initial object?