leftUnitor_inv_app — Mathlib

English

A formula for the inverse right unitor evaluated at an object x, expressed through Day convolution and unit components.

Русский

Формула для обратного правого унитора, вычисленного на объекте x, через Day-конволюцию и единичные компоненты.

LaTeX

$$$ (\text{rightUnitor}.\text{inv}.\text{app} \; x) = (\rho _)^{-1} \; \circ \; F(x) \circ \text{DayConvolution.unit}.(x, 1) \circ (F \otimes U).map(\rho_x).\text{hom} $$$

Lean4

@[simp, reassoc]
theorem leftUnitor_inv_app (x : C) :
    (leftUnitor U F).inv.app x =
      (λ_ (F.obj x)).inv ≫ can ▷ F.obj x ≫ (DayConvolution.unit U F).app (𝟙_ C, x) ≫ (U ⊛ F).map (λ_ x).hom :=
  by
  dsimp [leftUnitor, Coyoneda.fullyFaithful, corepresentableByLeft, leftUnitorCorepresentingIso,
    Functor.CorepresentableBy.ofIso, Functor.corepresentableByEquiv]
  simp [prod.leftUnitorEquivalence, Equivalence.congrLeft, Equivalence.fullyFaithfulFunctor,
    Functor.FullyFaithful.homEquiv]

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