factorThruImageSubobject_comp_imageToKernel

English

The composite from the image subobject through imageToKernel equals the kernel subobject factorization: factorThroughImageSubobject f ≫ imageToKernel f g w = factorThroughKernelSubobject g f w.

Русский

Состав через образ и imageToKernel равен факторизации через ядро: факторThroughImageSubobject f ≫ imageToKernel f g w = factorThroughKernelSubobject g f w.

LaTeX

$$$\text{factorThruImageSubobject}(f) \;\circ\; \text{imageToKernel}(f,g,w) = \text{factorThruKernelSubobject}(g,f,w)$$$

Lean4

theorem factorThruImageSubobject_comp_imageToKernel (w : f ≫ g = 0) :
    factorThruImageSubobject f ≫ imageToKernel f g w = factorThruKernelSubobject g f w :=
  by
  ext
  simp

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