English
The natural transformations Γ₂N₁.natTrans and Γ₂N₂.natTrans are compatible via the Karoubi isomorphism between N₂ and N₁, i.e., applying Γ₂N₂.natTrans then the inverse Karoubi iso equals applying Γ₂N₁.natTrans after mapping through the Karoubi level.
Русский
Натуральные преобразования Γ₂N₁.natTrans и Γ₂N₂.natTrans совместимы через каруоби-изоморфизм между N₂ и N₁: применение Γ₂N₂.natTrans затем обратного каруоби-изоморфизма эквивалентно применению Γ₂N₁.natTrans после отображения на уровне Кароуоби.
LaTeX
$$$Γ₂N₁.natTrans.app X = (Γ₂N₂ToKaroubiIso.app X).inv \circ Γ₂N₂.natTrans.app ((toKaroubi (SimplicialObject C)).obj X)$$$
Lean4
theorem compatibility_Γ₂N₁_Γ₂N₂_natTrans (X : SimplicialObject C) :
Γ₂N₁.natTrans.app X = (Γ₂N₂ToKaroubiIso.app X).inv ≫ Γ₂N₂.natTrans.app ((toKaroubi (SimplicialObject C)).obj X) :=
by
rw [Γ₂N₂.natTrans_app_f_app]
dsimp only [Karoubi.decompId_i_toKaroubi, Karoubi.decompId_p_toKaroubi, Functor.comp_map, NatTrans.comp_app]
rw [N₂.map_id, Γ₂.map_id, Iso.app_inv]
dsimp only [toKaroubi]
erw [id_comp]
rw [comp_id, Iso.inv_hom_id_app_assoc]
