Normal Forms in the Simplex Category

Stream: mathlib4

[Reed Mullanix]

Was thinking of formalizing some stuff from Cisinski's "Higher Categories and Homotopical Algebra", but noticed that the current definition of the simplex category makes it really difficult to actually write out a simplicial set! Would it be too large of a breaking change to refactor the simplex category to use normal forms of face/degeneracy maps instead of monotone maps? If it is possible, I'd be willing to take on the work.

[Adam Topaz]

The “mathlib” approach would be to prove that the current simplex category has those “generators and relations”, and provide corresponding constructors for functors out of that category as well as for natural transformations between such functors.

[Adam Topaz]

There was some discussion along these lines on zulip not too long ago. I don’t remember exactly where.

[Reed Mullanix]

I see; out of curiosity is that a backwards compatibility thing, or a larger philosophy?

I am a bit skeptical that this would work well though, it seems like you'd have really poor definitional behaviour. I'll give it a shot though.

[Adam Topaz]

I dont immediately see why this approach would have bad definitional behaviour

[Adam Topaz]

It’s not about backwards compatibility per se. Rather the way we usually do things in mathlib is to have one “official” definition and develop API that allows users to work with it effectively. And when there is an alternative definition, we usually just develop more API to let you work with the “official” definition as if it was that alternative one. This isn’t a hard rule, of course, and there are other designs that appear in mathlib as well.

[Reed Mullanix]

It has to do with the definitional behaviour of functors; the equivalence between generators/relations and monotone maps involves an O(n) operation, where n is the dimension of the domain. Moreover, any functors defined this way would have to round-trip through the generators/relations -> monotone maps -> generators/relations transformation; if there is a neutral at any point in that process, the whole procedure will get stuck and result in gnarly proof terms.

[Adam Topaz]

In this case you could define some category in terms of face and degeneracy maps (e.g. using quotients of some inductive types), and provide an equivalence with the existing simplex category. Or, you could prove that the existing simplex category has those generators and relations and develop the API for functors out of categories that have some generators and relations. I think the latter approach would end up being much more useful in practice, and could easily specialize to the first approach if needed.

[Adam Topaz]

Oh, if you want to actually compute with these functors, then that’s a whole different question.

[Adam Topaz]

You can just prove an extensionality principle that says two functors agree if they agree on the generators

[Reed Mullanix]

FWIW: you actually don't need to quotient, as you can always keep everything in normal form (series of face maps with increasing indexes followed by a series of degeneracies with decreasing indexes)

[Reed Mullanix]

I'll take a look at the API approach though; the case I had in mind that needs good definitional behaviour is the bar construction, but maybe enough simp and ext lemmas will do the trick.

[Joël Riou]

Whatever the definition of the simplex category is, you should be able to get good definitional properties for the action of your simplicial objects on objects (this is just a map from the natural numbers to the category), then I am not sure there is a strong need for good definitional properties for the action of morphisms: you may very well prove suitable equational lemmas for the action of face and degeneracies. (Also, there are other simplicial objects the construction of which would not at all be eased if the simplex category was defined by generators and relations, e.g. docs#CategoryTheory.Arrow.cechNerve and https://leanprover-community.github.io/mathlib4_docs/Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.html#AlgebraicTopology.DoldKan.%CE%93%E2%82%80)

[Reed Mullanix]

For things like the bar construction, you really do want nice definitional behavior on morphisms. However, this is a bit moot as lean cannot handle the dependent pattern matching required without transports.

[Joël Riou]

In category theory constructions, it is quite difficult to prevent random left/right compositions with identities from appearing... (It was a certain effort to prevent this in the formalization of docs#CategoryTheory.ComposableArrows, e.g. https://github.com/leanprover-community/mathlib4/blob/1e9f6406fbec558bb273b1315776cb7bc4f18d3e/Mathlib/CategoryTheory/ComposableArrows.lean#L426 )