English
A left-corepresentable by structure for the DayConvolutionUnit maps out of U ⊛ F via a left Kan extension, reflecting the left-side universal property of the unit.
Русский
Левая структура corepresentableBy для U ⊛ F описывает отображения из U ⊛ F через левое Кан-расширение, отражая левую универсальную собственность единицы.
LaTeX
$$$\\text{corepresentableByLeft } U F : ...$$$
Lean4
/-- A `CorepresentableBy` structure that characterizes maps out of `F ⊛ U` by
leveraging the fact that `F ⊠ U` is a left Kan extension of `F ⊠ (fromPUnit 𝟙_ V)`. -/
@[simps]
def corepresentableByRight [DayConvolution F U] :
(whiskeringLeft _ _ _).obj (tensor C) ⋙
(whiskeringLeft _ _ _).obj ((𝟭 C).prod (Functor.fromPUnit.{0} (𝟙_ C))) ⋙
coyoneda.obj (.op <| F ⊠ Functor.fromPUnit.{0} (𝟙_ V)) |>.CorepresentableBy
(F ⊛ U)
where
homEquiv :=
Functor.homEquivOfIsLeftKanExtension _ (DayConvolution.unit F U) _ |>.trans <|
Functor.homEquivOfIsLeftKanExtension _ (extensionUnitRight U (φ U) F) _
homEquiv_comp := by aesop
