map_id_left_eq_curry_map — Mathlib

English

For F : J × K ⥤ C, the map of the left component at j matches the map of the curry of F at j after applying the map on f.

Русский

Для F : J × K ⥤ C отображение левого компонента при фиксированном j совпадает с отображением карри (F) при том же j.

LaTeX

$$F.map (𝟙 j ×ₘ f) = ((curry.obj F).obj j).map f$$

Lean4

theorem map_id_left_eq_curry_map {j : J} {k k' : K} {f : k ⟶ k'} : F.map (𝟙 j ×ₘ f) = ((curry.obj F).obj j).map f :=
  rfl

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