N₂Γ₂ToKaroubiIso_hom_app — Mathlib

English

For a Karoubi object X with p being the projector, the f-component of the inverse of N₂Γ₂ evaluated at X is given by composing X.p.f with the Γ₀-splitting summand inclusion.

Русский

Для объекта Кароуби X с проектором p, компонент f обратного N₂Γ₂ на X задаётся композицией X.p.f с инъекцией разбиения Γ₀.

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_hom_app (X : ChainComplex C ℕ) : (N₂Γ₂ToKaroubiIso.hom.app X).f = PInfty :=
  by
  ext n
  dsimp [N₂Γ₂ToKaroubiIso]
  simp only [comp_id, assoc, PInfty_f_idem]
  conv_rhs => rw [← PInfty_f_idem]
  congr 1
  apply (Γ₀.splitting X).hom_ext'
  intro A
  rw [Splitting.ι_desc_assoc, assoc]
  apply id_comp

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