cokernel_π_comp_cokernelToAbelianCoimage

English

The cokernel projection composed with cokernelToAbelianCoimage equals the coimage projection of g.

Русский

Проекция коканалa, композиция с cokernelToAbelianCoimage, равна проекции кообраза g.

LaTeX

$$$$ \\operatorname{cokernel.\\pi}(f) \\circ S.cokernelToAbelianCoimage = \\operatorname{Abelian.coimage.\\pi}(g). $$$$

Lean4

@[reassoc (attr := simp)]
theorem cokernel_π_comp_cokernelToAbelianCoimage :
    cokernel.π S.f ≫ S.cokernelToAbelianCoimage = Abelian.coimage.π S.g :=
  cokernel.π_desc _ _ _

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