simp projection `_Hom` for categories

Stream: mathlib4

[Calle Sönne]

When defining a category (or a Quiver), often the Hom field is already defined as some other type Foo.Hom X Y. Tagging the definition of the category with @[simps] then adds a simp lemma of type:

∀ (X Y : C), (X ⟶ Y) = Foo.Hom X Y

I think I don't quite understand how the fields of structures work, will Quiver.Hom X Y (i.e. X ⟶ Y) not be an abbrev for Foo.Hom X Y anyways? So is it a good idea to be adding this simp lemma (and does it matter)?

What makes me confused is that it seems to me that if simp sees this type, and simplifies it to Foo.Hom X Y, then we are forgetting that the morphisms are actually a part of a category, so simp can no longer use various category-theory lemmas. It seems better that one should apply some sort of ext lemma to reduce to working with Foo.Hom X Y (or rather its projections) when one needs to use the actual underlying implementation of Foo.Hom.

Another small annoyance with @[simps] for categories that is slightly related, is that the simp lemmas that get added (e.g. comp_hom lets say, if Foo.Hom has a projection hom) will have the form

{X Y Z : C} (f : Foo.Hom X Y) (g : Foo.Hom Y Z) : (u ≫ v).hom = u.hom ≫ v.hom

but it would be more visually appealing if (f : Foo.Hom X Y) was (f : X ⟶ Y).

[Joël Riou]

Usually, when morphisms are a structure Hom, we add a lemma hom_ext which is definitionally the same as Hom.ext but it takes inputs in X ⟶ Y instead of Hom X Y. Similarly, we have to restate id_hom and comp_hom.

[Calle Sönne]

Do we have to restate id_hom and comp_hom? In some testing I did locally where Hom was a 1-field structure, the simp lemmas with Foo.Hom X Y as parameters still seems to apply when the morphisms had type X ⟶ Y (also without adding the _Hom simp lemma).

[Calle Sönne]

So the restated versions were already provable by simp

[Calle Sönne]

And having to restate them would be very annoying for bicategories, where if Hom and the 2-Homs are structures, then you suddenly have to restate 12 lemmas or even more sometimes.

[Joël Riou]

Ah, if you do @[simps id comp], it may work.

[Calle Sönne]

In my tests it seems to work in both cases

[Calle Sönne]

I think maybe my question was not very well stated, it is basically this:
Should the _Hom lemma generated by @[simps] be excluded most of the time (at least when Hom is a structure), in favor of a manually added ext lemma?

[Joël Riou]

In general, I do not think we should generate _Hom lemmas.

[Calle Sönne]

Thanks! I wonder if it is a good idea to remove this simps projection somehow, whilst still allowing simps to still access the projections of Hom. So that one would not have to manually exclude _Hom everywhere, which is especially painful for bicategories where one has to list the other ~12 simp lemmas that should be included. I don't know if this is possible already, maybe some metaprogramming needs to be done for this.

[Joël Riou]

Yes, we could add a initialize_simps_projections.

[Calle Sönne]

To remove the _Hom you mean? I'm worried that this will make the projections of Hom that we care about invisible to simps.

[Joël Riou]

I do not think there are many projection of Hom we need. It can be activated if we care. I only suggest changing the default behaviour.

[Calle Sönne]

Thanks for the help, then I will try removing it in a branch to see what happens.