English
If G preserves any pointwise right Kan extension of F along L at c, then G preserves all of them at c.
Русский
Если G сохраняет любое точечное правое Кан-расширение F вдоль L в точке c, то он сохраняет все такие расширения в точке c.
LaTeX
$$$\\forall c\\in\\mathrm{Ob}(C),\\ [\\exists E:\\text{RightExtension } L F \\text{ with } E\\text{ IsPointwiseRightKanExtensionAt } c] \\\\ \\land\\ [(RightExtension.postcompose_{L,F,G} |>.obj E)\\text{ IsPointwiseRightKanExtensionAt } c] \\Rightarrow G.PreservesPointwiseRightKanExtensionAt F L c.$$$
Lean4
/-- If `G` preserves any pointwise right Kan extension of `F` along `L` at `c`, then it preserves
all of them. -/
theorem mk' (c : C) {E : RightExtension L F} (hE : E.IsPointwiseRightKanExtensionAt c)
(hGE : (RightExtension.postcompose₂ L F G |>.obj E).IsPointwiseRightKanExtensionAt c) :
G.PreservesPointwiseRightKanExtensionAt F L c where
preserves E'
hE' :=
⟨Limits.IsLimit.ofIsoLimit hGE <|
(E.coneAtWhiskerRightIso G F L c) ≪≫
(Limits.Cones.functoriality _ _).mapIso (hE.uniqueUpToIso hE') ≪≫ (E'.coneAtWhiskerRightIso G F L c).symm⟩
