N₂Γ₂_compatible_with_N₁Γ₀

English

The inv-component of N₂Γ₂ on X equals the composition of X.p.f with the inj from the Γ₀ splitting, aligning with PInfty on the summand.

Русский

Обратный компонент N₂Γ₂ на X равен композиции X.p.f с инъекцией от Γ₀ разбиения, согласованной с PInfty на суммирующем подобъекте.

LaTeX

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

Lean4

theorem N₂Γ₂_compatible_with_N₁Γ₀ (K : ChainComplex C ℕ) :
    N₂Γ₂.hom.app ((toKaroubi _).obj K) = N₂Γ₂ToKaroubiIso.hom.app K ≫ N₁Γ₀.hom.app K :=
  congr_app whiskerLeft_toKaroubi_N₂Γ₂_hom K

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