Representation morphisms and `erw`

Stream: mathlib4

[Amelia Livingston]

There are a number of erws in the files Mathlib.RepresentationTheory.Rep and Mathlib.RepresentationTheory.GroupCohomology.Resolution - for instance, when defining morphisms of Reps (the category-theoretic, bundled definition of group representations). I'm going to extend these files in some PRs soon and didn't like how little simp was helping me/how many erws I was using.
So instead I added a definition of morphisms of unbundled, non-category-theoretic Representations:

@[ext]
structure Hom {k G V W : Type*} [CommSemiring k] [Monoid G]
    [AddCommMonoid V] [AddCommMonoid W] [Module k V] [Module k W]
    (ρ : Representation k G V) (τ : Representation k G W) where
    hom : V →ₗ[k] W
    comm : ∀ g, hom ∘ₗ ρ g = τ g ∘ₗ hom

and just worked with Representations instead; simp was very helpful and I didn't have to erw anything. Then given a Representation morphism defined using the above, the corresponding morphism of Reps is 1 line.

However, this approach seems like a bit of a shame. Getting things for free from the category theory framework is cool; it would be nice to just useReps, and actually work out why I'm having to erw things - although I have tried.

So how would people feel about me adding the unbundled definition Representation.Hom?

[Yaël Dillies]

It doesn't shock me that it would be necessary

[Kim Morrison]

Yes, I think it's sad, but please don't let this obstruct you forever. The unbundled definition is fine.

That said, if anyone is interested in investigating erws in the category theory library, I suspect there are still better solutions.

It would be great to have an erw? tool, which would print info messages explaining which subterms obstructued just using rw. I think this is not impossible for anyone who has previously read the code of kabstract (or would like to learn how the internal of rw operate!)

[Kim Morrison]

Nearly always the problem is that we have dsimp lemmas that operate in the implicit arguments of some category theoretic statement (e.g. modifying the objects in a composition), that then cause lemmas to not match syntactically and cause rw to fail.

Understanding exactly what is going wrong in specific cases would hopefully make it possible to either remove the unhelpful dsimp lemmas, or restate the theorems so their implicit arguments match what will be seen "in the wild" after a dsimp in a proof.

[Amelia Livingston]

Thank you very much! There are some erws that this approach won't affect, so I might try messing around with the dsimp lemmas in any case.