hasLeftExtension_iff_postcomp₁ — Mathlib

English

Existence of a left Kan extension for L' along F is equivalent to that for L along F when there is an isomorphism L ⋙ G ≅ L'.

Русский

Существование левого Кан-расширения вдоль L' для F эквивалентно существованию вдоль L для F при наличии изоморфизма L ⋙ G ≅ L'.

LaTeX

$$$L'.HasLeftKanExtension F \iff L.HasLeftKanExtension F$$$

Lean4

theorem hasLeftExtension_iff_postcomp₁ (e : L ⋙ G ≅ L') (F : C ⥤ H) :
    HasLeftKanExtension L' F ↔ HasLeftKanExtension L F :=
  (LeftExtension.postcomp₁ G e.inv F).asEquivalence.hasInitial_iff

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