mapBifunctorLeftUnitor_inv_apply — Mathlib

English

The inverse of the left unitor component at j is obtained by composing the inverse of e at Y j with the inverse of the singleObjApplyIso and then projecting via ιMapBifunctorMapObj.

Русский

Обратный к компоненте левого унитора на j образуется как композиция обратного к e в компоненте Y j с обратным к одиночному отображению и затем через ιMapBifunctorMapObj.

LaTeX

$$$ (mapBifunctorLeftUnitor F X e p hp Y).inv j \\\\; = \\\\; e.inv.app (Y j) \\\\; ≫ \\\\; (F.map (singleObjApplyIso (0 : I) X).inv).app (Y j) \\\\; ≫ \\\\; ιMapBifunctorMapObj F p ((single₀ I).obj X) Y 0 j j (hp j) $$$

Lean4

theorem mapBifunctorLeftUnitor_inv_apply (j : J) :
    (mapBifunctorLeftUnitor F X e p hp Y).inv j =
      e.inv.app (Y j) ≫
        (F.map (singleObjApplyIso (0 : I) X).inv).app (Y j) ≫
          ιMapBifunctorMapObj F p ((single₀ I).obj X) Y 0 j j (hp j) :=
  rfl

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