English
Let W, X, Y, Z be objects in a category with binary biproducts W ⊞ X and Y ⊞ Z. For any morphisms f: W → Y and g: X → Z, the biprod.map f g composed with the first projection equals the first projection composed with f: biprod.map f g ≫ biprod.fst = biprod.fst ≫ f.
Русский
Пусть X, Y, Z, W являются объектами в категории с бинарными би-образами W ⊞ X и Y ⊞ Z. Для любых отображений f: W → Y и g: X → Z, композиция biprod.map f g с проекцией fst равна композиции fst с f: biprod.map f g ≫ biprod.fst = biprod.fst ≫ f.
LaTeX
$$$\mathrm{biprod.map} \ f\ g \;\;≫\; \mathrm{biprod.fst} = \mathrm{biprod.fst} \;\;≫\; f$$$
Lean4
@[reassoc (attr := simp)]
theorem map_fst {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) :
biprod.map f g ≫ biprod.fst = biprod.fst ≫ f :=
IsLimit.map_π _ _ _ (⟨WalkingPair.left⟩ : Discrete WalkingPair)
