RingEquiv.ofHomInv and MonoidHom.toMulEquiv

Stream: Is there code for X?

[Kim Morrison]

We have both src#RingEquiv.ofHomInv and src#MonoidHom.toMulEquiv, seemingly inconsistently named. I was looking for the corresponding fact for linear equivalences, but couldn't find it.

1. Where is the result for linear equivalences?
2. Shall we add RingHom.toRingEquiv and/or MulEquiv.ofHomInv (if they don't already exist in hiding)?
3. Shall we deprecate either of the existing functions in favour of anything added in 2?

[Richard Copley]

1. docs#LinearEquiv.ofLeftInverse ? docs#LinearEquiv.ofInjective ?

[Richard Copley]

Richard Copley said:

1. docs#LinearEquiv.ofLeftInverse ? docs#LinearEquiv.ofInjective ?

Nope. docs#LinearEquiv.ofLinear

[Kim Morrison]

Thanks, that's the one. What an interesting variety of names! :-)

[Kim Morrison]

To make matters more fun, LinearEquiv.ofLinear takes its 3rd and 4th arguments in the opposite order than RingHom.ofHomInv and MonoidHom.toMulEquiv.

[Richard Copley]

I seem to recall ofLinear being hard to find, and it's clear that I found it hard to remember. What say ofInverse for everything, with the arguments always in the same order? (I'd say "it has a left inverse" first, "it has a right inverse" second, so the same as RingHom.ofHomInv and MonoidHom.toMulEquiv and the opposite of LinearEquiv.ofInverse.)

[Kim Morrison]

How about:

• XEquiv.ofInverse for each X
• aliased as XHom.toXEquiv as well?

[Yaël Dillies]

I think the name should contain both XEquiv and XHom.

[Eric Wieser]

I don't think we need it in the XHom namespace now that dot constructor notation is a thing, though I guess alias is harmless enough

[Eric Wieser]

(does alias on definitions make the alias reducible? If not, then we should pretty much never use it)

[Kim Morrison]

Yaël Dillies said:

I think the name should contain both XEquiv and XHom.

So XEquiv.ofXHom or XEquiv.ofXHomInverse?

[Yaël Dillies]

I think the Inverse doesn't add anything. It might even hinder comprehension since the entire point of the constructor is that you are not providing an inverse!

[Eric Wieser]

I thought the entire point of the constructor was that you get to use nice ext lemmas to prove the maps compose to the identity

[Eric Wieser]

We're taking about XEquiv.ofXHom someXHom invXHom h1 h2, right?

[Yaël Dillies]

Ghu yes you're right and indeed the Inverse belongs there to disambiguate it from the other constructor I had in mind.

[Eric Wieser]

Which one were you thinking of?

[Yaël Dillies]

The one which takes in a bijective hom

[Eric Wieser]

That's ofBijective

[Kim Morrison]

Okay, XEquiv.ofXHomInverse!

[Richard Copley]

RingEquiv.ofRingHomInverse, MulEquiv.ofMonoidHomInverse, LinearEquiv.ofLinearMapInverse

• One of these things is not like the others
• That aside, does the XHom add anything?

[Kim Morrison]

I would be happy to drop the XHom.

[Richard Copley]

Oh. What I was getting at is that MonoidHom.toMulEquiv doesn't actually use map_one', and I assumed the below would go through. But it doesn't. It would be unfortunate to have MulEquiv.ofInverse that takes a MonoidHom and not a MulHom, so maybe that's an argument for keeping the XHom. Or just for keeping it when the Xs aren't the same in the XHom and XEquiv parts?

import Mathlib.Algebra.Group.Equiv.Basic

def MulEquiv.ofMulHomInverse {M N} [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ* M)
    (h₁ : g.comp f = MulHom.id _) (h₂ : f.comp g = MulHom.id _) : M ≃* N where
  toFun := f
  invFun := g
  left_inv := DFunLike.congr_fun h₁
  right_inv := DFunLike.congr_fun h₂
  map_mul' := f.map_mul

example {M N} [MulOneClass M] [MulOneClass N] (f : M →* N) (g : N →* M)
    (h₁ : g.comp f = MonoidHom.id _) (h₂ : f.comp g = MonoidHom.id _) : M ≃* N :=
  MulEquiv.ofMulHomInverse f.toMulHom g.toMulHom h₁ h₂
--                                        ~~
-- application type mismatch
--   MulEquiv.ofMulHomInverse (↑f) (↑g) h₁
-- argument
--   h₁
-- has type
--   MonoidHom.comp g f = MonoidHom.id M : Prop
-- but is expected to have type
--   MulHom.comp ↑g ↑f = MulHom.id M : Prop

[Yaël Dillies]

The point of the XHom is for you to discover the function when you type XHom in the docs