biprodComparison_fst — Mathlib

English

Let X, Y be objects of C with binary biproducts, and F preserves zero morphisms and preserves biproducts for the pair. Then the first projection is compatible with F in the sense that the mapped fst equals the composition with biprodComparison: F.map biprod.fst = biprodComparison F X Y ≫ biprod.fst.

Русский

Пусть X, Y — объекты C с бинарным би-производством, F сохраняет нулевые морфизмы и сохраняет би-произведение пары. Тогда первая проекция совместима с отображением F: F.map biprod.fst = biprodComparison F X Y ≫ biprod.fst.

LaTeX

$$$F(\\text{biprod.fst}) = \\text{biprodComparison}(F,X,Y) \\circ \\text{biprod.fst}$$$

Lean4

@[reassoc (attr := simp)]
theorem biprodComparison_fst : biprodComparison F X Y ≫ biprod.fst = F.map biprod.fst :=
  biprod.lift_fst _ _

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