English
The identity on N₂.Obj coincides with the composition of the Karoubi-internal maps built from Γ₂ and N₂ when evaluated at object P; this is the standard objectwise identity relation in the Karoubi setting.
Русский
Тождество на N₂.Obj совпадает с композицией каруоби-вложенных отображений, построенных из Γ₂ и N₂ при вычислении на объекте P; это стандартное объектно-правильное тождество в каруоби-окружении.
LaTeX
$$$\mathrm{Id}_{N₂.obj P} = (N₂Γ₂.inv.app (N₂.obj P))\circ (N₂.map (Γ₂N₂.natTrans.app P))$$$
Lean4
theorem identity_N₂ :
(𝟙 (N₂ : Karoubi (SimplicialObject C) ⥤ _) ◫ N₂Γ₂.inv) ≫
(Functor.associator _ _ _).inv ≫ Γ₂N₂.natTrans ◫ 𝟙 (@N₂ C _ _) =
𝟙 N₂ :=
by
ext P : 2
dsimp only [NatTrans.comp_app, NatTrans.hcomp_app, Functor.comp_map, Functor.associator, NatTrans.id_app,
Functor.comp_obj]
rw [Γ₂.map_id, N₂.map_id, comp_id, id_comp, id_comp, identity_N₂_objectwise P]
