mk_of_preserves_isUniversal — Mathlib

English

A preservation lemma about the hom-factor of the left Kan extension when preserving holds.

Русский

Лемма сохранения для гом-фактора левого кан-расширения при сохранении.

LaTeX

$$$\operatorname{leftKanExtensionCompIsoOfPreserves\_hom\_fac}$$$

Lean4

/-- Show that `G` preserves left Kan extensions if it maps some left Kan extension to a left
Kan extension, phrased in terms of `IsUniversal`. -/
theorem mk_of_preserves_isUniversal (E : LeftExtension L F) (hE : E.IsUniversal)
    (h : Nonempty (LeftExtension.postcompose₂ L F G |>.obj E).IsUniversal) : G.PreservesLeftKanExtension F L :=
  .mk' G F L fun hE' ↦
    ⟨Limits.IsInitial.equivOfIso (LeftExtension.postcompose₂ L F G |>.mapIso <| Limits.IsInitial.uniqueUpToIso hE hE')
        h.some⟩

Похожие утверждения