Simp lemma for `Cofan.inj`

Stream: Is there code for X?

[Christian Merten]

Given (C : Type u) [Category.{v, u} C] (ι : Type w) (f : ι → C) (t : Cofan f) (i : ι), neither me nor simp can find a simp lemma for Cofan.inj t i = t.ι.app ⟨i⟩. Do you have objections to adding this (and the dual of course)? I find myself rewriting this manually quite often, because the general (co)limit machinery only applies for the latter version.

[Joël Riou]

We certainly do not want this as a simp lemma. We may experiment making the definition of Cofan.inj an abbreviation instead of a def: if this does not break too many things, this may be ok. Otherwise, the right way would be to develop more the suitable incarnation of the (co)limits API to the special case of (co)products.

[Adam Topaz]

If anything, there should be a simp lemma going the other way!

[Christian Merten]

Joël Riou said:

We certainly do not want this as a simp lemma. We may experiment making the definition of Cofan.inj an abbreviation instead of a def: if this does not break too many things, this may be ok. Otherwise, the right way would be to develop more the suitable incarnation of the (co)limits API to the special case of (co)products.

May I ask why we don't want this to be a simp lemma?

[Adam Topaz]

As Joel said, the whole point of introducing Cofan as a def is to build an API around it which specializes the API for cocones in this particular case. If you introduce the simp lemma you suggest, that means that whenever you use (d)simp in a proof, that will escape the API that you build around Cofan and Cofan.inj, which is counterproductive!

[Andrew Yang]

Can you give some examples where you need to do such a rewrite? It might be indicating that some API around cofans are missing.

[Christian Merten]

Adam Topaz said:

As Joel said, the whole point of introducing Cofan as a def is to build an API around it which specializes the API for cocones in this particular case. If you introduce the simp lemma you suggest, that means that whenever you use (d)simp in a proof, that will escape the API that you build around Cofan and Cofan.inj, which is counterproductive!

I guess this effect is exactly what I intended, since I felt like the general API around Cocone is more practical. But if extending the API around Cofan is the goal, then I understand why a simp lemma would be counterproductive.

[Christian Merten]

Andrew Yang said:

Can you give some examples where you need to do such a rewrite? It might be indicating that some API around cofans are missing.

Some examples (intermediate helper equalities that I used to show some inclusions in coproducts are monomorphisms):

import Mathlib

open CategoryTheory Limits Functor

example (ι : Type u) (f : ι → Type u) (t : Cofan f) (h : IsColimit t) (i : ι) :
    Cofan.inj t i = Sigma.ι f i ≫ (colimit.isoColimitCocone ⟨t, h⟩).hom := by
  show t.ι.app ⟨i⟩ = Sigma.ι f i ≫ (colimit.isoColimitCocone ⟨t, h⟩).hom
  simp only [Discrete.functor_obj, const_obj_obj, colimit.isoColimitCocone_ι_hom]

example {C : Type u} [Category.{v, u} C] (F : C ⥤ FintypeCat.{w}) {ι : Type} [Fintype ι] {f : ι → C}
    (t : ColimitCocone (Discrete.functor f)) (i : ι) :
    (F.mapCocone t.cocone).ι.app ⟨i⟩ = F.map (Cofan.inj t.cocone i) := by
  show (F.mapCocone t.cocone).ι.app ⟨i⟩ = F.map (t.cocone.ι.app ⟨i⟩)
  simp only [Functor.mapCocone_ι_app]

Dropping the show lines do not work, simp does not make any significant progress then.

[Adam Topaz]

both can be proved with simp ; rfl

[Adam Topaz]

or just aesop_cat for that matter.

[Christian Merten]

Adam Topaz said:

both can be proved with simp ; rfl

Sure, thats what aesop does.

[Christian Merten]

I guess, "simp does not make any significant progess then" is wrong, it does progress, but not as much as I would hope and less if I would just formulate this in terms of t.ι.app ⟨i⟩ instead of Cofan.inj.