bifunctorComp₁₂Iso — Mathlib

English

There is a canonical isomorphism describing bifunctorComp₂₃ in terms of currying, involving associators and uncurry operations.

Русский

Существует каноническое изоморфирование bifunctorComp₂₃ через каррирование, с участием ассоциатора и операций uncurry.

LaTeX

$$$$ \\mathrm{bifunctorComp}_{23} F G_{23} \\cong \\mathrm{curry.obj}\\big(\\mathrm{curry.obj}\\big(\\mathrm{prod.associator}\\; \\_\\; \\_ \\; ⋙ \\mathrm{uncurry.obj}(\\mathrm{uncurry.obj G_{23} \\;⋙ F.flip}).flip\\big)\\big). $$$$

Lean4

/-- `bifunctorComp₁₂` can be described in terms of the curryfication of functors. -/
@[simps!]
def bifunctorComp₁₂Iso (F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂) (G : C₁₂ ⥤ C₃ ⥤ E) :
    bifunctorComp₁₂ F₁₂ G ≅ curry.obj (uncurry.obj F₁₂ ⋙ G) :=
  NatIso.ofComponents (fun _ => NatIso.ofComponents (fun _ => Iso.refl _))

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