rightUnitor_inv_app — Mathlib

English

Naturality of the left unitor with respect to Day convolution extensions.

Русский

Естественность левого унитора по отношению к Day-конволюционным расширениям.

LaTeX

$$$ (\text{leftUnitor_naturality}) :\; DayConvolution.map(\mathrm{id})\; f \, = \, (\text{leftUnitor}(f))^\mathrm{hom} \, \circ \, f $$$

Lean4

@[simp, reassoc]
theorem rightUnitor_inv_app (x : C) :
    (rightUnitor U F).inv.app x =
      (ρ_ (F.obj x)).inv ≫ F.obj x ◁ can ≫ (DayConvolution.unit F U).app (x, 𝟙_ C) ≫ (F ⊛ U).map (ρ_ x).hom :=
  by
  dsimp [rightUnitor, Coyoneda.fullyFaithful, corepresentableByRight, rightUnitorCorepresentingIso,
    Functor.CorepresentableBy.ofIso, Functor.corepresentableByEquiv]
  simp [prod.rightUnitorEquivalence, Equivalence.congrLeft, Equivalence.fullyFaithfulFunctor,
    Functor.FullyFaithful.homEquiv]

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