simplex category notations

Stream: mathlib4

[Nick Ward]

Currently, we have the following notations for working with the SimplexCategory and SimplicialObject:

• [n] denotes the n-dimensional simplex (SimplexCategory.mk n).
• X _[n] denotes the n-th term of a (co)simplicial object X (X.obj (Opposite.op (SimplexCategory.mk n))).

In the process of adding analogous notations for the truncated simplex category, it was noted that conflicts with the List notation should probably be avoided.

[Nick Ward]

/poll What should be the new notation for objects of the SimplexCategory?
⁅n⁆
⦗n⦘
⦋n⦌
just use SimplexCategory.mk n

[Nick Ward]

Please feel free to vote for more than one option and to add any options you feel were missed.

[Adam Topaz]

I think .mk n would work in most cases. I don’t think it’s that bad

[Nick Ward]

My main argument for keeping some notation for SimplexCategory.mk is that we frequently need to use SimplexCategory.mk as part of a type (perhaps more commonly than for the typical constructor?) where I don't think .mk would be useful.

[Nick Ward]

Then there is also the extension to the truncated simplex category, where the notation [m]ₙ allows for automating the truncation proof. Without this notation, we would constantly be writing the following.

(φ : (⟨SimplexCategory.mk m, by tactic⟩ : SimplexCategory.Truncated n) ⟶ ⟨SimplexCategory.mk j, by tactic⟩)

[Nick Ward]

Adam Topaz said:

I think .mk n would work in most cases. I don’t think it’s that bad

To be fair to this argument, I should note that you could usually write the below rather than the above.

(φ : (⟨.mk m, by tactic⟩ : SimplexCategory.Truncated n) ⟶ ⟨.mk j, by tactic⟩)

My personal preference is still for (φ : [m]ₙ ⟶ [j]ₙ), though.

[Emily Riehl]

For readability and concision, I definitely would like to see some sort of abbreviation for this. Right now, because of the List conflict, we have to write

φ  :  ([n] : SimplexCategory) ⟶ [m]

over and over again which is a bit of a pain. Also, if we don't introduce some abbreviation, how to do we refer to the type X _[n] which elaborated is something like X.obj ( ([n] : SimplexCategory).op)?

[Emily Riehl]

While we're discussing this, I think the analogous thing for cosimplicial sets is also denoted X _[n]. Is there a rational for this instead of the more conventional (on paper) notation X ^[n]?

[Joël Riou]

I would agree that if there are no technical obstacles, the n-part of a cosimplicial object should be denoted X ^[n] instead of X _[n]. (We do not have that many cosimplicial objects in mathlib yet, which may explain why nobody noticed this!)

[Nick Ward]

Some brief experimentation suggests that notation3 can handle X ^[n], so this should be an easy change.

[Nick Ward]

Do we want to change the brackets in the notations X _[n] and X ^[n] in accordance with the change to the simplex category notation? e.g. changing them to X _⦋n⦌ and X ^⦋n⦌, respectively.

[Emily Riehl]

This is a good question. How hard are the new fancy brackets to typeset? (If not so hard, then yes maybe better to align; if annoying to type, then maybe we preserve the [ ] in as many settings as avoid the list conflict.

[Nick Ward]

I believe that all of the options except ⁅n⁆ still need to be added to the abbreviations list, so we would just need to decide on a good shortcut that is unclaimed.

[Nick Ward]

Just a thought, but if we used different brackets for X _[n] than for the simplex category notations, we might be able to get away with just X [n] (no underscore).

[Emily Riehl]

While the underscore and superscript are extra typing they feel intuitive (to me at least). On paper, I'd write $X_n$ for a simplicial object and $X^n$ for a cosimplicial one.

[Kevin Buzzard]

I bet [n] gets parsed as "list with 1 element n" (this is core notation and I don't think it can be turned off) and then you get some error of the form "X isn't a function which eats lists"

[Adam Topaz]

Another possibility is to add a CoeFun instance for simplicial objects.

[Nick Ward]

#21485 changes the notation for the n-th term of a cosimplicial object to X ^[n].

[Nick Ward]

The notation X [n] for (co)simplicial objects surprisingly does work, and a CoeFun instance would be a good idea as well. I think X _[n] and X ^[n] are intuitive enough, though, and also avoid any confusion with List notation.

[Nick Ward]

Is there an established precedent for how long to keep the polls open here? Or anything I can do to market the poll more widely? I want to make sure everyone has a chance to weigh in, but also don't want to lose track of this.

[Johan Commelin]

I think it's fine. Feel free to make the PR.

[Nick Ward]

Thanks Johan Commelin!

[Nick Ward]

I will tentatively start working towards changing the notation for the n-dimensional simplex to ⦋n⦌, though anyone with strong opinions should feel free to overrule me here.

[Nick Ward]

A few notes:

• Most people (myself included) seem to be indifferent between ⦋n⦌ and ⦗n⦘. If anyone feels strongly that ⦗n⦘ does a better job of avoiding conflict with List notation, that may be worth considering.
• We still need abbreviation(s) for the new notation. Jon Eugster has suggested several options: \<[, \]>, \<[]>, \simplex as abbrevs for ⦗, ⦘, ⦗⦘, ⦗⦘, respectively. Any other suggestions or thoughts are welcome.