Naturality lemmas for natural transforms of compositions

Stream: mathlib4

[Robin Carlier]

A pattern that occurs several times in the category theory library is that one has several functors, say T : C₁ ⥤ C₂, L : C₁ ⥤ C₃, R : C₂ ⥤ C₄, B : C₃ ⥤ C₄, and a natural transformation α : T ⋙ R → L ⋙ B (this is the litteral definition of a TwoSquare). Then within a proof, a simp call gets stuck on R.map (T.map f) ≫ α.app Y, and can’t proceed further. Then what one usually does is a variation of the following pattern

  have := α.naturality
  dsimp at this
  simp [this]

to put this in a #mwe: the following example can’t be closed by a single simp call.

import Mathlib
open CategoryTheory
variable {C₁ C₂ C₃ C₄ : Type*}
  [Category C₁] [Category C₂] [Category C₃] [Category C₄]
  (T : C₁ ⥤ C₂) (L : C₁ ⥤ C₃) (R : C₂ ⥤ C₄) (B : C₃ ⥤ C₄)

example (α : T ⋙ R ⟶ L ⋙ B) ⦃X Y : C₁⦄ (f : X ⟶ Y) :
    R.map (T.map f) ≫ α.app Y = α.app X ≫ B.map (L.map f) := by
  have := α.naturality
  dsimp at this
  simp [this]

Sure enough, other tactics, like aesop close this goal, and I’m sure grind will (and in this specific example, an exact α.naturality also of course works), but when it shows up in more complex proofs not directly closed by these hammers, or if one wants to precisely rewrite, or use them in reverse direction, we’re out of luck and have to add a have anyway.

This pattern occurs not only for two-squares, but for basically every natural transform that involves a composition of functors, or an identity functor. This is why e.g there are extra simp lemmas docs#CategoryTheory.Adjunction.counit_naturality that records the "dsimped forms" of naturality directly, I know I introduced some to get around some erws.

To ease automation, should we add some ([reassoc]and possibly simp) lemmas that restate the "dsimped" forms of general natural transformations of say, shape T ⋙ R ⟶ L ⋙ B, _ ⟶ F ⋙ G, G ⋙ F ⟶ _, F ⟶ 𝟭 C₂ and 1 C₁ ⟶ _ and _ ⟶ 𝟭 C₁ (the last four might need extra overlap)?
This is admittedly a rather "bruteforce" solution, but it seems to cover most of the use cases I could notice.

[Jovan Gerbscheid]

It could make sense to have an option in simp for simplifying the lemmas that you pass to it. So then simp [α.naturality] should be able to prove this goal.

[Jovan Gerbscheid]

Also, please follow the #mwe rules in the future to make it easier to run the minimal example

[Robin Carlier]

I thought about a simproc, but then we wouldn't be able to use it in rw, right?
Also, Sorry for the mwe, I forgot the imports and the universe variables... I'll update it.

[Jovan Gerbscheid]

Actually, what about an elaborator? Something like simp%, and then if I write simp% α.naturality, it elaborates to a proof of ∀ ⦃X Y : C₁⦄ (f : X ⟶ Y), R.map (T.map f) ≫ α.app Y = α.app X ≫ B.map (L.map f)

[Jovan Gerbscheid]

That would work in simp, but is also useful in rw.

[Jovan Gerbscheid]

I guess for maintainability reasons, the dsimp% version would be preferred, but that is enough for your example.

[Robin Carlier]

It would be nice (and similar to the very nice reassoc_of% elaborator), but won't something as radical simp% be a "hidden non-terminal simp"?

[Jovan Gerbscheid]

Yes exactly, that's what I meant with my last message. I think simp% and dsimp% would both be very nice, but simp% would count as a hidden non-terminal simp.

[Robin Carlier]

Arguably, you'd want something a little more advanced than just a dsimp% in cases involving identities, since you might want to simplify identities using Category.comp_id or Category.id_comp
Maybe a cat_normalize% that is a simp only [..] under the hood, where [...] is a curated category theory simp set?

[Jovan Gerbscheid]

That sounds like a good idea