Morphisms in FullSubcategory

Stream: mathlib4

[Yaël Dillies]

In the context of the Toric project, we need to work with the essential image of a functor F : C ⥤ D. The essential image docs#CategoryTheory.Functor.essImage is defined using docs#CategoryTheory.FullSubcategory.

[Yaël Dillies]

Here's the catch: For X Y : FullSubcategory P, the homset X ⟶ Y is defeq to the homset X.1 ⟶ Y.1 in the original category. Furthermore, there is no "identity" equivalence (X ⟶ Y) ≃ (X.1 ⟶ Y.1) that we can insert to unconfuse automation.

[Yaël Dillies]

This is causing me immense trouble when dealing with the essential image, eg

• I have given up on a subgoal of Toric here
• In #23480, @Joël Riou's suggestion was much harder to implement than it should have

[Yaël Dillies]

TLDR: Should we break the defeq between X ⟶ Y and X.1 ⟶ Y.1 when X Y : FullSubcategory P?

[Markus Himmel]

Yes, induced categories should be redefined to use a one-field structure for morphisms. Both Joël Riou and I tried this at some point (cf. the discussion here) but didn't finish for various reasons, most recently because we didn't want to interfere with Anne's concrete category refactor. Anne's work is complete, so now would be a good time to try again. This is on my TODO list and I will get to it eventually but of course I'd be very happy if someone else does it. Based on the experience at branch#induced-struct, it shouldn't be too hard to finish the refactor.