isIso_pi_iff — Mathlib

English

For functors X, Y in the Pi-category, a morphism f: X ⟶ Y is an isomorphism if and only if each coordinate f i is an isomorphism.

Русский

Для функторов X, Y в Pi-категории морфизм f: X ⟶ Y является изоморфизмом тогда и только тогда, когда каждый координатный компонент f i является изоморфизмом.

LaTeX

$$$\\text{IsIso}(f) \\iff \\forall i, \\text{IsIso}(f_i)$$$

Lean4

theorem isIso_pi_iff {X Y : ∀ i, C i} (f : X ⟶ Y) : IsIso f ↔ ∀ i, IsIso (f i) :=
  by
  constructor
  · intro _ i
    exact (Pi.isoApp (asIso f) i).isIso_hom
  · intro
    exact ⟨fun i => inv (f i), by cat_disch, by cat_disch⟩

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