instIsIso — Mathlib

English

A natural transformation between functors from a discrete index to a category C is an isomorphism if each component is an isomorphism.

Русский

Естественное преобразование между функторами из дискретного индекса в категорию C является изоморфизмом, если каждая компонента является изоморфизмом.

LaTeX

$$$\\forall i, IsIso (f_i) \\implies IsIso (\\mathrm{Discrete.natTrans} f)$$$

Lean4

instance {I : Type u₁} {i j : Discrete I} (f : i ⟶ j) : IsIso f :=
  ⟨⟨Discrete.eqToHom (eq_of_hom f).symm, by cat_disch⟩⟩

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