whiskerLeft_toKaroubi_N₂Γ₂_hom

English

The F-component of the inverse of N₂Γ₂ evaluated at a Karoubi object X matches the product X.p.f with the summand inclusion coming from the Γ₀ splitting.

Русский

Компонента F обратного N₂Γ₂ на Кароуби-объекте X равна произведению X.p.f и инъекции разбиения Γ₀.

LaTeX

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

Lean4

theorem whiskerLeft_toKaroubi_N₂Γ₂_hom :
    whiskerLeft (toKaroubi (ChainComplex C ℕ)) N₂Γ₂.hom = N₂Γ₂ToKaroubiIso.hom ≫ N₁Γ₀.hom :=
  by
  let e : _ ≅ toKaroubi (ChainComplex C ℕ) ⋙ 𝟭 _ := N₂Γ₂ToKaroubiIso ≪≫ N₁Γ₀
  have h := ((whiskeringLeft _ _ (Karoubi (ChainComplex C ℕ))).obj (toKaroubi (ChainComplex C ℕ))).map_preimage e.hom
  dsimp only [whiskeringLeft, N₂Γ₂, Functor.preimageIso] at h ⊢
  exact h

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