hasRightExtension_iff_postcomp₁

English

Analogous to Left extensions: existence of a right Kan extension along L' with F is equivalent to existence along L when L ⋙ G ≅ L'.

Русский

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

LaTeX

$$$L'.HasRightKanExtension F \iff L.HasRightKanExtension F$$$

Lean4

theorem hasRightExtension_iff_postcomp₁ (e : L ⋙ G ≅ L') (F : C ⥤ H) :
    HasRightKanExtension L' F ↔ HasRightKanExtension L F :=
  (RightExtension.postcomp₁ G e.hom F).asEquivalence.hasTerminal_iff

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