naming convention: `UniformSpace.Completion` morphisms

Stream: mathlib4

[Jireh Loreaux]

Currently the naming convention surroounding bundled morphisms concerning docs#UniformSpace.Completion is inconsistent. For example, given a morphism α →?hom β, the map UniformSpace.Completion.map : Completion α →?hom Completion β is called, for various morphisms:

1. docs#AddMonoidHom.completion
2. docs#NormedAddGroupHom.completion (matches the above)
3. docs#UniformSpace.Completion.mapRingHom

And in #33116, the author (@Gregory Wickham) is adding a version for continuous ilnear maps. Which of the above should we choose? I see arguments in both directions: (a) choose .completion to allow for dot notation, (b) choose the namespaced mapHom because it mentions map and when we're working with completions, we'll often have the namespace opem already.

My complaint with (a) is that there is no mention of map, and there are other things it could reasonably be (e.g., extension or coe). Note that along the lines of these other possibilites, we have the terrible (guess which morphism it is before clicking!) docs#UniformSpace.Completion.extensionHom, we also have docs#UniformSpace.Completion.coeRingHom, docs#Isometry.extensionHom, docs#NormedAddGroupHom.extension. And finally we have docs#normedAddGroupHomCompletionHom, which is a bundling of docs#NormedAddGroupHom.completion into an AddMonoidHom between spaces of NormedAddGroupHoms.

So, what do we prefer? I think my preference, if I were to do it from scratch would be: given α →?hom β, to name:

1. Hom.completionCoe : β → Completion β. This is not a typo, I really mean α in both places because we can just compose with this map to go from α → Completion β.
2. Hom.completionExtension : Completion α → β.
3. Hom.completionMap : Completion α → Completion β.

(1) allows for anonymous dot notation, while (2) and (3) allow for dot notation. In addition, this more closely follows our naming convention (than e.g., AddMonoidHom.completion) because this is about Completion.map (which becomes completionMap according to our conventions).

cc @Monica Omar

[Sébastien Gouëzel]

What about Hom.toCompletion for the version α → Completion β, and Hom.fromCompletion for the version Completion α → β (already assuming that beta is complete, probably) and Hom.completion for Completion α → Completion β? This looks easier to remember to me.

[Jireh Loreaux]

It's clear enough, so I'm fine with that, but I'll point out that it's sort of special casing an exception to our naming conventions

[Sébastien Gouëzel]

What is the naming convention that would apply here?

[Jireh Loreaux]

I just mean that we name things in terms of what's involved. Since this is a bundling of Completion.map, presumably map would appear in the name.

[Sébastien Gouëzel]

It's true that A.toB normally turns A into something of type B, and my proposal doesn't respect that...

[Sébastien Gouëzel]

Maybe I'm arguing that Completion.map should be renamed Function.completion...

[Jireh Loreaux]

Without a UniformSpace. preceding it? That sounds potentially confusing.

[Sébastien Gouëzel]

Yes, that's a bad idea, there are too many kinds of completions.

[Sébastien Gouëzel]

So toCompletion, fromCompletion and completionMap?

[Jireh Loreaux]

toCompletion and fromCompletion still don't mention the underlying function (though you could argue coe isn't much better). But I was only pointing this out, not necessarily dictating. Like I said above (about toCompletion, fromCompletion and completion):
Jireh Loreaux said:

It's clear enough, so I'm fine with that

[Monica Omar]

I like toCompletion and fromCompletion.
completionMap is okay, but maybe .Completion.map is also fine?

[Monica Omar]

Actually, completionMap is better, so, in the case of continuous linear maps, we can just have UniformSpace.completionCLM?

[Sébastien Gouëzel]

I think it is important to have dot notation. So, if A is a continuous linear map, I would like A.completion or A.completionMap or whatever to be valid for the continuous linear map between the completions.

[Monica Omar]

Yeah, I agree, that's what I was thinking too

[Monica Omar]

What would docs#Isometry.extensionHom be called? The current naming doesn't even mention what kind of homomorphism.

[Sébastien Gouëzel]

Isometry.fromCompletion?

[Monica Omar]

How about RingHom.Isometry.fromCompletion?

[Monica Omar]

Or RingHom.fromCompletion_of_isometry? But I like the dot notation one better

[Sébastien Gouëzel]

The only one enabling dot notation is Isometry.fromCompletion, right?

[Monica Omar]

RingHom.Isometry.fromCompletion too, but you would need to have RingHom opened for it to work (which is why I'm suggesting it)

[Sébastien Gouëzel]

If h : Isometry f (where Isometry is in the root namespace), are you saying that h.fromCompletion would work if one defines RingHom.Isometry.fromCompletion and RingHom is open? I didn't know that!

[Monica Omar]

Yeah! But note that you need to explicitly open RingHom and not just be in the namespace RingHom

[Monica Omar]

Even though namespace opens it..?

[Sébastien Gouëzel]

Indeed it works:

import Mathlib

def Foo.Nat.selfy (n : ℕ) : ℕ := n

open Foo

lemma bar (n : ℕ) : n.selfy = n := rfl

I'd like to be sure it's a feature and not a bug, though :-)

[Jireh Loreaux]

If we're going with to and from, I think that bare completion is fine (and involves fewer deprecations).

[Monica Omar]

I'd like to be sure it's a feature and not a bug, though :-)

I think the part where we need to do open Foo rather than just be in the Foo namespace is a bug:

import Mathlib

def Foo.Nat.selfy (n : ℕ) : ℕ := n

namespace Foo

example (n : ℕ) : n.selfy = n := rfl -- fails

open Foo

lemma bar (n : ℕ) : n.selfy = n := rfl

[Sébastien Gouëzel]

For me, it's rather the last one working which looks like a bug. But in any case the fact that one works and not the other is definitely a bug :-)

[Jireh Loreaux]

I think @Kyle Miller added this feature (intentionally), but I can't never remember how to find the thread that mentioned it.

[Monica Omar]

Alright, I can do all the renames and stuff next week, unless someone wants to do it asap?
But, I guess, for now, we can have the new definition of ContinuousLinearMap.completion @Gregory Wickham?

[Sébastien Gouëzel]

With this feature, I think it would even make sense to rename Completion.map to UniformSpace.Function.completion.

[Yaël Dillies]

Jireh Loreaux said:

docs#UniformSpace.Completion.mapRingHom

This looks best to me as there are many other kinds of completion out there

[Yaël Dillies]

Sébastien Gouëzel said:

With this feature, I think it would even make sense to rename Completion.map to UniformSpace.Function.completion.

Sorry but I am still of the opinion that this "feature" shouldn't be used as it makes the naming convention needlessly complicated and unpredictable

[Monica Omar]

Unpredictable how?
I wouldn't say unpredictable, but names do get long yeah. But dot notation is a win I'd say.

[Monica Omar]

This looks best to me as there are many other kinds of completion out there

I know you dislike this, but what about UniformSpace.RingHom.completion?

[Sébastien Gouëzel]

Yaël Dillies said:

Jireh Loreaux said:

docs#UniformSpace.Completion.mapRingHom

This looks best to me as there are many other kinds of completion out there

I don't see what other kind of completion this could be for ContinuousLinearMap.completion, say.

[Monica Omar]

Or docs#NormedAddGroupHom.completion

[Aaron Liu]

Jireh Loreaux said:

I think Kyle Miller added this feature (intentionally), but I can't never remember how to find the thread that mentioned it.

• #lean4 > dot notation and open
• #lean4 > open is confused