Explicit cokernel

Stream: condensed mathematics

[Riccardo Brasca]

In for_mathlib/SemiNormedGroup we have

noncomputable def coker.map {fab : A ⟶ B} {fbd : B ⟶ D} {fac : A ⟶ C} {fcd : C ⟶ D}
  (h : fab ≫ fbd = fac ≫ fcd) : explicit_cokernel fab ⟶ explicit_cokernel fcd :=
explicit_cokernel_desc (show fab ≫ fbd ≫ (explicit_cokernel_π _) = 0,
  begin
    rw [← category_theory.category.assoc, h, category_theory.category.assoc,
      comp_explicit_cokernel_π, limits.comp_zero],
  end
  )

This is morally a special case of docs#category_theory.limits.cokernel.map, but not literally, since with normed group we work with explicit_cokernel (that in any case is a cokernel). Does someone see how to prove cokernel.map using docs#category_theory.limits.cokernel.map? Or should we have both results?

[Adam Topaz]

you mean to construct this map using the function from the category theory library?

[Riccardo Brasca]

Yes

[Johan Commelin]

Is there some lemma saying that explicit_cokernel is a colimit for the cokernel diagram?

[Adam Topaz]

yes, one way to do this is to make an explicit cofork using explicit_cokernel, prove that it's a colimit (as Johan said), and use is_colimit.map or something like that.

[Riccardo Brasca]

We already have docs#SemiNormedGroup.explicit_cokernel_iso

[Riccardo Brasca]

So it's probably enough to use it

[Adam Topaz]

Looking at the code for that, we can use is_colimit_cokernel_cocone.

[Adam Topaz]

actually, lines 89-118 of that file are essentially what I was describing above :)

[Adam Topaz]

And the is_colimit.map I mentioned above is actually docs#category_theory.limits.is_colimit.map

[Adam Topaz]

(or you could just use docs#category_theory.limits.is_colimit.desc )

[Adam Topaz]

If you use the explicit cokernel iso you mentioned above and compose with cokernel.map, then I think that will introduce some compositions with identity morphisms under the hood which may (or may not) be annoying if we want to rely on some morphisms being defeq.

[Riccardo Brasca]

That's true... in any case my question is very practical: I want to throw away for_mathlib/SemiNormedGroup, so if there is a one line proof of cokernel.map I will just use it, but otherwise I am happy with the current proof, that is very short anyway, and I will PR it.

[Adam Topaz]

Let me see... one sec.

[Adam Topaz]

noncomputable def coker.map {fab : A ⟶ B} {fbd : B ⟶ D} {fac : A ⟶ C} {fcd : C ⟶ D}
  (h : fab ≫ fbd = fac ≫ fcd) : explicit_cokernel fab ⟶ explicit_cokernel fcd :=
@explicit_cokernel_desc _ _ _ fab (fbd ≫ explicit_cokernel_π _) $ by simp [reassoc_of h]

That's one line ;)

It looks like we need to make explicit some of the variables in explicit_cokernel_desc

[Riccardo Brasca]

Very nice!

[Adam Topaz]

Adam Topaz said:

It looks like we need to make explicit some of the variables in explicit_cokernel_desc

explicit_cokernel_desc should have variables similar to docs#category_theory.limits.cokernel.desc -- If I have time later today, I will try to make a mathlib PR with a fix.

[Riccardo Brasca]

I just opened #9712 to have explicit_cokernel.map and explicit_coker.map_desc. Even with your one line proof they seem useful to have.