Style for naming a pi type in topology/analysis files

Stream: mathlib4

[Yakov Pechersky]

In #22575, Johan brought up that he'd rather we named our families X or A instead of π : _ → Type*. I checked and this style of using pi happens consistently across topology and analysis files:

$ git grep -e "π : . → Type" | wc -l
95
$ git grep -e "π : . → Type" --name-only | cut -d/ -f-2 | uniq -c
      4 Mathlib/Algebra
      4 Mathlib/Analysis
     10 Mathlib/Data
      2 Mathlib/Logic
      5 Mathlib/MeasureTheory
     16 Mathlib/Order
     21 Mathlib/Topology

Should there be a consistent style, and what should it be?

[Yakov Pechersky]

/poll What should we name pi families in topology/analysis files, especially for Pi instances?

[Etienne Marion]

From naming convention:

Types with a mathematical content are expressed with the usual mathematical notation, often with an upper case letter (G for a group, R for a ring, K or 𝕜 for a field, E for a vector space, ...). This convention is not followed in older files, where greek letters are used for all types. Pull requests renaming type variables in these files are welcome.

[Etienne Marion]

From that I would say that π is not desirable.

[Yakov Pechersky]

Okay, made a programmatic change to switch to X in #22603

[Etienne Marion]

I don't think you should change all the π families in Mathlib to X. This is probably ok when π is a family of topological spaces because I think that it's a common notation (more common than π anyway), but in algebra for example if you have a family of groups you are often going to call it G or H, not X. And in general contexts where the family is not a particular structure (I'm thinking of many things in the Data folder for instance) I think the convention is actually to stick to greek letters.

[Yakov Pechersky]

How about something like the following?

variable {α β ι : Type*} {π : ι → Type*}

instance instIdemSemiring [∀ i, IdemSemiring (π i)] : IdemSemiring (∀ i, π i) :=
  { Pi.semiring, Pi.instSemilatticeSup, Pi.instOrderBot with
    add_eq_sup := fun _ _ ↦ funext fun _ ↦ add_eq_sup _ _ }

instance [∀ i, IdemCommSemiring (π i)] : IdemCommSemiring (∀ i, π i) :=
  { Pi.commSemiring, Pi.instIdemSemiring with }

variable [∀ i, KleeneAlgebra (π i)]

[Johan Commelin]

One thing that personally baffles me is that these families called $\pi$ seem to be everywhere, but I don't remember ever noticing one before :peek: :shrug:

[Yakov Pechersky]

I've narrowed the PR to be on Topology/Analysis/MeasureTheory files

[Etienne Marion]

Would it be ok if you split it in one PR for each folder? Personally I would be glad to turn π into X in the MeasureTheory folder but I don't use Topology and Analysis often enough to have an opinion

[Yakov Pechersky]

Sure, I'll split

[Yakov Pechersky]

In topology, we have the annoying situation where in a line above one has {X : Type*} ...

[Yakov Pechersky]

MeasureTheory: #22604

[Yakov Pechersky]

Analysis: #22605

[Floris van Doorn]

I don't think the fact that a variable is a "family" should dictate what letter is should be. Instead, the name should be whatever we would call a single object with the same type-classes. Is it a family of Banach spaces, then use E, if it is a family of groups, use G, if it is a family of measure spaces, use X, if it is a family of indexing sets, use ι, etc.

[Etienne Marion]

#22604 for MeasureTheory is ready I think

[Yakov Pechersky]

That totally makes sense. I think though in this specific situation of π -- the files containing π speak on a very low level, so there is no canonical name. Said differently, files that discuss groups, Banach spaces, etc weren't in the list that had a π.

Let's say for bornology, the PR now has

variable {α β ι : Type*} {X : ι → Type*} [Bornology α] [Bornology β]
  [∀ i, Bornology (X i)]

instance Pi.instBornology : Bornology (∀ i, X i) where

I am not sure what the better naming would be here.

[Kyle Miller]

I think X looks good here, since bornologies are space-like. Both Wikipedia and ncatlab start the definitions with "let $X$ be a set" as well.

(I think Bornology (Π i, X i) would look even nicer.)

[Yakov Pechersky]

I've updated the Analysis PR according to _M_odule, _R_ing, Seminormed_G_roup (because E and F were taken)
#22605

[Yakov Pechersky]

And I'll leave the ∀ to Π for another day