hasLeftExtension_iff_of_iso₁ — Mathlib

English

If L ≅ L' as functors C ⥤ D, then L has a left Kan extension of F if and only if L' has a left Kan extension of F.

Русский

Если L ≅ L' как функторы C ⥤ D, то L имеет лево-каноническое расширение F тогда и только тогда, когда L' имеет такое же расширение.

LaTeX

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

Lean4

theorem hasLeftExtension_iff_of_iso₁ : HasLeftKanExtension L F ↔ HasLeftKanExtension L' F :=
  (leftExtensionEquivalenceOfIso₁ iso₁ F).hasInitial_iff

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