English
In a suitable setting, the natural transformation that arises from applying the functor N₂ after Karoubi-completion exhibits isomorphisms at every object; hence it is a natural isomorphism.
Русский
В корректной обстановке натуральное преобразование, полученное после применения functor N₂ к каруоби-комплату, обладает изоморфизмами на каждом объекте; следовательно, оно является натуральной изоморфизмом.
LaTeX
$$$\Gamma_2 N_2\text{.natTrans}$ is a natural isomorphism; equivalently, $\forall P:\operatorname{Karoubi}(\mathrm{SimplicialObject}\, C),\; (\Gamma_2 N_2.natTrans).app P$ is an isomorphism.$$
Lean4
instance : IsIso (Γ₂N₂.natTrans : (N₂ : Karoubi (SimplicialObject C) ⥤ _) ⋙ _ ⟶ _) :=
by
have : ∀ P : Karoubi (SimplicialObject C), IsIso (Γ₂N₂.natTrans.app P) :=
by
intro P
have : IsIso (N₂.map (Γ₂N₂.natTrans.app P)) :=
by
have h := identity_N₂_objectwise P
dsimp only [Functor.id_obj, Functor.comp_obj] at h
rw [hom_comp_eq_id] at h
rw [h]
infer_instance
exact isIso_of_reflects_iso _ N₂
apply NatIso.isIso_of_isIso_app
