English
A unit-extension morphism φ is used to relate DayConvolution unit with the left Kan extension built from the unit, providing a universal comparison morphism.
Русский
Морфизм расширения единицы φ связывает единицу DayConvolution с левой Кан-расширением, построенным из единицы, обеспечивая универсальное сравнение морфизмов.
LaTeX
$$$(F ⊠ U) IsLeftKanExtension \\text{ extensionUnitLeft φ F}$$$
Lean4
/-- A `CorepresentableBy` structure that characterizes maps out of `U ⊛ F`
by leveraging the fact that `U ⊠ F` is a left Kan extension of `(fromPUnit 𝟙_ V) ⊠ F`. -/
@[simps]
def corepresentableByLeft [DayConvolution U F] :
(whiskeringLeft _ _ _).obj (tensor C) ⋙
(whiskeringLeft _ _ _).obj ((Functor.fromPUnit.{0} (𝟙_ C)).prod (𝟭 C)) ⋙
coyoneda.obj (.op <| Functor.fromPUnit.{0} (𝟙_ V) ⊠ F) |>.CorepresentableBy
(U ⊛ F)
where
homEquiv :=
Functor.homEquivOfIsLeftKanExtension _ (DayConvolution.unit U F) _ |>.trans <|
Functor.homEquivOfIsLeftKanExtension _ (extensionUnitLeft U (φ U) F) _
homEquiv_comp := by aesop
