implicit variable in ring_equiv.subring_map

Stream: general

[Filippo A. E. Nuccio]

I don't understand why the subring variable {s} in docs#RingEquiv.subringMap or docs3#ring_equiv.subring_map is implicit. To me, it seems that the idea of this def is that I have a ring equivalence f : S -> R and an explicit subring s of S and I create f.subring_map s.

[Eric Wieser]

I think the idea is that your have an x : s and let lean infer s

[Eric Wieser]

So you can write e.subring_map x

[Jireh Loreaux]

The nice thing about Lean 4 is that we now have the e.subring_map (s := s) syntax, so that we can (modulo a few extra characters) refer to the unapplied map itself. I think we should opt for implicit arguments in cases like these where we will often be applying the result to an element so that Lean can infer the type. In Lean 3 I may have preferred explicit arguments because we would have to write @ to get the map itself if there wasn't enough context to infer s.

[Johan Commelin]

@Eric Wieser Did you mean e.subring_map x?

[Filippo A. E. Nuccio]

Oh, sure, I see. Thanks!

[Notification Bot]

Filippo A. E. Nuccio has marked this topic as resolved.

[Eric Wieser]

Eric Wieser said:

I think the idea is that your have an x : s and let lean infer s

To be clear, I'm not saying this is necessarily the right choice, just that it seems to be the one that was made in the past.

[Notification Bot]

Filippo A. E. Nuccio has marked this topic as unresolved.

[Filippo A. E. Nuccio]

As a matter of fact, I have been thinking about this a bit more and I am not sure I am still convinced. In my experience, when we have a function f we are happy to write f x but when one is after an equivalence in some proof, this is typically in order to prove either that such an equivalence exists (to show that two things are isomorphic), or may be to invert it, or the like. At any rate, one is often more interested in the equivalence as a gadget that something that is meant to be evaluated. So I would advocate for marking s explicit and possibly to add a RingEquiv.subringMap_apply (if I got the camel right... :camel: ) where the subring is implicit and the element is explicit, so that the subring gets inferred by it.

[Filippo A. E. Nuccio]

Jireh Loreaux said:

The nice thing about Lean 4 is that we now have the e.subring_map (s := s) syntax, so that we can (modulo a few extra characters) refer to the unapplied map itself. I think we should opt for implicit arguments in cases like these where we will often be applying the result to an element so that Lean can infer the type. In Lean 3 I may have preferred explicit arguments because we would have to write @ to get the map itself if there wasn't enough context to infer s.

Good point, but I think that (see my message above) most of the time the "unapplied" equivalence is what shows up, while "unapplied functions" are indeed rare, and I understand both the (old) @ use or the new (s := s) in such rare cases.

[Jireh Loreaux]

Hmmm... yes, it would be interesting to have a collection of examples to see which is more common.