English
The functor N₂: Karoubi(SimplicialObject C) ⥤ Karoubi(ChainComplex C ⟂ ℕ) reflects isomorphisms; i.e., a morphism is an isomorphism if its image under N₂ is an isomorphism.
Русский
Функтор N₂: Karoubi(SimplicialObject C) ⥤ Karoubi(ChainComplex C ⟂ ℕ) отражает изоморфизмы; если отображение является изоморфизмом после применения N₂, то исходный морфизм также является изоморфизмом.
LaTeX
$$$N_2\;:\;\mathrm{Karoubi}(\mathrm{SimplicialObject}(C)) \to \mathrm{Karoubi}(\mathrm{ChainComplex}(C,\mathbb{N}))$ reflects isomorphisms$$
Lean4
instance : (N₁ : SimplicialObject C ⥤ Karoubi (ChainComplex C ℕ)).ReflectsIsomorphisms :=
⟨fun {X Y} f =>
by
intro
-- restating the result in a way that allows induction on the degree n
suffices ∀ n : ℕ, IsIso (f.app (op ⦋n⦌))
by
haveI : ∀ Δ : SimplexCategoryᵒᵖ, IsIso (f.app Δ) := fun Δ => this Δ.unop.len
apply NatIso.isIso_of_isIso_app
have h₁ := HomologicalComplex.congr_hom (Karoubi.hom_ext_iff.mp (IsIso.hom_inv_id (N₁.map f)))
have h₂ := HomologicalComplex.congr_hom (Karoubi.hom_ext_iff.mp (IsIso.inv_hom_id (N₁.map f)))
have h₃ := fun n => Karoubi.HomologicalComplex.p_comm_f_assoc (inv (N₁.map f)) n (f.app (op ⦋n⦌))
simp only [N₁_map_f, Karoubi.comp_f, HomologicalComplex.comp_f, AlternatingFaceMapComplex.map_f, N₁_obj_p,
Karoubi.id_f, assoc] at h₁ h₂ h₃
intro n
induction n with
-- degree 0
| zero =>
use (inv (N₁.map f)).f.f 0
have h₁₀ := h₁ 0
have h₂₀ := h₂ 0
dsimp at h₁₀ h₂₀
simp only [id_comp] at h₁₀ h₂₀
tauto
| succ n
hn =>
use φ {
a := PInfty.f (n + 1) ≫ (inv (N₁.map f)).f.f (n + 1)
b := fun i => inv (f.app (op ⦋n⦌)) ≫ X.σ i }
simp only [MorphComponents.id, ← id_φ, ← preComp_φ, preComp, ← postComp_φ, postComp, PInfty_f_naturality_assoc,
IsIso.hom_inv_id_assoc, assoc, IsIso.inv_hom_id_assoc, SimplicialObject.σ_naturality, h₁, h₂, h₃, and_self]⟩
