sup/Sup

Stream: lean4

[Kevin Buzzard]

In Lean 3 we have things like conditionally complete lattices which have a sup (the least upper bound of two things) and a Sup (the least upper bound of a set of things). I've been idly making some lattice theory because I'm thinking about making Lean 4 teaching material for mathematicians. I wrote this:

class HasSup (P : Type u) where
    sup : P → P → P

and now I realise that the capitalisation might cause confusion. Does anyone have advice or suggestions on what I should be doing here?

Of course later on we might well have the same question for group (the structure) and Group (the category).

[Eric Wieser]

For binary/nary, perhaps Sup and NSup, where N means n-ary?

[Eric Wieser]

Then we could even distinguish docs#sum from a generalization of docs#finset.sum by calling the latter HasNAdd. Surely no one will be confused by that /s.

[Gabriel Ebner]

n-ary can (and probably should) be defined in terms of binary. (As much as I'd like to suggest FinSup as the type class for n-ary suprema.) Similarly, indexed suprema can be defined from the set suprema.
Productively speaking, maybe sups (supremum of set) could be an unambigous analogy to supr (supremum of range).

[Mario Carneiro]

I think supS and supR would be better for such an abbreviation, since supr and infi seem to suggest that it's not actually "supremum of range" but rather a slightly different abbreviation of "supremum"

[Patrick Massot]

We need to decide the names of docs#sup, docs#Sup and docs#supr in mathlib4. We can't use capitalization tricks because there are too many capitalization rules that would interfere. There are notations for those three functions of course, but their name will appear in lemma names. How about: sup, setSup, rgSup where rg is the abbreviation of "range"?. Or maybe funSup?

[Patrick Massot]

Note that I wrote something to get the ball running but I don't have any strong feeling (except for the strong filling that order.complete_lattice should be ported).

[Patrick Massot]

Or iSup and iInf where i stands for indexed, but iInf is painful to read.

[Mario Carneiro]

my preference is for sup/sSup/iSup and inf/sInf/iInf , although I don't mind swapping the last pair for supr/infi if it reads better and is more backward compatible

[Patrick Massot]

It took me a very long time to get used to the mathlib3 name so I won't insist on backwards compatibility.

[Mario Carneiro]

if we wanted to chuck backwards compatibility we could also consider meet / join

[Mario Carneiro]

that's probably too much of a change though, and the names are famously hard to keep straight

[Mario Carneiro]

(not sure if sup and inf are much better on that axis though)

[Eric Wieser]

What did we call docs#set.Union in mathlib4?

[Adam Topaz]

docs4#Set.sUnion

[Eric Wieser]

That's docs#set.sUnion

[Eric Wieser]

set.Union is the indexed version, which Patrick's convention would rename to iUnion (and similiary for iInter)

[Mario Carneiro]

I don't think we made it that far @Eric Wieser

[Mario Carneiro]

we have the binary stuff but the indexed operators pull in all of lattice theory

[Eric Wieser]

Much further down the line we have the same naming issue with probability_theory.Indep vs probability_theory.indep

[Eric Wieser]

@Heather Macbeth mentions docs#filter.coprod vs docs#filter.Coprod

[Eric Wieser]

(the other thread is here)

[Patrick Massot]

/poll operator names
sup sSup iSup inf sInf iIinf
sup supS supI inf infS infI
sup supₛ supᵢ inf infₛ infᵢ
join sup iSup meet inf iInf
join sup supI meet inf infI

[Eric Wieser]

@Heather Macbeth, I think your sup sup2 is backwards compared to the other suggestions; you want the 2 subscript for the binary one right?

[Heather Macbeth]

Sorry, yes!

[Adam Topaz]

maybe I got meet/join backwards :)

[Eric Wieser]

Wikipedia says Patrick's interpretatio (meet = inf) is correct, but also says those names are the nary operators!

[Yaël Dillies]

I have a strong preference for the indices versions over the trailing cap ones because capitalisation is a headache in Lean 4.

[Patrick Massot]

One problem with the indices version is that we will also need to solve the bUnion case (in lemma names, this isn't a new operator) and I think there is no subscript b in unicode

[Patrick Massot]

I don't understand Heather sup₂. We need three variants, right?

[Yaël Dillies]

bUnion has mostly been replaced by Union₂ nowadays anyway.

[Yaël Dillies]

There's some remnants that make sense, but it wouldn't be such a loss (as opposed to the situation a year ago, say).

[Eric Wieser]

docs#bUnion still has plenty of results

[Eric Wieser]

docs#bsupr does too

[Eric Wieser]

Patrick Massot said:

One problem with the indices version is that we will also need to solve the bUnion case (in lemma names, this isn't a new operator) and I think there is no subscript b in unicode

Arguably the convention for bounded / conditional operations should use a different convention anyway to the binary/set/indexed naming, since this is a property of the lemma not of the operator

[Yaël Dillies]

#11516 is where the convention changed drastically.

[Eric Wieser]

I think this is a problem for @Heather's sup₂ suggestion for the binary sup, since lemmas about the n-ary one applied twice are certainly common.

[Floris van Doorn]

I prefer it if declaration names are written with ASCII characters, since I sometimes want to type them outside VSCode , where I don't have easy unicode input (e.g. on the mathlib docs website)

[Patrick Massot]

Now that capitalization can no longer be used I think we need extra flexibility so you should take the opportunity to configure your computer to type those everywhere.

[Eric Wieser]

Or we should configure the docs to behave like vscode

[Patrick Massot]

I went with sup supₛ supᵢ inf infₛ infᵢ

[Eric Wieser]

Then we should rename docs4#Set.sUnion to match

[Scott Morrison]

We now run into the problem that Lean 4 doesn't have extends ... renaming ..., but we want to write

class CompleteLinearOrder (α : Type _) extends CompleteLattice α, LinearOrder α
    renaming max → sup min → inf

[Yaël Dillies]

We should just rename min and max in LinearOrder

[Yaël Dillies]

I wanted to do that in Lean 3, but everything was slowed down because linear_order is in core.

[Floris van Doorn]

I like the names min and max.

[Floris van Doorn]

For the renaming of fields: I recommend for now to just add the missing fields of LinearOrder manually, and then to declare the instance manually.

[Yaël Dillies]

Renaming the fields has nothing to do with renaming the functions.

[Yaël Dillies]

But independently we should make LinearOrder extend Lattice

[Scott Morrison]

Okay, I've done CompleteLinearOrder per Floris' suggestion.

[Eric Wieser]

Is docs4#LinearOrder in core/Std4?

[Yaël Dillies]

It moved to mathlib.

[Notification Bot]

This topic was moved to #mathlib4 > sup/Sup by Eric Wieser.

[Eric Wieser]

(this was really a question about what to name things in mathlib)