(new) simplicial notations

Stream: Infinity-Cosmos

[Nick Ward]

Some concern has been expressed on #20688 about the conflict between the current notation [n] for SimplexCategory.mk n and the List notation (this is why you always have to write ([n] : SimplexCategory)).

As a result, we are on the hunt for a new series of notations for working with simplicial sets. Currently, we have [n] and [m]ₙ for objects of SimplexCategory and SimplexCategory.Truncated, respectively. Presumably the truncated notation will follow any changes to the SimplexCategory notation, but we can of course take the opportunity to change the subscript notation also. Any ideas or opinions are welcome.

[Nick Ward]

So far, @Jon Eugster has suggested some alternative unicode characters that resemble brackets (⁅m⁆ or ⦗m⦘ₙ) and also raised a good point that we can add any new notation we decide on to the abbreviations list, so we don't necessarily need to decide on characters that are already easy to type in lean.

[Emily Riehl]

I can live with funny looking notations but would prefer something that's not too hard to type (directly or via a useful abbreviation). ⦗m⦘ seems prettiest to me and less cluttered. I'd be happy to go ahead with that once we figure out how to type it.

[Nick Ward]

I also realized I have missed one of @Jon Eugster's suggestions: ⦋m⦌ₙ

[Nick Ward]

For comparison, we have so far: ⁅m⁆ₙ, ⦗m⦘ₙ, and ⦋m⦌ₙ.

[Nick Ward]

There also may be a non-unicode solution here, but everything I have tried so far has only managed to upset the parser.

[Jon Eugster]

These were just some suggestions which look close to [n]. What non-unicode solutions did you consider so far? Does the literature ever use anything else than square brackets?

[Jon Eugster]

If ⦗m⦘ₙ was the choice, I think abbreviations could look like this:
\<[, \]>, \<[]>, \simplex could be abbrevs for ⦗, ⦘, ⦗⦘, ⦗⦘ respectively

Ofc, it might take a moment to have them in the VS-Code extension but maybe not too long.

[Jon Eugster]

(also, after having a sound suggestion here, I'd suggest to present that suggestion on the mathlib4 channel for higher visibility)

[Johan Commelin]

I think ⦋m⦌ looks the most like [m]

[Jon Eugster]

There also ⦍m⦐, ⦏m⦎ for two similarly exotic symbols

[Nick Ward]

Perhaps my vision is not as sharp as others, but I can barely distinguish any of these (which could be good or bad, I'm not sure).

[Nick Ward]

Jon Eugster said:

What non-unicode solutions did you consider so far?

Probably all bad ideas, but the list included '[n], _[n], {{n}} [[n]], [{n}], many of which conflict even more than [n] with existing syntax anyway.

[Nick Ward]

Jon Eugster said:

(also, after having a sound suggestion here, I'd suggest to present that suggestion on the mathlib4 channel for higher visibility)

Good suggestion. Perhaps if we brainstorm a couple of options here we can create a zulip poll with more visibility.

[Nick Ward]

It seems like we have some good options already, but another route is a very short constructor name rather than a new syntax.

[Jon Eugster]

Nick Ward said:

I can barely distinguish any of these

me either :sweat_smile:.

There's ofc ⟦m⟧ too, which is already used for various syntax in Mathlib.

Something like '[m] would be close to the existing Δ[n] and probably address Kim's concern somewhat, at least doesn't look like a core notation anymore.

[Nick Ward]

Do we think that choosing different symbols which look as close as possible to square brackets actually addresses the concern of readability?

[Nick Ward]

In my mind, open Simplicial suggests that you are working far enough away from List that there isn't likely to be much confusion between the two, but curious to hear what others think.

[Joël Riou]

Jon Eugster said:

There's ofc ⟦m⟧ too, which is already used for various syntax in Mathlib.

We should not use this one because one day, we may want to study the stable homotopy category, and there the shift (for the triangulated structure) is denoted ⟦m⟧, and the definition of certain objects may also involve standard simplices.

[Jon Eugster]

no I'm not at all sure a unicode bracket makes things better :man_shrugging:

[Kevin Buzzard]

"a divides b" in lean is a \| b which is virtually indistinguishable from the set notation slash {a | b} and quotients G \/ H are hard to tell apart from division, and category arrows are hard to tell apart from function arrows, so we have some history here in choosing hard-to-tell-apart Unicode characters for fundamental things

[Nick Ward]

/poll What should be the new notation for SimplexCategory.mk?
⁅m⁆
⦗m⦘
⦋m⦌
⦍m⦐
⦏m⦎

[Nick Ward]

Well that certainly did not format as expected. It does not appear that I am able to edit or delete either, so please just ignore the extra backticks.

[Nick Ward]

Note that these are all unicode brackets (i.e. none of the options are the current square bracket notation).

[Nick Ward]

Also, anyone should feel free to add additional options to the poll or complain here if I have ignored your favorite suggestion.

[Damiano Testa]

Formatting polls is always hit or miss. Often miss.

[Nick Ward]

It appears I have missed.

[Damiano Testa]

The impossibility of editing is also a serious issue.

[Johan Commelin]

⁅m⁆ is also what's being used for the Lie bracket in mathlib. Any risk that this will clash?

[Emily Riehl]

Happy to support any of the options that aren't SimplexCategory.mk because the lack of abbreviation will add extra lines to nearly every theorem statement.

[Nick Ward]

I think I don't quite understand the logistics of using SimplexCategory.mk alone. The fully qualified name is too long in my opinion, and open SimplexCategory is bound to cause conflicts with other mks at times. Could we come up with a more unique constructor name that is also short?

[Joël Riou]

Sometimes, .mk n may work. (When Lean knows that target type is SimplexCategory)

[Nick Ward]

If no one is opposed (and if we haven't reached a point of decision fatigue already), I will make a poll in the mathlib4 channel for more visibility with the following options:
⁅m⁆, ⦗m⦘, ⦋m⦌, SimplexCategory.mk

[Nick Ward]

I will also try to clarify that there are really two (or perhaps four) notations being discussed here, i.e. [n] and [m]ₙ (plus X _[m] and X _[m]ₙ).

[Nick Ward]

#mathlib4 > simplex category notations

[Emily Riehl]

Sounds good. Could you point us to it here once it's up so we can vote again over there?

[Nick Ward]

@Emily Riehl it is live at the link below!
#mathlib4 > simplex category notations

[Nick Ward]

In case it's interesting for this discussion, commit 8abdf7b removes the usage of the notations [m]ₙ and X _[m]ₙ from #20668.

[Nick Ward]

.mk was indeed quite useful, but my main complaint is that the truncation level is nowhere to be found. I also ran into several places where the truncation level was inferred incorrectly, which was somewhat confusing and required a not-so-concise type annotation.

[Nick Ward]

(reposted from #mathlib4 > simplex category notations)

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.

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.

[Nick Ward]

@Jon Eugster do you know if a PR to the vscode abbreviations list is the only thing that needs to be done in order to get a new abbreviation working for vscode users?

[Jon Eugster]

I think so but I'm not 100% confident on top of my head.
If you want, I could create a PR for the abbreviations early next week.

[Jon Eugster]

\[=?

[Nick Ward]

Jon Eugster said:

If you want, I could create a PR for the abbreviations early next week.

I'm also happy to do so once we've decided on what to use. I think we should probably hold off on merging any notation changes until vscode users can type the new notation easily.

[Nick Ward]

I've also discovered the [$CURSOR] trick, which I think means that we could have an abbrev (e.g. \simplex) which inserts both brackets and places the cursor in between them.

[Nick Ward]

(though maybe this is reserved for a select few abbreviations, I'm not sure).

[Nick Ward]

\[]' appears to be unclaimed.

[Nick Ward]

#21565 (WIP) changes the notation for SimplexCategory.mk n to ⦋n⦌.

[Nick Ward]

Having done this, I am mildly concerned about how similar it looks to the List notation. Curious to hear what others think, though.

[Nick Ward]

#21565 has been merged, so we now have the notation ⦋n⦌ for SimplexCategory.mk n. We do not yet have a vscode abbreviation for this notation, but you can find some info about custom abbreviations here (see lean.input.customTranslations). (I would provide more details, but I am not very familiar with vscode).

[Jon Eugster]

Might be a bit pretentious, but I got the impression that even \[ is unclaimed. Other ideas: \s[, \[_

Maybe think about what's ergonomic (on an american keyboard)?

[Nick Ward]

I like \s[ (and \[ if we can justify it). It also seems that there is a precedent for having both one-sided (⦋, ⦌) and two-sided (⦋ ⦌) abbreviations. Maybe it makes sense to PR one of these options quickly so that everyone has some way to type the new notation. Then we can bikeshed the alternative abbreviation without a rush.

[Nick Ward]

#21581 updates the notations for (co)simplicial objects (X _⦋n⦌ and X ^⦋n⦌) to use the new brackets.

[Nick Ward]

Do we also want to change the notations Δ⦋n⦌, ∂Δ⦋n⦌, and Λ⦋n, i⦌?

[Emily Riehl]

Let's not change the notations for the standard simplicial sets now. We can do it later if it feels necesary.

[Emily Riehl]

Let's take \[ until someone objects? :smiling_devil:

[Emily Riehl]

Thanks @Nick Ward and @Jon Eugster for shepherding this through. Does the old [n] notation fail now?

[Emily Riehl]

And I guess maybe it makes sense to wait for the abbreviation before bumping this in our repository?

[Nick Ward]

Emily Riehl said:

Let's not change the notations for the standard simplicial sets now. We can do it later if it feels necesary.

#21586 (closed) can be re-run if we do decide to change these.

[Nick Ward]

Emily Riehl said:

Let's take \[ until someone objects? :smiling_devil:

Sounds good to me! Do you have a preference for a two-sided abbreviation (which would generate both brackets). I think we have suggestions \s[] and \simplex so far, but most of the options you might think of are available.

[Nick Ward]

Emily Riehl said:

Does the old [n] notation fail now?

It should only denote a List with one element now.

I think it's probably easiest to hold off on bumping the infinity-cosmos repo, depending how willing people are to copy-paste or set up a custom abbreviation in vscode.

[Nick Ward]

I have just realized I've been linking to the abbreviations list from the lean3 vscode extension. The correct list appears to be here.

[Nick Ward]

My reading of this doc from the vscode extension suggests that we might not actually want (or be able to use) the abbreviation \[.

[Jon Eugster]

Nick Ward said:

... but you can find some info about custom abbreviations here (see lean.input.customTranslations)...

You open your user settings: Cmd + Shift + P then search & select "Preferences: Open User Settings (JSON)".

In this JSON file, add the following entry:

    "lean4.input.customTranslations": {
        "s[]": "⦋$CURSOR⦌",
        "simplex": "⦋$CURSOR⦌"
    }

my full settings.json

{
    "editor.tabSize": 2,
    "editor.minimap.enabled": false,
    "explorer.sortOrder": "mixed",
    "git.openRepositoryInParentFolders": "always",
    "errorLens.fontStyleItalic": true,
    "lean4.input.customTranslations": {
        "s[]": "⦋$CURSOR⦌",
        "simplex": "⦋$CURSOR⦌"
    }
}

now restart VsCode (maybe enough to open a new window?) and use the abbreviation \s[] :)

[Jon Eugster]

By the looks of it, \s[ for a one-sided ⦋ doesn't quite work for the caveat described above: \s[ is automatically extended to \s[] so you'll immediately get ⦋⦌. (\s[] works fine).

[Nick Ward]

My understanding is the same, although there still seem to be analogous one-sided abbreviations in the list (e.g., c[ and c] or [[ and ]]).

[Jon Eugster]

is \[[ in the list? I've only seen \[[]]. And \c[ simply doesn't work for me and gives χ[] instead of the intended ⦃

[Nick Ward]

\[[ seems to be with the one-sided versions of all the two-sided brackets here. Interesting that \c[ doesn't work.

[Nick Ward]

@Jon Eugster what do you think of going for \s[] (or \simplex or \simp) now, then we can think on the one-sided abbreviation more?

[Nick Ward]

I'm not finding many one-sided bracket abbreviations in the list, which may be because it is difficult to come up with a good one.

[Jon Eugster]

I think adding only the abbreviations for the pair is good enough, that's the same as the current behaviour for most other special brackets :+1:

[Nick Ward]

Good point, we can probably be fine with just a two-sided abbreviation. \simplexl and \simplexr could also work in a pinch.

[Nick Ward]

There also seems to be precedent for adding multiple abbreviations, so we could probably get away with \s[] + \simplex or \simp.

[Nick Ward]

I'm happy to open a PR. Should we do a poll first, or are people just anxious to get typing as soon as possible?

[Emily Riehl]

I think if you and @Jon Eugster come to a consensus, we'd be happy to go along. All of the options seem reasonable and I suspect we'll get used to them quickly.

[Jon Eugster]

I'd say go ahead creating that PR and don't be afraid to add multiple abbreviations for the same thing

(btw, I'd add \simplex instead of \simp as typing \simp , \simpl , \simple , will all already give the right thing, similarly to how you only need \fo of \forall to get the ∀)

You could for example PR these 5:

    "lean4.input.customTranslations": {
        "s[]": "⦋$CURSOR⦌",
        "s[]_": "⦋$CURSOR⦌_",      <-- not sure this is needed for nicer behaviour
        "simplex": "⦋$CURSOR⦌",
        "lsimplex": "⦋",
        "rsimplex": "⦌"
    }

or any variation of that, as you feel like. I don't think it matters as long as the abbrevs exist, so you should probably just make the call :)

[Nick Ward]

Good call on \simplex over \simp. I'm not sure I understand the reason other bracket abbrevs have the [$CURSOR]_ version, but maybe a reviewer of the PR can confirm whether we need it or not.

[Nick Ward]

vscode-lean4#579

[Emily Riehl]

FYI this has now been merged into vscode. Just restart your lean extension and you've got the nifty new commands \simplex \lsimplex and \rsimplex!

[Emily Riehl]

I'm finding these very intuitive to use. Thanks to @Nick Ward and @Jon Eugster et al for thinking about this so carefully.

[Emily Riehl]

Regarding the truncated versions of the simplicial notations @Joël Riou seems pretty happy with the current state of the PRs #20688 and #20719 but requests a review by some expert in meta code. @Kevin Buzzard can you help us find such a reviewer? I'd love to start using these for some open PRs...

[Emily Riehl]

@Nick Ward feel free to chime in with any additional context/discussion.

[Nick Ward]

Nothing to add here, I think both PRs are ready for review but agree it would be good to have a metaprogramming expert provide some input. Maybe #PR reviews > #20688 truncated simplicial notations will pique someone's interest.

[Nick Ward]

Also, just to throw the idea out there -- if we find that we frequently want to use mathlib PRs in the infinity-cosmos repo before they are merged into the master branch of mathlib, we could consider maintaining our own mathlib branch / fork and pointing the infinity-cosmos repo there.

[Emily Riehl]

Nick Ward said:

Also, just to throw the idea out there -- if we find that we frequently want to use mathlib PRs in the infinity-cosmos repo before they are merged into the master branch of mathlib, we could consider maintaining our own mathlib branch / fork and pointing the infinity-cosmos repo there.

This is something worth considering. I'd be interested in hearing pluses and minuses. Though in the case of #20688 I'm eager to use it for the mathlib PRs we've been working on for the past few months rather than infinity-cosmos repo stuff ;)

[Nick Ward]

In terms of pros, the obvious advantage is the ability to adapt more of a "move fast and break things" mentality on this hypothetical cosmos-develop branch (whether that is really a pro is a matter of group preference, I think).

It might also make it a bit easier to keep track of PRs as they move from the infinity-cosmos repo to mathlib. It seems to happen often that we have a stale version of a change in the infinity-cosmos repo while the real change is continuously updated in the form of a mathlib PR. Then once the mathlib PR is merged we are finally able to remove the stale version of the change from infinity-cosmos and reconcile the two repos. By maintaining an experimental cosmos-develop branch of mathlib, we could track the current state of relevant changes more closely.

For cons, maintaining a mathlib branch has the potential to be very time-consuming depending on how "bleeding edge" we want it to be. Stability could be a problem, and we risk basing lots of infinity-cosmos work on PRs that might ultimately be rejected from mathlib or otherwise altered significantly.

[Kevin Buzzard]

Emily Riehl said:

Regarding the truncated versions of the simplicial notations Joël Riou seems pretty happy with the current state of the PRs #20688 and #20719 but requests a review by some expert in meta code. Kevin Buzzard can you help us find such a reviewer? I'd love to start using these for some open PRs...

This is still on my job list but right now both PRs have merge conflicts.

[Emily Riehl]

Looks like @Nick Ward fixed them.

[Nick Ward]

#20688 is merged, so the notations ⦋m⦌ₙ, X _⦋m⦌ₙ, and X ^⦋m⦌ₙ should be available in mathlib now. The delaborators are yet to come (#20719), so the notations won't pretty-print in the infoview for now.

Thanks to everyone who took the time to review!

[Emily Riehl]

Nick Ward said:

#20688 is merged, so the notations ⦋m⦌ₙ, X _⦋m⦌ₙ, and X ^⦋m⦌ₙ should be available in mathlib now. The delaborators are yet to come (#20719), so the notations won't pretty-print in the infoview for now.

Thanks to everyone who took the time to review!

Hallelujah and congratulations! This is very much appreciated.

[Emily Riehl]

@Nick Ward or @Mario Carneiro could you help me sort out the use of these new notations? I believe I should be able to delete lines 39-44 here and replace them with open SimplicialObject.Truncated.

Aside: it's not clear to me which truncated namespace is being opened here:

open Category Functor Limits Opposite SimplexCategory Simplicial SSet Nerve Truncated

This mostly works except I get an error on the arguments x around line 300:

theorem toNerve₂.ext (F G : X ⟶ nerveFunctor₂.obj (Cat.of C))
    (hyp : SSet.oneTruncation₂.map F = SSet.oneTruncation₂.map G) : F = G := by
  have eq₀ x : F.app (op ⦋0⦌₂) x = G.app (op ⦋0⦌₂) x := congr(($hyp).obj x)

which seems to be confusion about where x : X_⦋0⦌₂or whether x is a proof that 0 is less than or equal to 2.

[Nick Ward]

I believe you also need to open SimplexCategory.Truncated to get access to the ⦋0⦌₂ notation.

[Nick Ward]

If #18230 lands, I'd like to pull all of these notations into the Simplicial namespace.

[Nick Ward]

@Emily Riehl I have reproduced the issue, but not sure what the problem is yet. Apologies for missing NerveAdjunction.lean in the notation PR itself.

[Nick Ward]

I was able to solve by adding type annotations for x as below. Still not sure what the source of the confusion is, though.

  have eq₀ (x : X _⦋0⦌₂) : F.app (op ⦋0⦌₂) x = G.app (op ⦋0⦌₂) x := congr(($hyp).obj x)
  have eq₁ (x : X _⦋1⦌₂) : F.app (op ⦋1⦌₂) x = G.app (op ⦋1⦌₂) x := congr((($hyp).map ⟨x, rfl, rfl⟩).1)

[Emily Riehl]

No need to apologize. I'm not bothered now that I see how easy the fix is. BTW I just opened this as PR #22906.