English
Characterization of the forward direction of right unitor via universal maps in Day convolution.
Русский
Характеризация направления правого унитора через универзальные отображения Day-конволюции.
LaTeX
$$$ (\text{rightUnitor_hom_unit_app}) :\; F(X) \; \otimes \; can \; \to \; (\text{unit}) \to (\text{rightUnitor}(F X)).\text{hom} $$$
Lean4
/-- Characterizing the forward direction of `rightUnitor` via the universal maps. -/
@[reassoc (attr := simp)]
theorem rightUnitor_hom_unit_app (x : C) :
F.obj x ◁ can ≫ (DayConvolution.unit F U).app (x, 𝟙_ C) ≫ (rightUnitor U F).hom.app (x ⊗ 𝟙_ C) =
(ρ_ _).hom ≫ F.map (ρ_ x).inv :=
by
have :=
congrArg (fun t ↦ t.app (x, .mk PUnit.unit)) <|
(corepresentableByRight U F).homEquiv.rightInverse_symm <| ((rightUnitorCorepresentingIso F).symm.hom.app F) (𝟙 _)
dsimp [rightUnitor, Coyoneda.fullyFaithful, corepresentableByRight, rightUnitorCorepresentingIso,
Functor.CorepresentableBy.ofIso, Functor.corepresentableByEquiv] at this ⊢
simp only [MonoidalCategory.whiskerRight_id, Category.id_comp, Iso.hom_inv_id, Category.comp_id] at this
simp only [Category.comp_id, this]
simp [prod.rightUnitorEquivalence, Equivalence.congrLeft, Equivalence.fullyFaithfulFunctor,
Functor.FullyFaithful.homEquiv]
