truncated simplicial notations

Stream: Infinity-Cosmos

[Nick Ward]

mathlib4#20688 introduces the following notations:

• [m]ₙ denotes the m-dimensional simplex in the n-truncated simplex category. The proof p : m ≤ n can also be provided directly using the syntax [m, p]ₙ.
• X _[m]ₙ denotes the m-th term of an n-truncated (co)simplicial object X. The proof p : m ≤ n can also be provided directly using the syntax X _[m, p]ₙ.

[Nick Ward]

mathlib4#20719 provides a custom delaborator for the notation [m]ₙ, and the plan is to do the same for the X _[m]ₙ notation soon.

[Nick Ward]

The reason for this thread is to solicit any advice or opinions on these notations and how they should be pretty-printed.

[Nick Ward]

For instance, it's not obvious to me whether the subscript notation will be clear enough in the infoview (though this is currently what the delaborator uses, see the file MathlibTest/SimplexCategory.lean in #20719).

[Nick Ward]

Any feedback on the notations or the implementation is appreciated!

[Emily Riehl]

This thread might be a good place to confess that I don't know how to type "n+1" in a subscript (and thus have been doing a lot of copy pasting). I've been typing \_n to get a subscript n.

[Jack McKoen]

Generally you can just type \_ before the character you want

[Nick Ward]

I also find getting a subscripted "n+1" to be a bit inconvenient. I think the most direct way (in vim) is to type \_n, leave insert mode (or do whatever is needed to activate your unicode replacement), then type \_+, leave insert mode again, then type \1.

[Julian Berman]

In both VSCode and lean.nvim you can define a custom abbreviation if this kind of thing gets annoying, just in case that's helpful to mention (though every person who types things ends up needing to do so).

[Nick Ward]

This, along with the fact that not all characters can be subscripted in unicode, could be a reason to go a different way with the notation (something like [n]_m)

[Nick Ward]

Good point @Julian Berman. I guess the question also depends on whether n + 1 is as expressive as we will need to be for the truncation level.

[Nick Ward]

Related to the notation question above, I have decided we may need something like the definition below in order to avoid the proliferation of abbrevs like SSet.δ₂ here.

abbrev SimplexCategory.Truncated.mkHom {n : ℕ} {a b : SimplexCategory} (f : a ⟶ b)
    (ha : a.len ≤ n := by trunc) (hb : b.len ≤ n := by trunc) :
  (⟨a, ha⟩ : Truncated n) ⟶ ⟨b, hb⟩ := f

I believe the reason we need this is that, for all a, b ≤ n, [a] ⟶ [b] is defeq to [a]ₙ ⟶ [b]ₙ, but these types are not syntactically equal. So (I think) type ascription (as in ((δ 1) : [a]ₙ ⟶ [b]ₙ)) or coercions are not useful here. We could always write morphisms in the truncated simplex category as @id ([a]ₙ ⟶ [b]ₙ) (SimplexCategory.δ 1), but at that point we might as well use an explicit wrapper like mkHom above.

I have a couple of questions about this:

• Is there a better solution I'm missing?
• Should mkHom be an abbrev or a def?
• I would think abbrev, but SimplexCategory.Hom.toOrderHom is a similar construction that uses def. Does anyone understand the reason this was chosen?
• What namespace does this belong in? Do we want to be writing Truncated.mkHom (δ 1) or (δ 1).toTruncatedHom?
• Should we make this a notation? Something like ⟨δ 1⟩ₙ could work, but this always requires specifying the truncation level (which from some brief experiments can usually be inferred).

[Nick Ward]

To be clear, if X : SSet.Truncated n, we can always just write X.map (δ 1).op. The reason for wanting to explicitly coerce δ 1 to be of type [a]ₙ ⟶ [b]ₙ (as in X.map (mkHom (δ 1)).op) is to avoid needing erw everywhere.

[Emily Riehl]

Pinging the authors @Johan Commelin @Kim Morrison @Adam Topaz of the SimplexCategory file.

[Emily Riehl]

This seems very useful to me. I imagine this would be called most often from within the Truncated namespace, so the name Truncated.mkHom would just be mkHom, which feels intuitive (this is how you make the arrows).

[Nick Ward]

For reference, I've now implemented this change in #20668 (calling it SimplexCategory.Truncated.Hom.tr). I was able to get rid of all of the erws, but would still be very appreciative of any suggestions or preferences regarding e.g. naming or notation.

[Johan Commelin]

Getting rid of all the erw is a very good sign!

[Johan Commelin]

The new notations look good and useful to me. But I would appreciate if some (d)elaborator expert would also take a look at them.

[Nick Ward]

If a(n) (d)elaborator expert does get a chance to take a look, the delaborator is broken out into #20719.