remaining facts about the simplex category

Stream: Infinity-Cosmos

[Jakob von Raumer]

@Robin Carlier I have a bit of capacity to work on a few things, and was wondering if there's any good self contained tasks open on $\Delta$, I think 1.2.4 of the blueprint is just lacking the uniqueness of the epi-mono-factorization?

[Robin Carlier]

Yes, uniqueness was not part of what I proved when proving that the simplex category has generators and relations.

To state this, I think this could be worth to introduce a typeclass asserting that a morphism property has unique factorization with respect to an other. This is a slightly evil notion because it bundles an equality of objects, but given that "strict" factorization systems like this are part of the definition of a Reedy category (or Cisinski’s variant that he calls "Eilenberg-Zilber categories" in his book (def 1.3.1 here)) of which the simplex category is an example, maybe it’s a "necessary evil" we’ll want at some point? Maybe @Joël Riou has an opinion on the value of such a def?

[Joël Riou]

Mathlib already knows about the (essential) uniqueness of the epi/mono factorization in the SimplexCategory (I used it already when I formalized the Dold-Kan equivalence), see docs#SimplexCategory.instHasStrongEpiMonoFactorisations, docs#CategoryTheory.Limits.functorialEpiMonoFactorizationData and the definitions nearby.

[Robin Carlier]

I can think of two things around $\Delta$ that could be nice to have, but they’re not part of the blueprint and I’ll let @Emily Riehl decide if they’re valuable or not within the framework of the Infinity-Cosmos project:

• Something that could be nice to investigate (but that would need for my series of PR to be fully merged) would be to also describe truncated simplex categories by generators and relations, this is a bit boring though, as it’s basically redoing the definition of SimplexCategoryGenRel with an extra parameter n : N, and have explicit Fin n parameters in the morphisms. I do wonder if ENNat would help us have something unified.

• We also don’t have finality (or cofinality? I always mix them up...) of the inclusion of 2-trucated simplex category (in fact, the k-truncated for k>1) in $\Delta$, so that colimits of simplicial objects "are just" colimits of their 2-truncation (which happen to be reflexive coequalizers if we prove that the 2-trucated simplex category is equivalent to the walking reflexive coequalizer, which would be almost tautological with the previous point). This fact shows that the colimit functor on simplicial sets commutes with finite products (we could probably also directly prove it is sifted), which I find is a nice fact.

[Robin Carlier]

@Joël Riou my point was that in the case of the simplex category, we have the stronger statement of strict uniqueness rather than essential uniqueness. Would you say that actually we could make things like Reedy categories work with essential uniqueness everywhere? In the litterature they require strict uniqueness as far as I know.

[Joël Riou]

Mathlib also knows that in SimplexCategory, two isomorphic objects are equal and the iso must be the identity, so that essential uniqueness implies strict uniqueness. I am not saying more than that.

[Robin Carlier]

I never said the proof was hard :D, but I was asking wether or not a typeclass encoding strict factorizations (that the simplex category would easily instanciate with this argument) would be a good idea.

[Joël Riou]

Lemmas asserting the strict uniqueness of the factorization would not be very good looking... Unless we have more applications, I am not sure we need to create a new typeclass for that.

[Robin Carlier]

Ok, so let’s wait until we actually run into more strict factorization systems then.

[Jakob von Raumer]

Okay, didn't know we had essential uniqueness, that does indeed seem like it's enough

[Jakob von Raumer]

Thanks for the suggestions, @Robin Carlier !

[Jakob von Raumer]

Robin Carlier said:

• We also don’t have finality (or cofinality? I always mix them up...) of the inclusion of 2-trucated simplex category (in fact, the k-truncated for k>1) in $\Delta$, so that colimits of simplicial objects "are just" colimits of their 2-truncation (which happen to be reflexive coequalizers if we prove that the 2-trucated simplex category is equivalent to the walking reflexive coequalizer, which would be almost tautological with the previous point). This fact shows that the colimit functor on simplicial sets commutes with finite products (we could probably also directly prove it is sifted), which I find is a nice fact.

We don't have the factorization of a morphism Δ ⟶ Δ₁ with Δ₁.len ≤ n in SimplexCategory yet, that goes via ⦋n⦌?

[Jakob von Raumer]

(I don't even find the right function on Fin that would be the second leg of that factorization)

[Robin Carlier]

If you can’t find it then we probably don’t have it... Since the simplex category is a split epi category, we could just build an epi from ⦋n⦌ to Δ for every ∆ of lenght ≤ n (just by composing degeneracies), then take a section of that epi (which is automatically a mono), and compose Δ ⟶ Δ₁ with this section?

[Jakob von Raumer]

#26475 fwiw, but that can be generalized at least to arbitrary full subcategory inclusions where the subcategory contains either a terminal or an initial object.

[Robin Carlier]

Turns out my suggestion was bogus in the way I phrased it and I feel very sorry for not stating things correctly and making you work on it before properly checking...

It is true that any inclusion of a full subcategory containing the initial terminal object is final: in terms of colimits, this is telling us that the colimit of something out of the big category is the same as the colimit of something out of the subcategory (via restriction), and since there is a initial terminal object, in both case, colimits are given by evaluation at the initial termial object. In the case of the simplex category, this translates to a statement colimits of cosimplicial objects.

What I really meant to ask was this inclusion, for n > 0 is initial (that’s what I was meaning in my original post when mulling over "final vs cofinal"), so that we can translate it to the statement about colimits of simplicial objects (no co) (or limits of simplicial objects). What I was talking about when I mentioned colimits of simplicial objects being reflexive coequalizers really requires initiality (a.k.a cofinality) of that inclusion, and this one I believe is trickier and only valid for n > 0.

[Jakob von Raumer]

Yes, I suspected that, since the result was entirely trivial (and I didn't need the map I mentioned above).

[Robin Carlier]

Apologies again... I always get tangled into the initial vs final mess.

[Jakob von Raumer]

Will still generalize the result (and maybe remove the concrete instantiation)

Nvm, it's probably not worth it, since as you say, colimitOfTerminal gives us everything to evaluate those colimits anyway

[Robin Carlier]

I guess if you want to generalize the result (for subcategories w/ a final object I mean), mathlib knows that if an object x : Cis terminal, then the (fully faithful) functor from PUnit to C sending unit to x is final (docs#CategoryTheory.Functor.final_fromPUnit_of_isTerminal) and use docs#CategoryTheory.Fnuctor.Final.final_iff_final_comp

[Robin Carlier]

But yeah, in the end for colimit-computation purposes colimitOfTerminal does everything.

[Jakob von Raumer]

Repurposed #26475 to just show that 0 is terminal.

[Emily Riehl]

Very late to weigh in here but as illustrated by @Robin Carlier's confusions, I'm strongly in favor of "initial functor" to generalize the case of including an initial object and "final functor" to generalize the case of including a final object. Note this contradicts (but improves upon) the original historical terminology.

A functor k : I -> J is initial iff any cone over a J-shaped diagram is a limit cone iff its restriction along k to a cone over an I-shaped diagram is a limit cone. Dually, a functor k : I -> J is final if it has the same property for colimits.

Note the inclusion of the 1-truncated simplex category (spanned by just the objects 0 and 1) into Δ is initial; this was eroniously called the "2-truncated simplex category" above.

[Robin Carlier]

Yes, my confusions are not just with initial/final, but also with indices :sweat_smile: I was meaning the one spanned by 0 and 1 indeed.

[Jakob von Raumer]

@Emily Riehl Yes, the definitions of initial and final functors that we have in mathlib are equivalent to this, but defined as the category of (co)structured arrows being connected.

[Emily Riehl]

Jakob von Raumer said:

Repurposed #26475 to just show that 0 is terminal.

As Joël noted there, we had done something similar in another PR, which I've added you to. (I also used your code to improve ours.) We needed this fact to show that hoFunctor : SSet -> Cat is lax monoidal, in this case preserving the terminal object and binary products. @Jakob von Raumer if you have any suggestions on anything you see in there, they would be very welcome.

[Emily Riehl]

Regarding self contained tasks on Δ, anything that makes its truncations easier to work with would be very welcome @Jakob von Raumer . If you look at the top of the HomotopyCat file under SimplicialSet in mathlib, you'll find some API that Mario and I developed specific to the 2-truncated case. Essentially we reproved a bunch of simplicial identities in that special case because we found them hard to use when we needed them. @Julian Komaromy had similar issues with 2-truncated quasi-categories (in the infinity cosmos repository).

And all this should be extended to n-truncated things.

[Jakob von Raumer]

@Joël Riou Initiality shown in #26490. (Tell me if I should remove the helper construction in Limits.Final that I ended up not using at all)

[Jakob von Raumer]

Emily Riehl said:

Regarding self contained tasks on Δ, anything that makes its truncations easier to work with would be very welcome Jakob von Raumer . If you look at the top of the HomotopyCat file under SimplicialSet in mathlib, you'll find some API that Mario and I developed specific to the 2-truncated case. Essentially we reproved a bunch of simplicial identities in that special case because we found them hard to use when we needed them. Julian Komaromy had similar issues with 2-truncated quasi-categories (in the infinity cosmos repository).

And all this should be extended to n-truncated things.

You mean having more identities hardcoded in $\Delta_{\le n}$ with suitable autoparams?

[Jakob von Raumer]

Oh and speaking of monoidal functors, would it actually be helpful to have the monoidal structure on $\Delta$ (with $[m] \otimes [n] = [m + n]$) as well?

[Robin Carlier]

I have an open PR (#25743) that puts a monoidal structure on the augmented simplex category which corresponds to ordinal sum and is given by n \ot m = n + m + 1. I intend to use this (+ my ongoing series of PR on Day convolution) to define joins of (augmented) simplicial sets and monoidal Bar constructions.

[Jakob von Raumer]

Do you know by heart if the infrastructure for $\Delta$ to inherit that monoidal structure is already there (i.e. as a full subcat containing the unit or so)

[Jakob von Raumer]

Ah yes, we have that :)

[Robin Carlier]

It doesn't contain the unit, the unit in the augmented simplex category is the initial object that is added.
I don't think there is a nice monoidal structure on $\Delta$... With the formula you gave, I'm not sure how to define the whisker lefts and whisker right other than by putting identities (which basically "ignores" the morphisms of the simplex category and only care about its discrete subcategory in its type of object)

[Jakob von Raumer]

Ah, yes, off-by-one error in my head, you're right

[Emily Riehl]

Yes this is always confusing. Kudos on defining that monoidal structure.

[Emily Riehl]

@Jakob von Raumer or @Robin Carlier if you want to construct something fun you could use the monoidal structure on the augmented simplex category to define a strict bicategory Adj which has the universal property of being the free 2-category containing an adjunction. It has:

• two objects we can call + and -
• hom(+,+) = $\Delta_+$ (the augmented simplex category)
• hom(-,-) = $\Delta_+^{op}$ (its opposite; also the subcategory of $\Delta_+$ containing maps that preserve both the top and bottom element in each ordinal)
• hom(-,+) = $\Delta_\top$ (the subcategory of $\Delta$ containing only the maps that preserve the top element in each ordinal)
• hom(+,-) = $\Delta_\bot$ (the subcategory of $\Delta$ containing only the maps that preserve the bottom element in each ordinal; also the opposite of $\Delta_\top$)

Composition is defined by ordinal sum and its restriction to the various subcategories.

[Emily Riehl]

The original reference is "The free adjunction" by Schanuel and Street but a few more details are in definition 9.1.1 here

[Robin Carlier]

Thanks for the suggestion and reference! The definition in itself should be doable, but I don’t see myself tackling the proof that it is the free adjunction just yet (as mentioned above, one of my current focus is to show that $\Delta_+$ is the free monoid, which is already painful enough formally..., looks like chapter 10 of the PDF might contains things that could interest me in that regard).

[Jakob von Raumer]

Emily Riehl said:

If you look at the top of the HomotopyCat file under SimplicialSet in mathlib, you'll find some API that Mario and I developed specific to the 2-truncated case.

Generalized those abbreviations as Truncated.δ and Truncated.σ in #26738. To keep using a subscript for the truncation level, we'd have to use different characters, maybe underlined ones like δ̲

[Emily Riehl]

It wasn't ever obvious to me that the subscripts were a good idea. @Julian Komaromy or @Nick Ward do you have opinions about this API?

[Julian Komaromy]

I personally don't need anything other than the 2-truncated stuff, and I don't know if other truncation levels are going to be important elsewhere. As to using subscripts or not, I don't really have an opinion.