English
Let W, X, Y, Z be objects with binary biproducts W ⊞ X and Y ⊞ Z. For f: W → Y and g: X → Z, the map biprod.map f g composed with the second projection equals the second projection composed with g: biprod.map f g ≫ biprod.snd = biprod.snd ≫ g.
Русский
Пусть W, X, Y, Z — объекты с бинарными биобразованиями W ⊞ X и Y ⊞ Z. Для отображений f: W → Y и g: X → Z, композиция biprod.map f g с проекцией snd равна композиции snd с g: biprod.map f g ≫ biprod.snd = biprod.snd ≫ g.
LaTeX
$$$\mathrm{biprod.map} \ f\ g \;\;≫\; \mathrm{biprod.snd} = \mathrm{biprod.snd} \;\;≫\; g$$$
Lean4
@[reassoc (attr := simp)]
theorem map_snd {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) :
biprod.map f g ≫ biprod.snd = biprod.snd ≫ g :=
IsLimit.map_π _ _ _
(⟨WalkingPair.right⟩ : Discrete WalkingPair)
-- Because `biprod.map` is defined in terms of `lim` rather than `colim`,
-- we need to provide additional `simp` lemmas.
