English
The Day convolution F ⊛ G is corepresented by the bifunctor F ⊠ G via a universal property encoded by a left Kan extension, i.e., there is a canonical correspondence between morphisms out of F ⊛ G and appropriate natural transformations from the tensor bifunctor to F ⊠ G.
Русский
Day конволюция F ⊛ G является корпредставленной двойственным константным бифунктором F ⊠ G через универсальное свойство левого кан-расширения; существует каноническое соответствие между морфизмами из F ⊛ G и естественными преобразованиями.
LaTeX
$$$\\text{corepresentableBy } F G : ((F \\⊠ G) \\text{ is corepresented by } (F \\⊛ G)$$$
Lean4
/-- The universal property of left Kan extensions characterizes the functor
corepresented by `F ⊛ G`. -/
@[simps!]
def corepresentableBy :
(Functor.whiskeringLeft _ _ _).obj (tensor C) ⋙ coyoneda.obj (.op <| F ⊠ G) |>.CorepresentableBy (F ⊛ G)
where
homEquiv := Functor.homEquivOfIsLeftKanExtension _ (unit F G) _
homEquiv_comp := by aesop
