English
Another formulation that biprod.map equals biprod.map'.
Русский
Ещё одно формулирование того, что biprod.map совпадает с biprod.map'.
LaTeX
$$$ \operatorname{biprod.map} f g = \operatorname{biprod.map}' f g $$$
Lean4
theorem map_eq_map' {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) :
biprod.map f g = biprod.map' f g := by
ext
· simp only [mapPair_left, IsColimit.ι_map, IsLimit.map_π, Category.assoc, ← BinaryBicone.toCone_π_app_left,
← BinaryBicone.toCocone_ι_app_left]
simp
· simp only [mapPair_left, IsColimit.ι_map, IsLimit.map_π, Category.assoc, ← BinaryBicone.toCone_π_app_right,
← BinaryBicone.toCocone_ι_app_left]
simp
· simp only [mapPair_right, IsColimit.ι_map, IsLimit.map_π, Category.assoc, ← BinaryBicone.toCone_π_app_left,
← BinaryBicone.toCocone_ι_app_right]
simp
· simp only [mapPair_right, IsColimit.ι_map, IsLimit.map_π, Category.assoc, ← BinaryBicone.toCone_π_app_right,
← BinaryBicone.toCocone_ι_app_right]
simp
