uncurry_obj_curry_obj_flip_flip — Mathlib

English

The uncurrying of F.flip is isomorphic to swapping the factors followed by the uncurry of F.

Русский

Раскурривание F.flip изоморфно перестановке факторов затем раскурриванию F.

LaTeX

$$$\operatorname{uncurry.obj} F.flip \cong \operatorname{Prod.swap} \_ \_ \circ \operatorname{uncurry.obj} F$$$

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])

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