English
There is a corepresentable iso expressing the right unitor in the Day convolution setting.
Русский
Существует изоморфизм ядра-представления, выражающий правый унитор Day-конволюции.
LaTeX
$$$ (\text{RightUnitorCorepresentingIso}) :\; (\text{whiskeringLeft} \; (\text{tensor} C)).\text{obj} (F) \;\cong\; \mathrm{Coyoneda}.(\op F) $$$
Lean4
/-- Characterizing the forward direction of `leftUnitor` via the universal maps. -/
@[reassoc (attr := simp)]
theorem leftUnitor_hom_unit_app (y : C) :
can ▷ F.obj y ≫ (DayConvolution.unit U F).app (𝟙_ C, y) ≫ (leftUnitor U F).hom.app (𝟙_ C ⊗ y) =
(λ_ (F.obj y)).hom ≫ F.map (λ_ y).inv :=
by
have :=
congrArg (fun t ↦ t.app (.mk PUnit.unit, y)) <|
(corepresentableByLeft U F).homEquiv.rightInverse_symm <| ((leftUnitorCorepresentingIso F).symm.hom.app F) (𝟙 _)
dsimp [leftUnitor, Coyoneda.fullyFaithful, corepresentableByLeft, leftUnitorCorepresentingIso,
Functor.CorepresentableBy.ofIso, Functor.corepresentableByEquiv] at this ⊢
simp only [whiskerLeft_id, Category.comp_id] at this
simp only [Category.comp_id, this]
simp [prod.leftUnitorEquivalence, Equivalence.congrLeft, Equivalence.fullyFaithfulFunctor,
Functor.FullyFaithful.homEquiv]
