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