English
For any P in Karoubi(SimplicialObject C), the composition of the inverse N₂Γ₂.inv at N₂.obj P with N₂.map of Γ₂N₂.natTrans.app P equals the identity on N₂.obj P; this holds objectwise.
Русский
Для любого P в Karoubi(SimplicialObject C) композиция N₂Γ₂.inv.app (N₂.obj P) затем N₂.map Γ₂N₂.natTrans.app P возвращает тождественный отображение на N₂.obj P, поэтапно по каждому объекту.
LaTeX
$$$(N₂Γ₂.inv.app (N₂.obj P)) \;\circ\; N₂.map (Γ₂N₂.natTrans.app P) = 𝟙 (N₂.obj P)$$$
Lean4
theorem identity_N₂_objectwise (P : Karoubi (SimplicialObject C)) :
(N₂Γ₂.inv.app (N₂.obj P) : N₂.obj P ⟶ N₂.obj (Γ₂.obj (N₂.obj P))) ≫ N₂.map (Γ₂N₂.natTrans.app P) = 𝟙 (N₂.obj P) :=
by
ext n
have eq₁ :
(N₂Γ₂.inv.app (N₂.obj P)).f.f n =
PInfty.f n ≫ P.p.app (op ⦋n⦌) ≫ ((Γ₀.splitting (N₂.obj P).X).cofan _).inj (Splitting.IndexSet.id (op ⦋n⦌)) :=
by simp only [N₂Γ₂_inv_app_f_f, N₂_obj_p_f, assoc]
have eq₂ :
((Γ₀.splitting (N₂.obj P).X).cofan _).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫ (N₂.map (Γ₂N₂.natTrans.app P)).f.f n =
PInfty.f n ≫ P.p.app (op ⦋n⦌) :=
by
dsimp
rw [PInfty_on_Γ₀_splitting_summand_eq_self_assoc, Γ₂N₂.natTrans_app_f_app]
dsimp
rw [Γ₂N₂ToKaroubiIso_hom_app, assoc, Splitting.ι_desc_assoc, assoc, assoc]
dsimp [toKaroubi]
rw [Splitting.ι_desc_assoc]
simp [Splitting.IndexSet.e]
simp only [Karoubi.comp_f, HomologicalComplex.comp_f, Karoubi.id_f, N₂_obj_p_f, assoc, eq₁, eq₂,
PInfty_f_naturality_assoc, app_idem, PInfty_f_idem_assoc]
