RFC: notation for continuous maps in algebra

Stream: mathlib4

[Kevin Buzzard]

Mathlib needs to invent notation for various structure-preserving maps and isomorphisms which in the literature are just denoted by $\to$ and $\cong$; this is just a necessary consequence of our design decisions. For example, ring homomorphims are →+* and ring isomorphisms are ≃+* which I think is great, it's pretty easy to guess what these notations mean with high accuracy (in the sense that someone who knew nothing about mathlib might have a chance of guessing them). Similarly for $R$-modules and $R$-algebras we have things like →ₗ[R] (linear map) and ≃ₐ[R] (algebra isomorphism).

More and more I'm finding myself having to deal with topological algebraic objects as part of FLT. We have gone for ≃ₜ for topological isomorphisms, which also seems reasonable. Recently we merged additive/multiplicative isomorphisms between topological objects and used notation ≃ₜ+ and ≃ₜ* and these notations seem good to me. But actually in some sense they clash with another convention which we have; docs#ContinuousLinearMap s are →L[R], continuous linear equivs are ≃L[R], and continuous algebra maps are →A[R], so the convention has been "turn the small letter into a capital letter to indicate continuity", which can only be applied in situations where there is a small letter in the first place.

These two conventions are now on a crash course with each other, because I want bicontinuous algebra isomorphisms in FLT (in fact we have them locally and I am preparing a PR for mathlib); the "add a t" convention suggests ≃ₜₐ[R] and the "make it capital" convention suggests ≃A[R].

Having thought about it, I think I prefer the "adding a t" convention, because I think it's easier to understand: "ta" for "topological algebra". However it's one character longer, and I have never used things like ≃L[R] before so am not particularly attached to them. I also think that the "add a t" convention to indicate bicontinuity conforms to our conventions where we add a * to indicate preservation of multiplication etc etc.

I've had very little experience with polls but I'm about to try and set one up to see if I can get some kind of consensus for what bicontinuous algebra isomorphisms should be called.

[Kevin Buzzard]

/poll What should bicontinuous algebra isomorphisms be called?
≃A[R]
≃ₜₐ[R], and also change →SL[σ] to →ₜₛₗ[σ], →L[R] to →ₜₗ[R], →A[R] to →ₜₐ[R], ≃SL[σ] to →ₜₛₗ[σ], and ≃L[R] to ≃ₜₗ[R]

[Eric Wieser]

What do continuous affine maps become?

[Kevin Buzzard]

erm →ₜᵃ[R]? I didn't even know these things existed until today

[Jireh Loreaux]

Kevin, note that there is already inconsistency elsewhere because we do have notation for some things on paper. E.g., we use C(α, β) instead of α →ₜ β. I find →ₜₗ[R] a bit hard to swallow because we don't call them "topological linear maps".

[Yaël Dillies]

Sadly, \_c gives ₐ

[Jovan Gerbscheid]

I agree that there is some room for improvement, and we should try to have these notations be more guessable. As @Yaël Dillies said, we can't use a subscript c for continuous, because it doesn't exist. But instead, we can use normal script c (or superscript ᶜ). I think that is more readable than the subscript ₜ. So I propose

→SL[σ] to →cₛₗ[σ], →L[R] to →cₗ[R], →A[R] to →cₐ[R], →ᴬ[R] to →cᵃ[R] (or →ᶜᵃ[R])
And the ≃ versions analogously.

[Yury G. Kudryashov]

We also have docs#ContinuousOpenMap docs#ContinuousOrderHom docs#CompactlySupportedContinuousMap docs#ZeroAtInftyContinuousMap that use →C to denote "continuous" part.

[Yury G. Kudryashov]

Also note that A is used both for algebra maps and affine maps. Currently, they differ by subscript/superscript, but it's hard to remember which one is which.

[Jovan Gerbscheid]

Ah I see, they use the capital C, I'd be happy to switch to that one as well.

[Jovan Gerbscheid]

It's really quite annoying that certain letters aren't available as subscript lowercase letters. What do you think about switching to either normal letters (either capital or lowercase), subscript capitals (is only missing X, and not currently supported with a shortcut in lean) or superscript lowercase (has all 26 letters)?

[Jovan Gerbscheid]

In that case we could write af instead of a for affine maps

[Yaël Dillies]

Note that \->c is already notation for docs#CoalgHom

[Jovan Gerbscheid]

I don't think there are any notations where c comes immediately after the →, so there wouldn't be any notation overlap

[Jovan Gerbscheid]

(Your example uses A →ₗc[R] B)

[Jovan Gerbscheid]

/poll What should we write for (Continuous) AlgHom, AddMonoidHom, (semi) LinearMap, AffineMap and friends? (and the analogous notations for the Equiv versions with ≃ where applicable)
Current: →ₐ[ ]/→A[ ], →+/→ₜ+, →ₛₗ[ ]/→SL[ ], →ₗ[ ]/→L[ ], →ᵃ[ ]/→ᴬ[ ]
superscript lowercase: →ᵃ[ ]/→ᶜᵃ[ ], →+/→ᶜ+, →ˢˡ[ ]/→ᶜˢˡ[ ], →ˡ[ ]/→ᶜˡ[ ], →ᵃᶠ[ ]/→ᶜᵃᶠ[ ]
Capitals/Pascal case: →A[ ]/→CA[ ], →+/→C+, →SL[ ]/→CSL[ ], →L[ ]/→CL[ ], →Af[ ]/→CAf[ ]
Lowercase: →a[ ]/→ca[ ], →+/→c+, →sl[ ]/→csl[ ], →l[ ]/→cl[ ], →af[ ]/→caf[ ]
subscript Capitals (requires a PR to vscode-lean4): →ᴀ[ ]/→ᴄᴀ[ ], →+/→ᴄ+, →ꜱʟ[ ]/→ᴄꜱʟ[ ], →ʟ[ ]/→ᴄʟ[ ], →ᴀꜰ[ ]/→ᴄᴀꜰ[ ]

[Jovan Gerbscheid]

Are there more opinions on which option to use? One advantage of superscript over normal lowercase is that the same notation can be used in identifiers. For example:

• Submodule.SubtypeL → Submodule.Subtypeᶜˡ
• AffineSubspace.subtypeA → AffineSubspace.subtypeᶜᵃᶠ (see #24295)
• innerₗ → innerˡ
• innerₛₗ → innerˢˡ
• innerSL → innerᶜˢˡ

[Kevin Buzzard]

So the reason we can't have subscript lower case is because there's no c? :-(

[Jovan Gerbscheid]

Indeed (and there is no f)

[Kevin Buzzard]

For some reason I find superscripts so much more intrusive than subscripts. I would love for the system to be consistent though.

[Kevin Buzzard]

I really want to vote for subscripts and to have all the subscripts which should be there :-(

[Jovan Gerbscheid]

In that case let's hope that unicode is open to PRs :sweat_smile:

[Eric Wieser]

Probably a stupid idea, but could we use A ⤳ B vs A → B for continuous vs basic maps? (edit: no, docs#Specializes takes this notation)

[Jovan Gerbscheid]

does it have a ≃ version?

[Eric Wieser]

↭?

[Jovan Gerbscheid]

Apparently, they're adding subscript w,y,z to unicode in the future, meaning that we'll only be missing b,c,d,f,g,q

[Andrew Yang]

I agree that superscripts seem much more intrusive to me somehow. I would rather use subscript t everywhere (for topology, as we do for homeomorphisms) if I had to make a choice.

[Kevin Buzzard]

and what do we do about the f in affine?

[Kevin Buzzard]

The reason I like t is that "continuous isomorphism" sounds to me like "map which is an isomorphism of algebraic structures and also happens to be continuous but its inverse might not be" and "topological isomorphism" sounds less likely to be interpreted that way, whereas Jireh pointed out above that conversely we don't say "topological function", we say "continuous function"

[Jovan Gerbscheid]

what about using subscript whenever possible, and switching to superscript when it is forced?

[Jovan Gerbscheid]

Kevin Buzzard said:

"continuous isomorphism" sounds to me like "map which is an isomorphism of algebraic structures and also happens to be continuous but its inverse might not be"

I think the structure is usually called an Equiv, which I think removes the confusion.

[Yury G. Kudryashov]

I'll try to make up my mind and vote in the next 48 hrs, but now I have to pack for a flight.