uncurry_obj_curry_obj_flip_flip' — Mathlib

English

A variant identity: uncurry.obj (F1 ⋙ (F2 ⋙ (curry.obj G).flip).flip) = (F1.prod F2) ⋙ G.

Русский

Вариант идентичности: раскурривание F1 и F2 через каррирование и двойной flip дает композицию, равную произведению F1 и F2 примененную к G.

LaTeX

$$$\operatorname{uncurry.obj} (F_1 \cdot (F_2 \cdot (\operatorname{curry.obj} G).flip).\text{flip}) = (F_1 \prod F_2) \cdot G$$$

Lean4

theorem uncurry_obj_curry_obj_flip_flip' (F₁ : B ⥤ C) (F₂ : D ⥤ E) (G : C × E ⥤ H) :
    uncurry.obj (F₁ ⋙ (F₂ ⋙ (curry.obj G).flip).flip) = (F₁.prod F₂) ⋙ G :=
  Functor.ext (by simp)
    (fun ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ ⟨f₁, f₂⟩ => by
      dsimp
      simp only [Category.id_comp, Category.comp_id, ← G.map_comp, prod_comp])

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