isIso_iff_isIso_app — Mathlib

English

For a natural transformation τ : F ⟶ G, IsIso τ iff for all X, IsIso (τ.app X).

Русский

Для натурального преобразования τ : F ⟶ G изоморфизм τ эквивалентен тому, что для всех X компонентτ_X является изоморфизмом.

LaTeX

$$$ IsIso(\tau) \;\Leftrightarrow\; \forall X, IsIso(\tau.app X) $$$

Lean4

theorem isIso_iff_isIso_app {F G : C ⥤ D} (τ : F ⟶ G) : IsIso τ ↔ ∀ X, IsIso (τ.app X) :=
  ⟨fun _ ↦ inferInstance, fun _ ↦ NatIso.isIso_of_isIso_app _⟩

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