isLeftKanExtension_iff_isIso — Mathlib

English

Let α, α' be as above with e and φ an isomorphism. Then F''.IsLeftKanExtension α' holds iff IsIso φ.

Русский

Пусть α, α' как выше и φ — изоморфизм. Тогда F''′IsLeftKanExtension α' эквивалентно тому, что φ является изоморфизмом.

LaTeX

$$$[F'.IsLeftKanExtension α] \Rightarrow (F''.IsLeftKanExtension α' \iff IsIso φ)$$$

Lean4

theorem isLeftKanExtension_iff_isIso {F' : D ⥤ H} {F'' : D ⥤ H} (φ : F' ⟶ F'') {L : C ⥤ D} {F : C ⥤ H} (α : F ⟶ L ⋙ F')
    (α' : F ⟶ L ⋙ F'') (comm : α ≫ whiskerLeft L φ = α') [F'.IsLeftKanExtension α] :
    F''.IsLeftKanExtension α' ↔ IsIso φ := by
  constructor
  · intro
    rw [F'.hom_ext_of_isLeftKanExtension α φ (leftKanExtensionUnique _ α _ α').hom (by simp [comm])]
    infer_instance
  · intro
    exact isLeftKanExtension_of_iso (asIso φ) α α' comm

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