Quotient map explicit arguments

Stream: mathlib4

[Patrick Massot]

Is there any reason why docs#QuotientGroup.map and docs#Submodule.mapQ take the subobjects are explicit arguments? Is this done so that writing proofs on the fly is more convenient? It would be really nice to have documentation when such choices are made.

[Patrick Massot]

Note that the map could also be implicit, but I understand this would seem a bit weird (although we could also switch to a version that takes any map and has property only under appropriate assumptions).

[Eric Wieser]

(I assume you mean docs#Submodule.Quotient.map, which doesn't exist?)

[Edward van de Meent]

are you thinking of docs#Submodule.mapQ ?

[Patrick Massot]

Sorry, I meant mapQ

[Patrick Massot]

This is one of our many inconsistencies in naming.

[Patrick Massot]

I fixed the original post.

[Patrick Massot]

I just checked very quickly that the file defining quotient module compiles without any trouble after making those arguments implicit, the only adaptation being to remove those arguments. But this experiment doesn’t say whether it would have been more painful to write.

[Edward van de Meent]

i imagine there might be some cases where it gets used as Quotient.map N M f (by _), which could be considered a tad more annoying to write...

[Edward van de Meent]

where you rely on the explicit parameters to fill in the precise type required of by _

[Patrick Massot]

I understand this possibility, this is why I said that fixing existing proofs is not completely convincing. But I would like to know whether leaving those arguments implicit has actually been tried.

[Kevin Buzzard]

Now of course we can write (N := N) to mitigate against this, when preparing a proof.

[Matthew Ballard]

I would mainly be worried about the strain placed on the elaboration. But it should be tried.

[Patrick Massot]

Matthew, is there any reason you fear this more than with a random implicit argument?

[Matthew Ballard]

I have run into situations before involving significant differences in performance where the arguments to the quotient are implicit or explicit. I don't think this is one and I can't put my finger on the exact cause or line of code at the moment.