Русский
Если H' является точечным левым Кан-расширением вдоль L и tensorLeft сохраняет колимиты, то K ⊠ H является точечным левым Кан-расширением вдоль Id_E × L.
LaTeX
$$$(\\text{isPointwiseLeftKanExtensionExtensionUnitRight}) : (P: (H' α).IsPointwiseLeftKanExtension) \\to (K \\boxtimes H) \\text{ is pointwise along } (Id_E × L)$$$
Lean4
/-- If `H' : D' ⥤ V` is a pointwise left Kan extension along `L : D ⥤ D'` and
if tensoring left with an object preserves colimits in `V`,
then `K ⊠ H' : D' × E ⥤ V` is a pointwise left Kan extension along `(𝟭 E) × L`. -/
def isPointwiseLeftKanExtensionExtensionUnitRight
[∀ d : D', ∀ e : E, Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorLeft <| K.obj e)]
(P : Functor.LeftExtension.mk H' α |>.IsPointwiseLeftKanExtension) :
Functor.LeftExtension.mk (K ⊠ H') (extensionUnitRight H' α K) |>.IsPointwiseLeftKanExtension := fun ⟨e, d⟩ ↦
isPointwiseLeftKanExtensionAtExtensionUnitRight H' α K d (P d) e
