Contribution of lemmas about colimits

[t-wissmann]

Hi,

thank you all for agda-categories :-) I spent almost entire last year on an initial F-algebra construction, which builds the initial algebra from finite, recursive F-coalgebras ("Initial Algebras Unchained", accepted at LICS'24, preprint, formalization, agda html). For the construction, I had written a couple of lemmas (mostly about colimits) which I find helpful for a general audience. Before flooding you with PRs, I'd like to double check with you, which ones you find useful:

• singleton-hom 𝒞 X Y (doc): the property that the hom set 𝒞(X,Y) is singleton, with notation
  _[_=∃!=>_] (𝒞 [ X =∃!=> Y ])

• For a diagram F : Functor J C and another functor G : Functor C D, one obtains a Functor (Cocones F) (Cocones (G ∘F F)) (doc; now in PR Add functors between (co)cone categories #448). This functor just does F₀ = F-map-Coconeˡ G and F₁ = F-map-Cocone⇒ˡ G (from Categories.Diagram.Cocone.Properties), but it's very useful to have a functor for the next lemma (with different identifiers, sorry!):

• If a functor F sends a colimit C₁ : Colim J to a colimitting cocone FC₁ : Colim (F ∘F J), then every colimitting J-cocone is sent to a colimitting cocone (doc). On paper the proof is: colimits are unique up to isomorphism and functors preserve isomorphism :-)

• The colimit injections form a jointly-epic family (doc)

• For a diagram in a full subcategory of a category 𝒞: If the colimit in 𝒞 exists and if the coapex is isormorphic to some object in the subcategory, then this yields the colimit in the subcategory (doc)

• The forgetful functor from F-Coalgebras to the base category creates all colimits (doc)

• If E : Functor ℰ 𝒟 is a final subdiagram of D : Functor 𝒟 𝒞, then Colimit D = Colimit (D ∘F E) (doc), corresponding nLab-page: https://ncatlab.org/nlab/show/final+functor

• A slightly more general proof of Lambek's lemma (doc) for coalgebras (also works for algebras) that does not require finality/initiality: an F-coalgebra structure c : C ⇒ F C is an isomorphism provided that there is only one (coalgebra-)endomorphism on (C,c) and at least one coalgebra morphism (FC,Fc) ⇒ (C,c)

• Properties about recursive F-Coalgebras (doc): almost all are from a paper by Capretta/Uustalu/Vene (doi); and the result that recursive F-coalgebras are closed under colimits.

Rather special results (maybe only of limited interest):

• Definition of (finitely-)presentable object and the property that presentable objects are closed under (binary) coproducts (https://arxiv.org/src/2405.09504v2/anc/Presentable.html#1245). My proof involves the concrete characterization of colimits in Setoids and that each element of a colimit comes from some element of some object in the diagram (doc)

• A necessary and sufficient conditions when hom-functors preserve (filtered) colimits (doc)

Most of the above mentioned general results should easily adapt to the the non-Co-world (Limits and Algebras). But before rewriting them, I'd be interested in your comments, which ones I should clean up and prepare as PRs.

Looking forward to your comments :-)

[JacquesCarette]

Definitely very interested. The next couple of days are very busy for me, but I'll give more detailed comments as soon as I can. (Others are most welcome to comment too!)

[JacquesCarette]

Turns out that "very busy" extended for months! I now have a nice 2 week window before the next term starts...

I think the results in your first list seem quite useful. It would be nice to be careful to have explicit duals to these theorems, when they exist / are true / etc. Having each of them as a separate PR would be wonderful.

The special results do seem more special. However, a lot of the set up (like finitary, presentable, etc) are things that are really needed in agda-categories!

Again, apologies for taking so long.

[t-wissmann]

I'm sorry for being inactive for quite a while as well :-(; I've just sent the first PR (#448), and I plan to send the others once in a while but as soon as possible :-)

[JacquesCarette]

Thanks. And no worries - all progress is good progress.