N₂Γ₂ToKaroubiIso_inv_app — Mathlib

English

The same as 39150 but stated for the general Karoubi object X and indexing by n.

Русский

То же самое, что и в 39150, но сформулировано для общего Karoubi-объекта X и индекса n.

LaTeX

$$$\big( N_2Γ_2^{-1}\text{ app } X \big).f = X.p.f \circ ((Γ_0.splitting X.X).cofan{\}).inj(\mathrm{IndexSet.id}(op\,⟦n⟧))$$$

Lean4

@[simp]
theorem N₂Γ₂ToKaroubiIso_inv_app (X : ChainComplex C ℕ) : (N₂Γ₂ToKaroubiIso.inv.app X).f = PInfty :=
  by
  ext n
  dsimp [N₂Γ₂ToKaroubiIso]
  simp only [comp_id, PInfty_f_idem_assoc, AlternatingFaceMapComplex.obj_X, Γ₀_obj_obj]
  convert comp_id _
  apply (Γ₀.splitting X).hom_ext'
  intro A
  rw [Splitting.ι_desc]
  erw [comp_id, id_comp]

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