naming defs

Stream: general

[Jireh Loreaux]

So here is something that isn't really addressed in the naming convention. Let's say I'm making a def. Obviously the name should describe what it "is". As a typical example, let's say that we have a particular function foo : α → β that we want to bundle into some bar. Natural candidates for the name would be foo_bar or bar_foo, but which one is preferred in mathlib? As explicit example, how should the bundling of the map λ x : ℝ≥0∞, x⁻¹ into an order isomorphism ℝ≥0∞ ≃o order_dual ℝ≥0∞ be called?

[Jireh Loreaux]

/poll Naming bundles
order_iso_inv_dual
order_iso_dual_inv
inv_order_iso_dual?

[Yaël Dillies]

Yours is a bit specific, so maybe it will inherit a trailing _ennreal

[Jireh Loreaux]

yes, it's in the ennreal namespace

[Jireh Loreaux]

why the .? It won't allow for projection notation.

[Yaël Dillies]

Ah, I think it should be in the order_iso namespace

[Jireh Loreaux]

Interesting, why there over ennreal? I can't see using it specifically while I have order_iso open, but I can imagine using it when I have ennreal open.

[Yaël Dillies]

I'm not against reconsidering it, but that's how mathlib already works for the most part.

[Jireh Loreaux]

To make sure I understand, defs of a bundle of type bar belong in the bar namespace, and not in the namespace of the type on which the underlying function is defined?

[Yaël Dillies]

Exactly. In particular because most bundled homs aren't defined on a concrete type, or (more rarely) are defined on two (different) concrete type. They are homs after all!

[Yaël Dillies]

and also because there are usually many strengthenings to be had. For example, I'm fairly sure yours is actually an order homeomorphism.

[Jireh Loreaux]

Sure, it is. Do we have a bundle that does both? If so, I'll add it in my PR.

[Mario Carneiro]

I think the inv should come first, since it is inv with some stuff

[Mario Carneiro]

I don't think you need the _dual unless there is another inv order iso that isn't going to the dual

[Jireh Loreaux]

ah, I see, docs#order_iso.to_homeomorph, the homeomorphism comes for free because the topology on ℝ≥0∞ is the order topology.

[Eric Wieser]

In this case, the order_iso namespace matches docs#order_iso.mul_left

[Anne Baanen]

Also the family of maps named docs#monoid_hom.id, that are id bundled into a monoid_hom.

[Eric Rodriguez]

I would say inv_order_iso, a la docs#polynonial.map_ring_hom, docs#polynomial.eval_ring_hom. But more than anything, why not replace the current definition with the bundled definition?

[Yaël Dillies]

You want to replace inv? :rofl:

[Eric Rodriguez]

Why can't it be made an order_iso from the get go? I'm not sure how notation interfaces with coetofun but we've certainly been bundling more stuff...

[Yaël Dillies]

Well, some div_inv_monoid are not ordered.

[Eric Rodriguez]

the inv is defined separately, it's not defined automatically

[Yaël Dillies]

Still, I don't see how that makes sense. It's like asking "Why is id not an homeomorphism?"

[Eric Rodriguez]

I mean, it is when it can be defined in such a way. Just define inv := the whole shebang, then has_inv := inv, and it should all work out. a mathematician would treat it as an order_iso, why not lean?

[Yaël Dillies]

The inv notation comes from docs#has_inv. You can't put an order_iso in has_inv.

[Eric Rodriguez]

yeah you can, just put the coe_to_fun. and if the name inv isn't taken already, why not just use that?

[Yaël Dillies]

Also, I don't see why the order structure would get priority. There are many other bundlings.

[Eric Rodriguez]

that I can see, but we haven't seemed to need inv as a ring_hom or such like and I don't see any other bundling that is needed (as pointed out above, the homeomorphism is free)

[Yaël Dillies]

This also causes a bootstrap problem. You'll have to prove many properties of inv as you're defining it.

[Yaël Dillies]

and I didn't even mention that if you want to define own inv, you'll have to get it off the algebraic hierarchy. meaning for example that fields won't have an inv anymore.

[Yaël Dillies]

For the record, I tried this with docs#convex_hull and docs#closure_operator, and I regret.

[Eric Rodriguez]

I'm not suggesting to remove it in general. I'm suggesting that ennreal's inv, specifically, can be designed as an order_iso. yea there's bootstrapping stuff, but it shouldn't be too bad considering it's defined as an Inf.

[Jireh Loreaux]

I don't think you want it bundled anyway most of the time anyway. inv goes from ennreal to itself. The bundle goes to it's order_dual.

[Jireh Loreaux]

Eric Rodriguez said:

a mathematician would treat it as an order_iso, why not lean?

I think the key thing here is that mathematicians continuously re-bundle their objects as they prove new things, but you can't really do this formally, because it just means you have to redefine everything all the time. So, in general it's better to provide a separation of concerns, which is why has_inv is just a notation. And when you want the order isomorphism you appeal to the bundle. But As Yaël said, why prefer one bundle over another?

[Frédéric Dupuis]

@Jireh Loreaux I just changed my vote to order_iso.inv_ennreal because I just noticed that order_iso.inv already exists, and is basically the same thing but for groups, so it would be strange for this one to have a very different name.

[Jireh Loreaux]

it just got put on the queue. If someone wants to stop it I'll switch the name. Or can I stop it?

[Eric Wieser]

Can you link the PR? I don't see it mentioned anywhere in this thread

[Rémy Degenne]

Is that a PR I put on the queue? There was a comment about names pointing to a zulip discussion, but it was marked as resolved, so I thought a conclusion had been reached

[Rémy Degenne]

#11869 ?

[Jireh Loreaux]

It was resolved, and then last minute became unresolved. No one's fault. Yes, it was #11869. I'll just submit another PR to change the name.

[Jireh Loreaux]

For future reference, if a PR isn't delegated to me, is it even possible for me to pull it off the queue with bors r-?

[Riccardo Brasca]

I don't think so (but I am not sure). Btw pushing a commit will do.

[Frédéric Dupuis]

Sorry, this is my fault, I should have made it clear in the PR that there was one last thing to do.

[Jireh Loreaux]

#11958

[Jireh Loreaux]

Whoops, sorry, something is off. I used the same branch and I think that's not good.

[Jireh Loreaux]

Okay, this looks correct: #11959