Freyd-Mitchell embedding

Stream: Is there code for X?

[Shuhao Song]

I searched the Zulip and someone is working on it. What is the progress?

[Kim Morrison]

Can you link to that conversation?

[Shuhao Song]

#narrow/stream/116290-rss/topic/Recent.20Commits.20to.20mathlib4.3Amaster/near/441119443

[Shuhao Song]

"This PR is part of the effort to prove the Freyd-Mitchell embedding theorem."

[Kim Morrison]

@Paul A. Reichert, would you be able to assist @Shuhao Song with an update? Thanks!

[Johan Commelin]

cc @Markus Himmel @Jakob von Raumer, who were also working on this, I think

[Markus Himmel]

Paul is part of our team :) We're three people from Karlsruhe slowly working towards the theorem. I talked about our progress in Durham last week. The slides aren't really designed for consumption outside the talk, but the slide "How to prove the embedding theorem (3)" (page 23 of the PDF) gives an overview over the current progress. As explained on the next slide, we're working on this on evenings and weekends and have many other commitments, and at our current pace we're still years away from finishing.

That said, if you're looking for a way to work with abelian categories in your application, mathlib has some tools that are meant to make this easier in the absence of the full embedding theorem, see file#CategoryTheory/Abelian/Refinements and file#CategoryTheory/Abelian/Pseudoelements.

[Shuhao Song]

@Markus Himmel Where can I find your code on Grothendieck categories? I read your slide "How to prove the embedding theorem (3)", and you mentioned that the step of proving Grothendieck categories are complete was done. However, in mathlib4 and all branches, I only found Mathlib.CategoryTheory.Abelian.Generator, which is related to step (4). This shows that we only need to prove Grothendieck categories have enough injectives to prove they have an injective cogenerator.

[Markus Himmel]

The statement that Grothendieck categories are complete is docs#CategoryTheory.Limits.hasLimits_of_hasColimits_of_isSeparating (for the well-copoweredness assumption, combine docs#CategoryTheory.Abelian.wellPowered_opposite, docs#CategoryTheory.wellPowered_of_isDetector, and docs#CategoryTheory.IsSeparator.isDetector). We don't have the actual definition of Grothendieck categories yet, but all the pieces for writing it down are there (see for example docs#instPreservesFiniteLimitsFunctorAddCommGrpColim for how to spell the AB5 axiom).

[Shuhao Song]

Thanks! @Markus Himmel