toKaroubiCompN₂IsoN₁ — Mathlib

English

The functor N₂Γ₂ToKaroubiIso is an isomorphism between the Karoubi envelope of the chain complexes and the corresponding Karoubi of simplicial objects, compatible with N₂ and Γ₂.

Русский

Функтор N₂Γ₂ToKaroubiIso является изоморфизмом между каруоби-оболочкой цепных комплексов и соответствующим каруоби симплициальных объектов, совместимым с N₂ и Γ₂.

LaTeX

$$$N_2\Gamma_2^{\mathrm{ToKaroubiIso}} : \mathrm{Karoubi}(\mathrm{ChainComplex}(C, \mathbb{N})) \cong \mathrm{Karoubi}(\mathrm{SimplicialObject}(C))$$$

Lean4

/-- The canonical isomorphism `toKaroubi (SimplicialObject C) ⋙ N₂ ≅ N₁`. -/
def toKaroubiCompN₂IsoN₁ : toKaroubi (SimplicialObject C) ⋙ N₂ ≅ N₁ :=
  (functorExtension₁CompWhiskeringLeftToKaroubiIso _ _).app N₁

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