map_swap — Mathlib

English

In a suitable setting with limits over a discrete WalkingPair, the following swap identity holds: prod.map (id_X) f ≫ prod.map g (id_B) = prod.map g (id_A) ≫ prod.map (id_Y) f.

Русский

В условиях с предельными объектами по дискретному WalkingPair выполняется тождество обмена: prod.map(id_X) f ≫ prod.map g (id_B) = prod.map g (id_A) ≫ prod.map (id_Y) f.

LaTeX

$$$prod.map(id_X)\\, f \\;\\\\circ \\\\prod.map g (id_B) = prod.map g (id_A) \\\\circ prod.map (id_Y) f$$$

Lean4

@[reassoc]
theorem map_swap {A B X Y : C} (f : A ⟶ B) (g : X ⟶ Y) [HasLimitsOfShape (Discrete WalkingPair) C] :
    prod.map (𝟙 X) f ≫ prod.map g (𝟙 B) = prod.map g (𝟙 A) ≫ prod.map (𝟙 Y) f := by simp

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