English
The inverse of the right unitor is given by composing the inverse of the e-map with the inverse of the singleObjApplyIso and then applying theι-map conjugation entry ιMapBifunctorMapObj, reflecting the canonical decomposition of the right unitor.
Русский
Обратный правый унитор расписывается как композиция обратной e-марши, затем обратной единичной мапы и применения ιMapBifunctorMapObj, что совместимо с каноническим разложением правого унитора.
LaTeX
$$$ (mapBifunctorRightUnitor F Y e p hp X).inv j = e.inv.app (X j) \gg (F.obj (X j)).map (singleObjApplyIso (0 : I) Y).inv \gg ιMapBifunctorMapObj F p X ((single₀ I).obj Y) j 0 j (hp j) $$$
Lean4
/-- Given `F : D ⥤ C ⥤ D`, `Y : C`, `e : F.flip.obj Y ≅ 𝟭 D`, `X : GradedObject J D` and
`p : J × I → J` such that `p ⟨j, 0⟩ = j` for all `j`,
this is the right unitor isomorphism `mapBifunctorMapObj F p X ((single₀ I).obj Y) ≅ X`. -/
noncomputable def mapBifunctorRightUnitor : mapBifunctorMapObj F p X ((single₀ I).obj Y) ≅ X :=
isoMk _ _ (fun j => (CofanMapObjFun.iso (mapBifunctorRightUnitorCofanIsColimit F Y e p hp X j)).symm)
