isCokernelEpiComp_desc — Mathlib

English

Given two cokernel coforks over f and g, and an isomorphism between kernels, the projection π for f is isomorphic to the projection π for g via the isomorphism.

Русский

Даны два коканаловых когорка над f и g и изоморфизм между их ядрами; проекция π над f изоморфна π над g через этот изоморфизм.

LaTeX

$$$\forall f,g, IsIso(ker(f)\to X) \Rightarrow \text{(равенства проекций через изоморфизм})$$$

Lean4

@[simp]
theorem isCokernelEpiComp_desc {c : CokernelCofork f} (i : IsColimit c) {W} (g : W ⟶ X) [hg : Epi g] {h : W ⟶ Y}
    (hh : h = g ≫ f) (s : CokernelCofork h) :
    (isCokernelEpiComp i g hh).desc s =
      i.desc
        (Cofork.ofπ s.π
          (by
            rw [← cancel_epi g, ← Category.assoc, ← hh]
            simp)) :=
  rfl

Похожие утверждения