AlgEquiv.toFun_eq_coe

Stream: mathlib4

[Antoine Chambert-Loir]

Why did docs3#alg_equiv.to_fun_eq_coe disappear during the port from Mathlib3 to Mathlib4 ?

lemma AlgEquiv.toFun_eq_coe {R : Type u} {A₁ : Type v} {A₂ : Type w}
    [CommSemiring R] [Semiring A₁] [Semiring A₂]  [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂)  :
  e.toFun = e := rfl

It's not that deep, but I found it useful in rewriting, and I did not find any swifter way than reintroducing it.

[Kevin Buzzard]

Probably because it became a syntactic equality in mathlib4 (or someone thought it did) so was no longer necessary? That's the usual reason coercion lemmas like this disappeared.

[Antoine Chambert-Loir]

Is there any objection to restoring it?
The point is that I need to apply map_one after that, but it is inaccessible otherwise.

[Kevin Buzzard]

Coercions work completely differently in mathlib4 to mathlib3. Are you sure that this is not a syntactic equality?

[Kevin Buzzard]

yeah the two sides are displaying differently, maybe this is an error and the lemma shouldn't have been deleted? The linter seems happy.

[Notification Bot]

17 messages were moved from this topic to #mathlib4 > Algebra.TensorProduct.rid as isomorphism over the larger ... by Eric Wieser.

[Eric Wieser]

Aside from the tangent I started (and now moved), we should definitely add back AlgEquiv.toFun_eq_coe