N₂Γ₂_inv_app_f_f — Mathlib

English

The hom-component of the isomorphism between the two-step Karoubi composition and N₁Γ₀ equals PInfty at each level.

Русский

Гомоморфная часть изоморфизма между двумя уровнями кароуоби-композиций и N₁Γ₀ равна PInfty на каждом уровне.

LaTeX

$$$\big( toKaroubiCompN_2IsoN_1 \text{.hom} \text{ .app } X \big).f = PInfty$$$

Lean4

@[simp]
theorem N₂Γ₂_inv_app_f_f (X : Karoubi (ChainComplex C ℕ)) (n : ℕ) :
    (N₂Γ₂.inv.app X).f.f n = X.p.f n ≫ ((Γ₀.splitting X.X).cofan _).inj (Splitting.IndexSet.id (op ⦋n⦌)) :=
  by
  dsimp [N₂Γ₂]
  simp only [whiskeringLeft_obj_preimage_app, NatTrans.comp_app, Functor.comp_map, Karoubi.comp_f,
    N₂Γ₂ToKaroubiIso_inv_app, HomologicalComplex.comp_f, N₁Γ₀_inv_app_f_f, toKaroubi_obj_X,
    Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f, PInfty_on_Γ₀_splitting_summand_eq_self, N₂_map_f_f, Γ₂_map_f_app,
    unop_op, Karoubi.decompId_p_f, PInfty_on_Γ₀_splitting_summand_eq_self_assoc, Splitting.IndexSet.id_fst,
    SimplexCategory.len_mk, Splitting.ι_desc]
  apply Karoubi.HomologicalComplex.p_idem_assoc

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