isIso_map_iff — Mathlib

English

Let e : F₁ ≅ F₂ be an isomorphism of functors. For any f: X → Y, IsIso(F₁.map f) ↔ IsIso(F₂.map f).

Русский

Пусть e : F₁ ≅ F₂ — изоморфизм функторов. Для любого f: X → Y верно IsIso(F₁.map f) ⇔ IsIso(F₂.map f).

LaTeX

$$$ IsIso(F_1.map(f)) \;\;\leftrightarrow\;\; IsIso(F_2.map(f)) $$$

Lean4

theorem isIso_map_iff {F₁ F₂ : C ⥤ D} (e : F₁ ≅ F₂) {X Y : C} (f : X ⟶ Y) : IsIso (F₁.map f) ↔ IsIso (F₂.map f) :=
  by
  revert F₁ F₂
  suffices ∀ {F₁ F₂ : C ⥤ D} (_ : F₁ ≅ F₂) (_ : IsIso (F₁.map f)), IsIso (F₂.map f) from fun F₁ F₂ e =>
    ⟨this e, this e.symm⟩
  intro F₁ F₂ e hf
  exact IsIso.mk ⟨e.inv.app Y ≫ inv (F₁.map f) ≫ e.hom.app X, by cat_disch⟩

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