epi_of_comp_epi_of_mono

Stream: Is there code for X?

[Kevin Buzzard]

I'm assuming this is true?

import category_theory.abelian.basic

open category_theory

lemma epi_of_comp_epi_of_mono {V : Type*} [category V] [abelian V]
  {A B C : V} (f : A ⟶ B) (g : B ⟶ C) [epi (f ≫ g)] [mono g] : epi f :=
begin
  sorry
end

I can't see a "low-level" approach (maybe I'm missing something). In my model example of an abelian category, namely abelian groups, the issue is that there exist non-split monics, which stop a nice three-line proof from going through. If you just imagine everything as being concrete, and epi being surjective etc, then it's a simple diagram chase. This makes me think that it might be the sort of thing which is trivial with pseudoelements. @Markus Himmel am I right? I've never used pseudoelements before.

[Adam Topaz]

I think this is called docs#category_theory.epi_of_epi

[Adam Topaz]

Oh no not quite.

[Kevin Buzzard]

I think it's deeper. It might well not be true in general, although abelian is probably overkill.

[Reid Barton]

Using epi_of_epi, g is epi as well as mono, so since you're in a balanced category you can cancel it

[Kevin Buzzard]

Excellent, thanks!

[Adam Topaz]

(We have docs#category_theory.is_iso_of_mono_of_epi for that last step)

[Kevin Buzzard]

(and cancelling isos in statements about epis is something I built yesterday)

[Adam Topaz]

no that's not it.

[Adam Topaz]

I'm quite sure we have that in mathlib as well..

[Kevin Buzzard]

(just to be clear, I have a proof of this now which I just pushed to LTE, but it relies on stuff which isn't in mathlib)