RingHomClass.toRingHom vs RingEquiv.toRingHom

Stream: mathlib4

[Nailin Guan]

In which cases we prefer RingHomClass.toRingHom over RingEquiv.toRingHom in which cases the converse?
I found most semi-linear equiv use the former one. However, when synethizing instance about Functor.IsEquivalence, I found ModuleCat.restrictScalars_isEquivalence_of_ringEquiv using RingEquiv.toRingHom. So I am a bit confused.

[Anne Baanen]

I think RingEquiv.toRingHom is preferred, since it allows for better simplification.

[Junyan Xu]

I think we are getting rid of RingEquiv.toRingHom (or maybe make it an abbrev of RingHomClass.toRingHom for dot notation), see #mathlib4 > should one explicit coercions? @ 💬.

[Nailin Guan]

However as in semi linear equiv, RingHomClass.toRingHom is used every where. This is the confusing part.

[Christian Merten]

Junyan Xu said:

I think we are getting rid of RingEquiv.toRingHom (or maybe make it an abbrev of RingHomClass.toRingHom for dot notation), see #mathlib4 > should one explicit coercions? @ 💬.

No, RingEquiv.toRingHom will stay and RingHomClass.toRingHom e will simplify to RingEquiv.toRingHom e.

[Junyan Xu]

What's the benefit of having two ways of spelling the same thing other than enabling dot notation?

[Andrew Yang]

The point is we are getting rid of RingHomClass.toRingHom eventually so there will only be one way in the end. See #mathlib4 > Mathlib's morphism hierarchy

[Junyan Xu]

If you get rid of RingHomClass.toRingHom and you also want docs#RingHom.ker to take RingHom rather than RingHomClass, then how do you apply RingHom.ker to an AlgEquiv? (You can still apply it to AlgHom since it extends RingHom so we can't get rid of AlgHom.toRingHom.)

[Anne Baanen]

My idea was (but not sure if this ended up in the consensus) that RingEquiv.toRingHom and AlgEquiv.toRingEquiv will become the new coercions, so we'd write RingHom.ker (↑e).

[Junyan Xu]

If e : AlgEquiv R A B then e.toAlgHom.toRingHom and e.toRingEquiv.toRingHom form a non-reducibly-defeq diamond:

import Mathlib
variable (R A B : Type*) [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B]
example (e : A ≃ₐ[R] B) : e.toAlgHom.toRingHom = e.toRingEquiv.toRingHom := by
  with_reducible rfl -- fails

so I think it's better to use RingHomClass.toRingHom as the normal form (we can provide lemma to rewrite it to both sides of the diamond). @Jireh Loreaux doesn't like FooHomClass.toFooHom being coercions, but I think it's fine.

[Andrew Yang]

Have you read Jireh's post? In particular this section

Another issue is that we (and I have certainly been guilty of this before I saw the light) have implemented definitions which take a term of a morphism class (rather than a morphism itself) as a parameter. At first, this seems appealing, but the problem is that doing doesn't really create a single definition, but in some sense it is a definition schema, with one new definition for each instance of the morphism class. For example, since docs#AlgHom is an instance of docs#RingHomClass, and since docs#RingHom.ker takes a term of a RingHomClass as an argument, if f : A →ₐ[R] B is an algebra homomorphism we have both RingHom.ker f and RingHom.ker (↑f : A →+* B), and these are not trivially equal. Thus we would need additional API to go between them. So, we should restrict definitions to explicit morphisms, instead of morphism classes in order to avoid proliferating definitions.

[Nailin Guan]

So, how about this : I add a version RingHomInvPair e.toRingHom e.symm.toRingHom and refactor as much as I can foresee? Is this the correct way? (I am dealing with these kind of stuffs.)

[Junyan Xu]

I read the post and I think this "another issue" you quoted is more important, and the previous issue is less. Namely, I agree RingHom.ker should take a RingHom but I don't care whether it's RingHom.ker (↑f) or RingHom.ker (.ofClass f).
I also think it would be nice to write f.toRingHom.ker, but it would be ideal that f.toRingHom is reducibly defeq to RingHom.ofClass f (currently called RingHomClass.toRingHom f). Unfortunately for the projections generated by extends (like AlgHom.toRingHom) we cannot achieve this.

[Jireh Loreaux]

Junyan Xu said:

Namely, I agree RingHom.ker should take a RingHom but I don't care whether it's RingHom.ker (↑f) or RingHom.ker (.ofClass f).

Right, the biggest issue I think is definitions parameterized over hom classes, which is exacerbated by the .ofClass constructors being coercions.

If f is a term of a fixed morphism type, I think it might be okay to use .ofClass f to get down to a lower morphism type. Just be prepared that there may not be many lemmas available for it. Although myself I would probably opt for AlgEquiv.toRingEquiv.toRingHom, diamond notwithstanding.