English
For objects A,B,X,Y in a category with colimits of shape Discrete WalkingPair, the diagram map_swap expresses a commutation relation among the maps coprod.map (id X) f, coprod.map g (id B), coprod.map g (id A), coprod.map (id Y) f; i.e., these two composites are equal.
Русский
Для объектов A,B,X,Y в категории с колимитами формы Discrete WalkingPair диаграмма map_swap задаёт равенство двух составов из coprod.map: один — через id X, f и id B; другой — через g и id A, затем через id Y, f.
LaTeX
$$$\mathrm{coprod.map}(\mathbf{1}_X, f) \;\circ\; \mathrm{coprod.map}(g, \mathbf{1}_B) = \mathrm{coprod.map}(g, \mathbf{1}_A) \;\circ\; \mathrm{coprod.map}(\mathbf{1}_Y, f).$$$
Lean4
@[reassoc]
theorem map_swap {A B X Y : C} (f : A ⟶ B) (g : X ⟶ Y) [HasColimitsOfShape (Discrete WalkingPair) C] :
coprod.map (𝟙 X) f ≫ coprod.map g (𝟙 B) = coprod.map g (𝟙 A) ≫ coprod.map (𝟙 Y) f := by simp
