single coproducts

Stream: condensed mathematics

[Johan Commelin]

I'm working on the sorries in single_coproducts.lean.

[Johan Commelin]

There is 1 sorry left in this file. I don't see immediately how to tackle it with the lemmas that we have. It is:

noncomputable
instance preserves_coproducts_Ext' {α : Type v} (i : ℤ) (Y : A) [AB4 A] :
  preserves_colimits_of_shape (discrete α)
  ((Ext' i).flip.obj Y).right_op :=

[Adam Topaz]

Isn't this supposed to use the fact that Ext(-,Y) sends coproducts to products?

[Adam Topaz]

Along with the fact that single preserves coproducts

[Johan Commelin]

well, that's what it's proving, I guess

[Adam Topaz]

But we already have the isomorphism between ext of the coproduct and the product of the exts

[Adam Topaz]

And I think we may even have that Ext(-,Y).right_op preserves coproducts??

[Adam Topaz]

Maybe we never got around to adding that...

[Johan Commelin]

Hmm, the skeleton for this sorry is much more than simply "compose two instances"

[Adam Topaz]

Oh I remember now, we couldn't really state a preserves colimit instance because of the uniformly bounded stuff

[Johan Commelin]

yeah, that makes sense

[Adam Topaz]

I pushed a proof of this sorry

[Johan Commelin]

Nice! Thanks

[Johan Commelin]

Another file sorry-free (-;