RingHom.inverse

Stream: Is there code for X?

[Antoine Chambert-Loir]

Is there a reason for which the following definition seems to be absent from mathlib?

def RingHom.inverse (f : R →+* S) (g : S → R)
    (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) : S →+* R :=
  { (f : R →+ S).inverse g h₁ h₂,    (f : R →* S).inverse g h₁ h₂ with toFun := g }

[Riccardo Brasca]

We tend to use docs#RingEquiv, but it's possible that this literal construction is missing (I am sure we have something really really close).

[Antoine Chambert-Loir]

I don't understand the error message compiler IR check failed at 'RingHom.inverse'._rarg', error: unknown declaration 'RingEquiv.ofBijective' in

import Mathlib.Algebra.Ring.Equiv

def RingHom.inverse' {R S : Type _} [Semiring R] [Semiring S](f : R →+* S)
    (h : Function.Bijective f) : S →+* R :=
    RingEquiv.toRingHom (RingEquiv.ofBijective f h).symm

[Antoine Chambert-Loir]

(For comparison, there are docs#MulEquiv and docs#MulHom.inverse, as well as docs#MonoidHom.inverse.)

[Riccardo Brasca]

This

import Mathlib.Algebra.Ring.Equiv

noncomputable
def RingHom.inverse' {R S : Type _} [Semiring R] [Semiring S](f : R →+* S)
    (h : Function.Bijective f) : S →+* R :=
    RingEquiv.toRingHom (RingEquiv.ofBijective f h).symm

works

[Antoine Chambert-Loir]

Thanks! I was just writing that I appreciated that docs#MonoidHom.inverse didn't have to be tagged with noncomputable…

[Eric Wieser]

I think RingHom.inverse is a fine definition and we should add it

[Antoine Chambert-Loir]

Do you understand the error message?

[Riccardo Brasca]

If we have for other structures I don't see any reason to not having it also for RingEquiv.

[Riccardo Brasca]

docs#RingEquiv.ofBijective is noncomputable, so everything that depends on it should also be tagged noncomputable? But I am not sure.

[Eric Wieser]

Note we also have docs#NonUnitalAlgHom.inverse

[Eric Wieser]

Antoine Chambert-Loir said:

Do you understand the error message?

What error message?

[Riccardo Brasca]

Indeed docs#MonoidHom.inverse is done by hand.

[Eric Wieser]

Riccardo Brasca said:

If we have for other structures I don't see any reason to not having it also for RingEquiv.

I think it's somewhat less compelling for the equivs; you can always build it yourself from RingEquiv.ofRingHom and RingHom.inverse

[Eric Wieser]

I think it should be called RingEquiv.ofRingHom' or something if we do have it; RingEquiv.inverse would be confusing

[Riccardo Brasca]

@Antoine Chambert-Loir I think that the difference is in between having h : Function.Bijective f and (h₁ : Function.LeftInverse g ↑f) (h₂ : Function.RightInverse g ↑f). In the first case you have a bijective function and you cannot produce (in a computable way) an inverse (I believe). In the second case you have the inverse and you can compute with it.

[Riccardo Brasca]

The point is that docs#Function.Bijective means injective and surjective, there is no inverse bundled in the definition.

[Eric Rodriguez]

Eric Wieser said:

Antoine Chambert-Loir said:

Do you understand the error message?

What error message?

Antoine Chambert-Loir said:

I don't understand the error message compiler IR check failed at 'RingHom.inverse'._rarg', error: unknown declaration 'RingEquiv.ofBijective' in

import Mathlib.Algebra.Ring.Equiv

def RingHom.inverse' {R S : Type _} [Semiring R] [Semiring S](f : R →+* S)
    (h : Function.Bijective f) : S →+* R :=
    RingEquiv.toRingHom (RingEquiv.ofBijective f h).symm

[María Inés de Frutos Fernández]

I got a similar error the other day, which was also fixed by adding noncomputable (and I was also very confused with the error message).

[Eric Wieser]

Yes, that error just means "add noncomputable", but in this case the better solution is to make it computable since otherwise the def is mostly pointless

[María Inés de Frutos Fernández]

Right, I agree with making this definition computable in this case, but would it be possible to change the error message in general?

[Antoine Chambert-Loir]

I made a short PR : #5997

[Eric Wieser]

@María Inés de Frutos Fernández, you should request that in a different thread in #lean4, with a #mwe

[Kevin Buzzard]

I was very confused why the inverse of a computable bijection might not be computable but Mario explained the issue to me in 2019 and I wrote a blog post about it.

[Alex J. Best]

María Inés de Frutos Fernández said:

Right, I agree with making this definition computable in this case, but would it be possible to change the error message in general?

I think this error message is not really intentional, and really a result of the work on the new compiler (which I'm not sure the status of right now), I think it will go away eventually in the future and be replaced by something more understandable when the new compler is done.