instIsIsoFunctorNatTrans — Mathlib

English

Let I be a type and F,G: Discrete I ⥤ C be functors. If for every i ∈ I the component f_i : F.obj i ⟶ G.obj i is an isomorphism, then the natural transformation Discrete.natTrans f is an isomorphism.

Русский

Пусть I — тип, и F,G: Discrete I ⥤ C — функторы. Если для каждого i ∈ I компонент f_i : F.obj i ⟶ G.obj i является изоморфизмом, тогда натуральная трансформация Discrete.natTrans f является изоморфизмом.

LaTeX

$$$\\bigl(\\forall i : \\text{Discrete } I,\\; IsIso\\,(f i)\\bigr) \\Rightarrow IsIso\\bigl(Discrete.natTrans f\\bigr).$$$

Lean4

instance {I : Type*} {F G : Discrete I ⥤ C} (f : ∀ i, F.obj i ⟶ G.obj i) [∀ i, IsIso (f i)] :
    IsIso (Discrete.natTrans f) :=
  by
  change IsIso (Discrete.natIso (fun i => asIso (f i))).hom
  infer_instance

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