notation for filters

Stream: general

[Bernd Losert]

Having worked with filters in mathlib for a while, I've noticed that order.filter.basic can't make up its mind about which notation to use for filters:

• Sometimes it uses f and g (e.g. in docs#filter.prod_comm). I think this choice is bad because then you need to use different letters for functions (like m), which for a mathematician used to seeing f for functions is quite odd.
• Sometimes it uses F and G (e.g. in docs#filter.prod_map_map_eq'). This choice is better, but you run into problems if you're dealing with filters on groups and G is generally used for groups.
• Sometimes it uses a, b and x, y (e.g. in docs#filter.tendsto.prod_map and docs#filter.tendsto_prod_iff). This goes against the use of these variables for inhabitants of types and members of sets.
• Sometimes it uses l (e.g. in docs#filter.map_inf_principal_preimage). This is admittedly better than all of the above options, but if you are dealing with more than one filter, I find it awkward being limited to l.
• The neighborhood filters and the principal filters use bold curly math: 𝓝, 𝓟.

In my own project, I've been using normal curly math letters, like ℱ, 𝒢, etc. for filters. This curly math letter notation is also used in the math literature.

I would like to propose to make the filter notation consistent throughout mathlib. I vote for using the bold curly math letters. I would also like to volunteer to do this refactoring work (or help someone that already had this idea). Thoughts?

[Yaël Dillies]

It's a bit harder to write and filters are everywhere. To me, it only makes sense to change the letters if you're heavily reworking one file anyway. I agree that having the same letters across files is useful (then you can copy-paste code and not spend 5min change letters one by one), but it's pretty low priority.

[Bernd Losert]

It's a bit harder to write

This is not a good argument given the crazy amount of fancy unicode mathlib uses.

[Bernd Losert]

it's pretty low priority

Indeed. But I would be happy to do it either way.

[Andrew Yang]

But usually the name of the variables are not fancy unicode.
Also \McF is quite exceptionally hard to write (compared to other sequences) for people that doesn't really know how to press the shift key like me.

[Bernd Losert]

I find it surprising that this is a problem. I was originally using plain ascii in my project and everybody was egging me to use fancy unicode instead. And now the tables have turned!

[Yaël Dillies]

We use ASCII for terms and fancy unicode for types. You were using ASCII for types. You now want to use fancy unicode for terms.

[Bernd Losert]

But lean/mathlib also uses fancy unicode in terms, e.g. in relations and operators, subscripts, superscripts, etc. In any case, my preference is to use the math notation from the literature. Ultimately, I don't really care what notation is used, as long as it is consistent.

[Yaël Dillies]

For reference, I used fancy unicode for docs#finset.shadow and I regret it.

[Yaël Dillies]

And I'm taking its generalization to any boolean algebra as an opportunity to get rid of the fancy unicode.

[Bernd Losert]

Never heard of shadows. In what branch of math do they appear?

[Yaël Dillies]

Set family combinatorics. The shadow of a set family A (a set of sets) is the set of sets you can get to by removing one element of some set of A.

[Bernd Losert]

Ah, I should have realized it was combinatorics since it's under combinatorics.set_family.

[Yury G. Kudryashov]

For me, the main objection against using fancy unicode for variables is that in this case we shouldn't use the same unicode letters in notation.

[Frédéric Dupuis]

I personally like l, it doesn't look like a function and it's easy to type. And we can easily have variants: l', l₁, l₂, ℓ, and so on.

[Kevin Buzzard]

I think the idea of fancy curly letters for filters is a great one. I don't think you hear the authors of textbooks complaining that they don't want to use fancy letters because they take too long to LaTeX. I'm all for the normal mathematical notation being using throughout mathlib, if makes it easier to read, despite possibly being harder to write

[Bernd Losert]

if makes it easier to read, despite possibly being harder to write

This brings up a good point: The code is going to be read more often that it will be written, so it makes sense to optimize for readability.

[Bernd Losert]

I personally like l, it doesn't look like a function and it's easy to type. And we can easily have variants: l', l₁, l₂, ℓ, and so on.

I've seen la and lb as well. Is this also OK?

[Yury G. Kudryashov]

If we're going to use \Mc* letters for filters, then we should agree on some relatively small set of letters that can be used for filters and shouldn't be used in notation.

[Yury G. Kudryashov]

Later we might need to shrink this list.

[Adam Topaz]

Just my 2c: I loathe writing the \Mc* characters. It goes against all of my built in latex muscle memory. I tend to just use a Roman F (maybe with some decorations) for filters.

[Johan Commelin]

Could we patch the VScode translations to (also) have \mathcalF etc? If that would make life easier?

[Adam Topaz]

My usual latex macros are \Fcal, \Ffrak etc.

[Adam Topaz]

I suppose I could set up my vscode/emacs with custom commands such as this.

[Adam Topaz]

I guess the question is... Does anyone actually like \Mc*?

[Frédéric Dupuis]

I also really hate typing \Mc*.

[Patrick Massot]

Same here

[Patrick Massot]

I do use custom translations in VSCode

[Yaël Dillies]

Adam Topaz said:

I guess the question is... Does anyone actually like \Mc*?

Me, a bit, when I want several terms called a .

[Mario Carneiro]

I agree with Yury's objection. Fancy letters are usually used for notations; I had to check whether they are even legal identifier characters (they are)

[Stuart Presnell]

After years of using Latex I have to admit the novelty of being able to type fancy Unicode characters in just a few keystrokes still hasn’t worn off.

[Mario Carneiro]

I believe the convention with curly letters in mathematics is to use them for sets of sets, which is why filters are often written as such

[Mario Carneiro]

Although one of these days we'll generalize filters to sets in a preorder and then the convention won't be as good

[Mario Carneiro]

Also, it's true that they are harder to write but more important to me is that they are harder to read. I always had to go get a dictionary when looking at mathscr and mathfrak letters

[Yaël Dillies]

I'm actually longing to doing this refactor, but I got told it involved convincing Patrick.

[Mario Carneiro]

and this is exacerbated on a reasonably small monospace font

[Adam Topaz]

@Yaël Dillies I wasn't wondering about whether people like the curly letters themselves, but rather the macro \Mc* used to type them.

[Adam Topaz]

I think with \McF it's fairly awkward to type an uppercase letter, followed by a lowercase one, followed by an uppercase one. Typing \Fcal is much easier IMO

[Yaël Dillies]

Ah yeah no. I use it but I don't understand it.

[Bernd Losert]

It seems the discussion has derailed to a discussion about how to type fancy unicode. In this regard, let me say that I use vim with custom digraphs for all the fancy unicode, which are even harder to type. For example, I have to type C-k FQ to get ℱ. Ultimately, typing anything non-ascii sucks, be it in vim, vscode, emacs, etc.

Anyways, so far, it seems that the majority are against the curly math letters. This is fine. Frédéric Dupuis suggested using l. How do people feel about this?

[Adam Topaz]

Looking at https://github.com/leanprover-community/mathlib/blob/master/src/order/filter/basic.lean it seems that the letter f is the most common.

[Alex J. Best]

Adam Topaz said:

I suppose I could set up my vscode/emacs with custom commands such as this.

Its easy to add extra/custom things to the vscode plugin, search in vscode settings for Lean: extra translations and edit it to add

    "lean.input.customTranslations":  {
        "mcF": "ℱ",
    },

[Patrick Massot]

Yaël Dillies said:

I'm actually longing to doing this refactor, but I got told it involved convincing Patrick.

I may have missed some messages and I'm a bit lost. Which refactor do you want to do? Using McF?

[Patrick Massot]

Bernd Losert said:

Ultimately, typing anything non-ascii sucks, be it in vim, vscode, emacs, etc.

I disagree. Using \a to type $\alpha$ is really easy and efficient, whatever the editor. He the issue is that we have three characters alternating upper case and lower case. When I need to type \McF a lot I simply give it a shorter abbreviation.

[Patrick Massot]

Stuart Presnell said:

After years of using Latex I have to admit the novelty of being able to type fancy Unicode characters in just a few keystrokes still hasn’t worn off.

There is nothing preventing you from doing that in LaTeX as well. You simply need a modern TeX compiler such as xeLaTeX or LuaLaTeX.

[Bernd Losert]

Using \a to type α is really easy and efficient, whatever the editor.

That assumes you're using vscode with the lean extension. That doesn't work in e.g. nano, regardless of how you configure it.

[Reid Barton]

We don't support people who are trying to make things difficult for themselves--why take away their fun?

[Alex J. Best]

It also works in vim with https://github.com/Julian/lean.nvim and emacs has the same support (https://github.com/leanprover/lean-mode). The abbreviations files are kept synced so while getting the best abbreviations is always a work in progress everyone can use one of these 3 common editors easily

[Yury G. Kudryashov]

You can also configure ~/.XCompose (if you're using Linux)

[Yury G. Kudryashov]

Or some more advanced input method. Pro: it will work in any app.

[Eric Rodriguez]

Yury G. Kudryashov said:

You can also configure ~/.XCompose (if you're using Linux)

(windows has WinCompose; i've sadly never found an equivalent for MacOS)

[Julian Berman]

There's Settings > Keyboard > Text on macOS if you want replacements to work globally. But it doesn't use a compose key obviously, you can just stick \a -> α in there or whatever.

[Bernd Losert]

Julian Berman said:

There's Settings > Keyboard > Text on macOS if you want replacements to work globally. But it doesn't use a compose key obviously, you can just stick \a -> α in there or whatever.

That doesn't work uniformly across all applications. It works fine in TextEdit, but not if you're in the Terminal. Even fancier programs like https://textexpander.com/ don't work correctly across all applications.

[Bernd Losert]

In any case, we're going off-topic again.

Looking at https://github.com/leanprover-community/mathlib/blob/master/src/order/filter/basic.lean it seems that the letter f is the most common.

I get this in mathlib:

$ git grep 'f : filter' | wc -l
     395
$ git grep 'l : filter' | wc -l
     398

[Bernd Losert]

Here's a general summary:

$ git grep -ho '\w\+ : filter' | sort | uniq -c
   1 1 : filter
   1 A : filter
   9 B : filter
   1 C : filter
  35 F : filter
   6 G : filter
   1 H : filter
   8 L : filter
   2 U : filter
  19 a : filter
  22 at_bot : filter
  29 at_top : filter
  14 b : filter
   6 c : filter
   4 cofinite : filter
   1 compact_conv_nhd_filter_is_basis : filter
   1 compact_convergence_uniformity : filter
   2 d : filter
   1 default : filter
 392 f : filter
   1 fa : filter
   1 fb : filter
   5 fi : filter
   1 filter : filter
   1 filter_empty : filter
   1 filter_local : filter
   1 filter_map_eq_filter : filter
   1 filter_zero : filter
 114 g : filter
   1 generate_empty : filter
   1 generate_univ : filter
  16 h : filter
   1 hFf : filter
   5 have : filter
   2 hf : filter
   1 hk : filter
   2 k : filter
 397 l : filter
   9 la : filter
   1 large : filter
  17 lb : filter
  11 lc : filter
   4 li : filter
   4 lt : filter
   1 map_compose : filter
   1 map_id : filter
   1 map_map : filter
   1 map_monoid_hom : filter
   1 outer : filter
  28 p : filter
   1 stone_cech_unit : filter
   1 t : filter
   1 tendsto_abs_cocompact_at_top : filter
   5 u : filter
   1 uniformity : filter
  31 x : filter
  14 y : filter
   4 z : filter

[Mario Carneiro]

I think this shows a clear preference for f, g or l

[Mario Carneiro]

and I don't think it's necessary to make one choice between these two across the board

[Mario Carneiro]

I do think that a,b,c are bad names for filters unless they are mnemonic for something

[Frédéric Dupuis]

Well, the situation right now when you're searching for lemmas about filters is that you'll find some where f is a filter and some where f is a function, depending on which file your search lands in.

[Frédéric Dupuis]

It feels more or less 50-50, and apparently the numbers bear this out.