kernelSubobjectMap_comp — Mathlib

English

The composition of kernelSubobjectMap with another kernelSubobjectMap corresponds to the composition of arrows in the source category.

Русский

Композиция kernelSubobjectMap соответствует композиции стрел в исходной категории.

LaTeX

$$$$ kernelSubobjectMap ((CategoryTheory.instCategoryArrow C).comp sq sq') = kernelSubobjectMap sq ≫ kernelSubobjectMap sq' $$$$

Lean4

@[simp]
theorem kernelSubobjectMap_comp {X'' Y'' : C} {f'' : X'' ⟶ Y''} [HasKernel f''] (sq : Arrow.mk f ⟶ Arrow.mk f')
    (sq' : Arrow.mk f' ⟶ Arrow.mk f'') :
    kernelSubobjectMap (sq ≫ sq') = kernelSubobjectMap sq ≫ kernelSubobjectMap sq' := by cat_disch

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