Zulip Chat Archive

Stream: condensed mathematics

Topic: AB4

Johan Commelin (Jul 04 2022 at 06:51):

for_mathlib/endomorphisms/ab4.lean contains another categorical sorry

Johan Commelin (Jul 05 2022 at 05:21):

This is now done

Julian Külshammer (Jul 05 2022 at 05:56):

I likely misunderstood something, but isn't that an application of the lemma AB4_of_preserves_colimits_of_reflects_limits_of_AB4 applied to the forgetful functor?

Johan Commelin (Jul 05 2022 at 05:59):

I think that's roughly what we used.

Johan Commelin (Jul 05 2022 at 05:59):

Or do you mean it should be a 1-liner?

Johan Commelin (Jul 05 2022 at 05:59):

Feel free to push a fix (-;

Julian Külshammer (Jul 06 2022 at 06:22):

On vacation right now, but as far as I can tell the only things preventing it to be a one-liner are a missing creates_limits instances on forget which I checked is two one-liners and a has_coproduct instance on endomorphisms which I wouldn't think is hard to derive from has_coproduct on A.

Adam Topaz (Jul 06 2022 at 10:40):

Hah! Yeah that would be a one-line proof! I forgot I proved that AB4_of_preserves_colimits_of_reflects_limits_of_AB4 lemma :)

Adam Topaz (Jul 06 2022 at 10:41):

(the name is not quite accurate IIRC)

Adam Topaz (Jul 06 2022 at 11:43):

FWIW we know that the forgetful functor from endomorphisms creates all limits and colimits, so getting the necessary instances should be easy

Last updated: Dec 20 2023 at 11:08 UTC