flipIsoCurrySwapUncurry — Mathlib

English

The functor F.flip is naturally isomorphic to the curry of the swapped product followed by uncurry: F.flip ≅ curry.obj (Prod.swap ⋅ uncurry.obj F).

Русский

Функтор F.flip естественным образом изоморфен к карри-образу переставленного произведения и раскуррированию: F.flip ≅ curry.obj (Prod.swap ⋅ uncurry.obj F).

LaTeX

$$$F.\text{flip} \cong \operatorname{curry.obj}(\mathrm{Prod.swap} \_\_ \_ \circ \mathrm{uncurry.obj} F)$$$

Lean4

/-- `F.flip` is isomorphic to uncurrying `F`, swapping the variables, and currying. -/
@[simps!]
def flipIsoCurrySwapUncurry (F : C ⥤ D ⥤ E) : F.flip ≅ curry.obj (Prod.swap _ _ ⋙ uncurry.obj F) :=
  NatIso.ofComponents fun d => NatIso.ofComponents fun _ => Iso.refl _

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