CategoryTheory.Limits.Fan.proj

Stream: mathlib4

[Kim Morrison]

I am surprised to see docs#CategoryTheory.Limits.Fan.proj and Cofan.inj are defs rather than abbrevs, as they are introducing a new way to talk about the same thing, and seem like they just increase the API surface area, and block rewriting. Does anyone remember the history here (I fear that I am to blame, long ago...)?

[Johan Commelin]

I think we can just try to make it an abbrev and see what happens?

[Markus Himmel]

I'm not too happy about this. Specifically in the limits parts of the category theory library we have the problem that there are already a lot of abbrevs which mean that in many situations the lemma that you need to apply has a name that is quite different from what you see in the goal. I think this is one of the reasons why the category theory part of mathlib has a reputation of being difficult to learn.

Looking at the data, this problem seems to be confined mostly to the fact that we repeat a lot of the general limits API definition for every special shape (I had thought that there are more examples outside of the special shapes, but it looks like I was wrong). I wish we could find a solution for this. I understand that it's nice to have the specialized API, and I understand that repeating all of the limits lemmas for every special shape is painful, but the current situation of "either simp can solve the goal, or I need to go look what the thing on my screen actually means and then manually look through the general limits API to find the matching lemma which looks completely different from my goal" is also very unsatisfying in my opinion.

In the case of products, I think that there is a good reason to have a "hard" (def) abstraction barrier, namely that we might want users (perhaps especially those who just use category theory while working on results from other fields) to be able to work with products in terms of the indexing type β and not the indexing category Discrete β, and simp and similar automation should make sure that the goal stays in "product land" so that the user does not have to interface with the more general limits library if all they need are the basic properties of products. Moving to "limits land" should be an explicitly user-requested step that changes Fan.proj into Cone.π, j : β into ⟨j⟩ : Discrete β and so on. Right now, in my experience calling simp often leaks these things into goals because simp just apply whatever general limits lemma it can find.

[Kim Morrison]

Sounds even better. :-)

[Joël Riou]

For pullbacks (which are defined as abbrev), it seems that when a lemma like pullback.lift_fst may apply, simp would rather use the more general limit.lift_π, which is moderately annoying. If we were to make a change, introducing more API separation using defs instead of abbrevs could be better. However, another issue is that when we make a definition of a Fan, the simps attribute would generate lemmas involving Cone.π instead of the specialized API Fan.proj...