English
The cofork obtained by precomposing a coequalizer cocone with an epimorphism is itself a coequalizer.
Русский
Кофорк, полученный путем предкомпозиции коэквалайзерного кокона эпиморфизмом, является коэквалайзером.
LaTeX
$$$ IsColimit( Cofork.ofπ c.π ( (h ≫ f) ≫ Cofork.π c = (h ≫ g) ≫ Cofork.π c )) $$$
Lean4
/-- The cofork obtained by precomposing a coequalizer cofork with an epimorphism is
a coequalizer. -/
def isCoequalizerEpiComp {c : Cofork f g} (i : IsColimit c) {W : C} (h : W ⟶ X) [hm : Epi h] :
have : (h ≫ f) ≫ Cofork.π c = (h ≫ g) ≫ Cofork.π c :=
by
simp only [Category.assoc]
exact congrArg (h ≫ ·) c.condition
IsColimit (Cofork.ofπ c.π (this) : Cofork (h ≫ f) (h ≫ g)) :=
Cofork.IsColimit.mk' _ fun s =>
let s' : Cofork f g := Cofork.ofπ s.π (by apply hm.left_cancellation; simp_rw [← Category.assoc, s.condition])
let l := Cofork.IsColimit.desc' i s'.π s'.condition
⟨l.1, l.2, fun hm => by apply Cofork.IsColimit.hom_ext i; rw [Cofork.π_ofπ] at hm; rw [hm]; exact l.2.symm⟩
