Contributing sifted colimits (how to define them?)

Stream: mathlib4

[Fernando Chu]

Hello, I'm new in Lean and I want to contribute sifted categories as well as a proof that sifted colimits commute with finite products. Before I begin writing the code, what should be the official definition of them? In the literature it is common to define sifted colimits as those that commute with finite products and then characterizing them.

Is there any convention or rule of thumb on which equivalent definition I should use? For the particular case of sifted, any of 1.1, 2.1, or 2.2. from the nlab seem like a good definition to me. The characterization in 2.2. is the most concrete and parallels the definition of filtered categories already in mathlib, but it's so concrete it may never be actually used.

[Joël Riou]

Definitions 2.1 or 2.2 are better because definition 1.1 would create universe issues (in Lean/mathlib, we have as many categories of sets as there are universes). Between 2.1 and 2.2, I would rather choose 2.1 because we already have an API for final/initial functors.

[Fernando Chu]

But there's also API for cospans and connected categories, I believe.

[Scott Morrison]

I suspect 2.1 will be more useful in Mathlib.
(Doesn't hurt to prove the equivalence, of course!)

[Kevin Buzzard]

Yeah fix a definition and then the more API the better :-)

[Fernando Chu]

Okay, I'll choose 2.1 then, thanks for the comments! I'll ask here again later if any problems appear.

[Fernando Chu]

Hello, after reading the library some more I got this so far https://github.com/leanprover-community/mathlib4/commit/4afc84c7864b8a50f18f7d9cfffb2346826858c4

I wanted some early feedback even though there's not much, and also to ask what would be the best way to show that C is nonempty from [HasFiniteCoproducts C]. I'm not sure how to get the initial element data from it.

[Kevin Buzzard]

Is there docs#HasInitialObject ?

[Kevin Buzzard]

No not quite. I was hoping it would all have been anyway done for you

[Adam Topaz]

You can write \bot_ _ (modulo unicode) to get the initial object

[Adam Topaz]

docs#CategoryTheory.Limits.HasInitial

[Fernando Chu]

I'm getting failed to synthesize instance: Bot C I suppose because [HasFiniteCoproducts C] gives me HasColimitsOfShape (Discrete (Fin n)) C, not HasColimitsOfShape (Discrete.{0} PEmpty) C hmmmm. I suppose the problem is that these discrete categories are not definitionally equal?

[Adam Topaz]

Don’t fortget the underscore

[Fernando Chu]

Oh my bad, it's working now, thanks! But now I'm wondering, how did it bypass the non-definitional-equality between the two discrete categories?

[Adam Topaz]

It’s just an instance that’s registered somewhere in mathlib, I think.