AB axioms for CondensedAb

Stream: Copenhagen Masterclass 2023

[Dagur Asgeirsson]

Kevin Buzzard said:

My feeling is that things are going faster than expected, which is great. Adam and I are really hoping that you can prove AB5 for condensed abelian groups by the end of the week. Adam will talk about things related to this today, and I'll do warm-up from 9 to 10, talking about abelian categories in Lean, finite biproducts, and filtered colimits.

Did anyone end up doing anything with the AB axioms for condensed abelian groups?

[Johan Commelin]

Which ones were done in LTE?

[Johan Commelin]

I don't remember :see_no_evil:

[Adam Topaz]

4 + 5