Γ₂N₂ — Mathlib

English

There is a unit isomorphism between the identity functor on Karoubi(SimplicialObject C) and the composite N₂ followed by Γ₂.

Русский

Существует единичный изоморфизм между тождественным функтором на Karoubi(SimplicialObject C) и композицией N₂ с Γ₂.

LaTeX

$$$\mathrm{Id} \cong (N_2) \circ \Gamma_2$$$

Lean4

/-- The unit isomorphism of the Dold-Kan equivalence. -/
@[simps! inv]
def Γ₂N₂ : 𝟭 _ ≅ (N₂ : Karoubi (SimplicialObject C) ⥤ _) ⋙ Γ₂ :=
  (asIso Γ₂N₂.natTrans).symm

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