kernelSubobjectMap_arrow — Mathlib

English

For sq between f and f' and sq' between f' and f'', the kernelSubobjectMap respects composition: kernelSubobjectMap ((CategoryTheory.instCategoryArrow C).comp sq sq') = kernelSubobjectMap sq ≫ kernelSubobjectMap sq'.

Русский

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

LaTeX

$$$$ kernelSubobjectMap ((CategoryTheory.instCategoryArrow C).comp \\; sq \\; sq') = kernelSubobjectMap\\; sq \\; \\gg kernelSubobjectMap\\; sq' $$$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem kernelSubobjectMap_arrow (sq : Arrow.mk f ⟶ Arrow.mk f') :
    kernelSubobjectMap sq ≫ (kernelSubobject f').arrow = (kernelSubobject f).arrow ≫ sq.left := by
  simp [kernelSubobjectMap]

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