should one explicit coercions?

Stream: mathlib4

[Antoine Chambert-Loir]

In many cases, mathlib has a coercion function that applies whenever needed (and appropriately detected).

Example in algebra : a docs#RingEquiv f : M ≃+* N has an associated docs#RingHom, f.toRingHom, but it can also be obtained by coercion, as (f : M →+* N) and is indicated by an uparrow ↑f.

Is there a preferred form?

Indeed, this sometimes brings the necessity to have two theorems, one where the coercion is applied, and one with the explicit original function. Maybe this reflects a lack of a simp lemma that would prefer one form to the other.

[Junyan Xu]

I think we're getting rid of the coercions in favor of explicit invocation of .ofClass, see #mathlib4 > Mathlib's morphism hierarchy @ 💬. I think we should probably also get rid of RingEquiv.toRingHom etc. It's been observed before that docs#LinearEquiv.toLinearMap isn't reducibly defeq to the coercion and it caused problems, for example.

[Christian Merten]

No, the plan is to get rid of the coercions and make RingEquiv.toRingHom the simp NF. The .ofClass constructors should only be used in general lemmas about FooHomClass.

[Junyan Xu]

Are you sure? We certainly won't be able to get rid of structure projections, but RingEquiv.toRingHom is not one; if we want to keep it I think we should make it an abbrev of .ofClass, and the same applies to LinearEquiv.toLinearMap.

[Riccardo Brasca]

I think that the coercions we want to get rid of are those from to FooHomClass to FooHom, not those from FooHom to BarHom.

[Junyan Xu]

The coercions from FooHom to BarHom are given by the BarHomClass FooHom instances, no? Structure projections (from extends) like docs#RingHom.toAddMonoidHom or manually defined RingEquiv.toRingHom/LinearEquiv.toLinearMap are not coercions.

[Junyan Xu]

Oh, I finally remembered what is particularly egregious about the LinearEquiv/LinearMap coercion: there's a manually defined LinearEquiv.instCoeLinearMap which is not reducibly defeq to the coercion from LinearEquiv being LinearMapClass ...

[Riccardo Brasca]

Let me ping @Jireh Loreaux that surely know what is the plan

[Yaël Dillies]

Indeed the plan is to get rid of the generic (ie the ones that trigger in the presence of a hom class instance) coercions and add the specific (ie between two concrete types) coercions

[Yaël Dillies]

Once that is done, Antoine's original problem is no more: the coercion will syntactically be the same as .toRingHom

[Antoine Chambert-Loir]

That was one of the coercions I had in mind, the other one is related to quotients, I rapidly fell onto equalities such as ⟦x⟧ = ↑x where rfl showed they coincided but rw? found nothing.

[Yaël Dillies]

That's a completely separate refactor which @Yuyang Zhao was doing