TwoSidedIdeal.map and TwoSidedIdeal.comap defined wrong?

Stream: mathlib4

[Edison Xie]

I've just learnt that we shouldn't use FunLike in definitions, does that mean our definition of TwoSidedIdeal.mapand TwoSidedIdeal.comap is wrong?

[Edison Xie]

what's our convention about using FunLike and actual homs?

[Edison Xie]

Btw I've just found out Ideal.map and Ideal.comap also uses FunLike, so is it the other way around that we should use FunLike for defs?

[Edison Xie]

@Bhavik Mehta @Andrew @Eric Wieser

[Eric Wieser]

I think we're mid-pivot here towards not using FunLike in defs

[Edison Xie]

so does that mean we need to refactor all of the defs I've mentioned above?

[Edison Xie]

apparently Submonoid.comap and Submonoid.map also uses FunLike but Subring.map and Submodule.map uses actual homs :-(

[Edison Xie]

so I just did some experiments and if I changed the definition of TwoSidedIdeal.comap from taking FunLike to taking →ₙ+* and suddenly all the lemma involving actual ringhoms fails and the coercion from RingHom to NonUnitalRingHom doesn't fire :smiling_face_with_tear: Is there a fix for this? @Eric Wieser

[Ruben Van de Velde]

Probably there is a fix. Not sure what it is based on your description

[Eric Wieser]

Perhaps we should first change Submonoid.map/comap before changing everything else at once

[Kevin Buzzard]

Looking over Edison's shoulder, the problem seemed to be that with the refactor for Ideal.map and TwoSidedIdeal.map he had f : A ->+* B and when using it to push forward and pull back two-sided ideals he could not use f directly and had to write f.toNonUnitalRingHom everywhere.

[Eric Wieser]

Does adding a Coe instance fix that?

[Edison Xie]

Eric Wieser said:

Does adding a Coe instance fix that?

I just tried and it still gives me the same error

[Edison Xie]

Application type mismatch: The argument
  f
has type
  R →+* S
but is expected to have type
  R →ₙ+* ?m.13
in the application
  comap f

[Aaron Liu]

oh it's this problem again

[Aaron Liu]

the coercion isn't found because you have metavariables

[Kevin Buzzard]

I have no idea what unification hints are but can this be solved with unification hints?

[Aaron Liu]

see lean4#7440

[Edison Xie]

So does that mean currently the definition has to stay what they were until we fix that issue? :smiling_face_with_tear:

[Eric Wieser]

I think it's ok to write f.toNonUnitalRingHom or (f : R →ₙ+* S) to make things happy

[Kevin Buzzard]

It does feel like a regression though. Imagine the PR: change the definition to take a non unital ring hom, add lots of type annotations which weren't needed before, looks like you're going in the wrong direction :-/