English
Let E be a universal right extension of L along F, and suppose there exists a universalization of the postcomposition with G. Then G preserves right Kan extensions along L for F.
Русский
Пусть E — универсальное правое расширение along F, а предположим, что постсоставление с G также универсализировано. Тогда G сохраняет правые Кан-расширения вдоль L для F.
LaTeX
$$$E\\text{ универсальное по отношению к } (L,F) \\wedge [\\text{Nonempty }(RightExtension.postcompose_{L,F,G} |>.obj E).IsUniversal] \\Rightarrow G \\text{PreservesRightKanExtension } F L.$$$
Lean4
/-- Show that `G` preserves right Kan extensions if it maps some right Kan extension to a left
Kan extension, phrased in terms of `IsUniversal`. -/
theorem mk_of_preserves_isUniversal (E : RightExtension L F) (hE : E.IsUniversal)
(h : Nonempty (RightExtension.postcompose₂ L F G |>.obj E).IsUniversal) : G.PreservesRightKanExtension F L :=
.mk' G F L fun hE' ↦
⟨Limits.IsTerminal.equivOfIso
(RightExtension.postcompose₂ L F G |>.mapIso <| Limits.IsTerminal.uniqueUpToIso hE hE') h.some⟩
