Colimits in `Grp`

Stream: Is there code for X?

[Sophie Morel]

Does mathlib have colimits in the category Grp of groups? The file https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Category/Grp/Colimits.html where such colimits should be if they exist has as its title "The category of additive commutative groups has all colimits", so I'm guessing the answer is "no".
I was thinking of writing a proof that the universe lifting functor Grp.uliftFunctorpreserves small colimits (it does not preserve all colimits), but I don't know how to do it without the explicit construction of such colimits, so I guess I won't. I'm mostly interested in CommGrp.uliftFunctor anyway, which does preserve all colimits because CommGrp has a cogenerator.

[Andrew Yang]

@Junyan Xu

[Junyan Xu]

Sophie Morel said:

... the universe lifting functor Grp.uliftFunctorpreserves small colimits (it does not preserve all colimits)

Funnily I made the same observation in #Is there code for X? > tensor products commute with direct limits @ 💬

I recall it's in mathlib that colimits exist if coproducts and coequalizers exist. It's also true that colimits are preserved if coproducts and coequalizers are, right?

[Junyan Xu]

I also recently noticed that the construction AddCommGroup.DirectLimit actually works for all colimits (if you generalize the Preorder to an arbitrary indexing category), and you might use that as well.

[Sophie Morel]

No, it is not true that colimits are preserved if coproducts and coequalizers are, because the colimit of a functor F : J ⥤ Grp.{u} could exist without the coproduct of all F.obj j existing, if J is a big category relative to the universe u.

[Sophie Morel]

I am currently writing a proof that AddCommGrp.uliftFunctor preserves all colimits that doesn't use any construction of colimits but uses the cogenerator AddCircle (1 : ℚ) of AddCommGrp.{u}, similar to the proof in https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Limits/Preserves/Ulift.html (that uses the generator Prop for Type u but doesn't really explain what it is doing). This is actually much simpler than using a specific construction of colimits.

[Sophie Morel]

As for the functor Grp.uliftFunctor : Grp.{u} ⥤ Grp.{max v u}, it does not preserve all colimits. It does preserve colimits indexed by u-small categories, but since I was unable to find a construction of such colimits in mathlib (I cannot even find a construction of small coproducts in Grp), and since I am not planning to write such a construction, I cannot prove it.

[Sophie Morel]

This all started from me needing the fact that AddCommGroup.uliftFunctoris a faithful exact functor, so I do not want to get distracted too much.

[Sophie Morel]

Junyan Xu said:

Sophie Morel said:

... the universe lifting functor Grp.uliftFunctorpreserves small colimits (it does not preserve all colimits)

Funnily I made the same observation in #Is there code for X? > tensor products commute with direct limits @ 💬

I recall it's in mathlib that colimits exist if coproducts and coequalizers exist. It's also true that colimits are preserved if coproducts and coequalizers are, right?

I had found the same flavor of counterexample to show that Grp.uliftFunctor does not preserve colimits. Funnily, you don't mention the thing that I wanted, which is that AddCommGrp.uliftFunctor does, though of course it follows easily from the existence of a cogenerator in Type. (I am not touching Module categories, I have enough trouble with universes as it is without bring more into play.)

[Junyan Xu]

Sorry for not being precise. I meant that if it preserves coproducts of a certain size (i.e. with J in a certain universe) then it preserves coproducts of that size.

Cogenerators are mentioned in #Is there code for X? > tensor products commute with direct limits @ 💬
I acutally authored the proof in Type. But I think there's a shorter proof in mathlib now ...

[Sophie Morel]

Yes, the file credits Dagur Asgeirsson and you, and I could see the similarities between the proof you linked and the one in mathlib.

[Junyan Xu]

I think in mathlib there's now an Equiv between an abstract colimit in Type and a Quot type, which could be used to remove my code completely.

[Sophie Morel]

This? (And the results around it.)
https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Limits/Types.html#CategoryTheory.Limits.Types.hasColimit_iff_small_quot

[Sophie Morel]

I would prefer not to remove your code, as it is less category-dependent, i.e. it is easier to adapt to other algebraic categories that have a small cogenerator, even if we don't have a nice explicit construction of colimits for them.

[Sophie Morel]

It's just a pity that it doesn't explain what it is doing.

[Kevin Buzzard]

PRs documenting code always welcome! I was experimenting with this to see how other people would react, e.g. here, here and lots more occurrences in that file, i.e. actually explaining what my code did. Nobody seemed to object!

[Sophie Morel]

Well Kevin, I recently proved that the adjoint of a triangulated functor is triangulated, and decided to see if I could PR it, which is going to take a lot of effort. I could do that, or I could document other people's code, but I'm not sure I can do both.

[Kevin Buzzard]

Fair point! I think that my personal preference would be you doing adjoints of triangulated functors :-)

[Sophie Morel]

(I will of course try to document my own code sufficiently.)

[Sophie Morel]

There was a "funny" moment during that project, where one line of informal math became about 1000 lines of code. Ah, category theory...
(It was the proof that, if a functor commutes with shifts, so does its left/right adjoint. Because "commuting with shifts" is not a property, it's a structure, and a structure that needs to satisfy some compatibilities, and I don't think anybody ever checks these compatibilities in informal math.)

[Junyan Xu]

I cannot even find a construction of small coproducts in Grp

There's actually docs#Monoid.CoprodI.instGroup

[Sophie Morel]

Ah, thanks! So having coproducts in the category Grp should be easy from that. Now I just hope you don't find cokernels, because I would have to find another excuse not to show that Grp.uliftFunctor commutes with small colimits. :grinning_face_with_smiling_eyes:

[Joël Riou]

Sophie Morel said:

Well Kevin, I recently proved that the adjoint of a triangulated functor is triangulated, and decided to see if I could PR it, which is going to take a lot of effort. I could do that, or I could document other people's code, but I'm not sure I can do both.

I did this already about one year ago in https://github.com/leanprover-community/mathlib4/blob/jriou_localization/Mathlib/CategoryTheory/Triangulated/Adjunction.lean and https://github.com/leanprover-community/mathlib4/blob/jriou_localization/Mathlib/CategoryTheory/Shift/Adjunction.lean (the code is still draft...)

[Sophie Morel]

Well I figured that somebody must have done it, but at this point it was easier to just prove it myself than to look for code in people's branches. It's hard enough to find theorems in mathlib.

[Kim Morrison]

Obviously it's nice to not have to duplicate work, but sometimes it is either hard to avoid, or realistically the correct way to get things moving. The existence of work in draft shouldn't obstruct others from redoing and completing something. And in the alternative, starting to do so sometimes kick starts new progress on the work in draft, which is also positive!

[Sophie Morel]

So interesting fact about colimits in AddCommGrp: the file https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Category/Grp/Colimits.html provides an HasColimit K instance for every K : J ⥤ AddCommGroup.{u} if J : Type u and we have a Category.{u,u} J instance, but not if we have a Category.{v,u} J instance with v another universe.
Of course the construction of colimits should work as soon as the set of objects of J is u-small, so I'm guessing something went wrong somewhere in the universe soup.

[Sophie Morel]

Joël Riou said:

I did this already about one year ago in https://github.com/leanprover-community/mathlib4/blob/jriou_localization/Mathlib/CategoryTheory/Triangulated/Adjunction.lean and https://github.com/leanprover-community/mathlib4/blob/jriou_localization/Mathlib/CategoryTheory/Shift/Adjunction.lean (the code is still draft...)

I'm using a different definition of compatibility of CommShift with adjunctions, though it's easy to see it's equivalent. Your definition is more elegant, but the one I use makes it obvious that CommShift.iso isomorphisms for the left adjoint determine those for the right adjoint and vice versa, which then simplifies the construction of the CommShift structure on the adjoint (or rather the verification that it satisfies the required compatibilities, this becomes almost obvious). I'll see if I can merge the two in a satisfactory way.

I haven't looked at the details of your proof that the right adjoint preserves triangulated functors (mathematically this is the hardest part, but it Lean this was the more straightforward part for me); it seems that you use a more direct approach than me, I went through the five lemma and an adjunction homEquiv upgraded to categories of abelian groups, which is super natural mathematically but caused me some technical trouble in Lean.

I also wrote some code to get the other direction (right adjoint to left adjoint) for "free" using opposite categories, becase I need both directions for my application. It's not very difficult but you need to add a bunch of "compatibility with opposites" lemmas in a variety of places.

[Joël Riou]

Yes, I did the diagram chase in a down to earth way because at the time we did not have universe-heterogeneous versions of the 5-lemma for unbundled abelian groups (and I am not sure we have it now).
At the time I wrote this code, CategoryTheory.Adjunction.Mates was not as developed as it is know. It should be possible to get cleaner definitions and proofs using that.

[Sophie Morel]

No, it was awful, I had to apply universe lift functors everywhere to use the five lemma, and then I realized that mathlib did not know that the universe lift functor for abelian groups was exact. (Though it hopefully soon will, I finished writing the commutation with colimits and it's ready to PR.)
I also had a nasty fight with ShiftSequences, because somehow I ended up with several instances of them on the same functor, that were equal but Lean did not realize that. And every time I try to use ComposableArrows, it's awkward because simp often does not simplify statements about them so I have to know exactly what I want to prove and use change. But I'm pretty happy about how it turned out, except for the ShiftSequence stuff; there were some timeouts.

[Joël Riou]

Making attribute [local simp] Precomp.map and/or set_option simprocs false may help for the ComposableArrows issue (which appeared after a change in Lean core).

[Kim Morrison]

Which simproc causes the problem here?

[Sophie Morel]

I made the CommShift for adjunctions (+ equivalences) stuff into a PR (#20033), so you can have a look at it. It might be too long for a PR, I'm not sure.
The main difference with Joël's code (except for some cleanup of stuff that has made its way into mathlib since) is the fact that I introduce the compatibility condition separately for each element of the group and prove that it implies that the commutation isomorphism on one adjoint determine that on the other, which simplifies the proof of the compatibilities later.

[Sophie Morel]

(My TODO says "do the other direction using opposite categories", but the code became simple enough that it might okay to just do it directly.)

[Joël Riou]

In this context, working with the opposite category is a little bit painful, but here, using OppositeShift (which does not change the sign of the shift) may be an option, even though it may be easier to do the dual case directly (in another PR).
For Adjunction.left/rightAdjoint_isTriangulated, it will probably be more painful (as the signs are changed), but at some point, we should develop an API for triangulated functors and duality (F is triangulated iff F.op/F.leftOp/F.rightOp is, etc). (I still have not PRed the painful proof that the opposite category of a triangulated category is triangulated, i.e. the octahedron axioms dualises.)

[Joël Riou]

Kim Morrison said:

Which simproc causes the problem here?

I do not remember exactly, but it had to do with natural numbers.

[Sophie Morel]

I wrote some code to prove that F.op is triangulated if F is (and vice versa), but I did not touch leftOp and rightOp:
https://github.com/leanprover-community/mathlib4/compare/master...SM.AdjointTriangulated#diff-546cff707f4054447b28780149cda9090fb308564e57893467ee88a44c4dd3b2

(Please ignore the omits, I didn't put my lemmas in the correct order.)

[Sophie Morel]

(The part with the signs is fun, you have to take the opposite CommShift then pull it back by the n ↦ -n morphism.

[Sophie Morel]

As for Adjunction.CommShift in the other direction, I do have a proof written down with OppositeShift, but I'm not sure that it will be shorter than a direct proof (even after cleanup).

[Sophie Morel]

I have another question about the file Mathlib.Algebra.Category.Grp.Colimits. The beginning says "TODO: In fact, in AddCommGrp there is a much nicer model of colimits as quotients of finitely supported functions, and we really should implement this as well (or instead)." I do agree with that sentiment, I just wonder if the fact that DFinsupp J requires DecidableEq J would cause problems. (It seems to me that, if we are doing colimits in the category of groups, we are past worrying about decidability issues, but I might be missing something.)

[Joël Riou]

Sophie Morel said:

I do agree with that sentiment, I just wonder if the fact that DFinsupp J requires DecidableEq J would cause problems.

I think there would be no issue if you put DecidableEq J as an assumption in the definitions, but not in the statement of certain lemmas (e.g. proving HasColimitsOfShape).

[Sophie Morel]

Ah yes, I forgot that I can just start the proof of a lemma with classical...