fac — Mathlib

English

The coimage projection composed with the Abelian factor through coimage equals f; i.e., coimage.π f ≫ Abelian.factorThruCoimage f = f.

Русский

Проекция кообраза в композиции с через кообразовую факторизацию равна f; то есть coimage.π f ≫ Abelian.factorThruCoimage f = f.

LaTeX

$$$\mathrm{coimage.\pi}(f) \circ \mathrm{Abelian.factorThruCoimage}(f) = f$$$

Lean4

/-- `f` factors through its coimage via the canonical morphism `p`. -/
protected theorem fac : coimage.π f ≫ Abelian.factorThruCoimage f = f :=
  cokernel.π_desc _ _ _

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