English
There is an explicit isomorphism between the nested application ((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y) and X a.c. a, given a ∈ J × I with a₂ = 0, built from the composite of mapIso and the left unitor.
Русский
Существует явное изоморфизм между вложенным применением ((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y) и X a, заданное для a ∈ J × I при a₂ = 0 из композиции mapIso и левого унитора.
LaTeX
$$$ \\exists \\alpha : (((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)) a \\cong X a.fst $$$
Lean4
/-- Given `F : D ⥤ C ⥤ D`, `Y : C`, `e : F.flip.obj X ≅ 𝟭 D` and `X : GradedObject J D`,
this is the isomorphism `((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y) a ≅ Y a.2`
when `a : J × I` is such that `a.2 = 0`. -/
@[simps!]
noncomputable def mapBifunctorObjObjSingle₀Iso (a : J × I) (ha : a.2 = 0) :
((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y) a ≅ X a.1 :=
Functor.mapIso _ (singleObjApplyIsoOfEq _ Y _ ha) ≪≫ e.app (X a.1)
