English
There is a canonical isomorphism in Karoubi (the Karoubi envelope) relating N₂ followed by Γ₂ and N₁ followed by Γ₂; this expresses a compatibility between two factorizations of the functors in the idempotent completion.
Русский
Существует каноническое изоморфизм в envelope Karoubi, связывающий последовательности N₂ ∘ Γ₂ и N₁ ∘ Γ₂; он демонстрирует совместимость двух разложений функционалов в каруоби-окружении.
LaTeX
$$$N_2 \circ Γ_2 \cong N_1 \circ Γ_2 \quad \text{in Karoubi}(SimplicialObject C)$$$
Lean4
/-- The natural transformation `N₁ ⋙ Γ₂ ⟶ toKaroubi (SimplicialObject C)`. -/
@[simps]
def natTrans : (N₁ : SimplicialObject C ⥤ _) ⋙ Γ₂ ⟶ toKaroubi _
where
app
X :=
{ f :=
{ app := fun Δ => (Γ₀.splitting K[X]).desc Δ fun A => PInfty.f A.1.unop.len ≫ X.map A.e.op
naturality := fun Δ Δ' θ => by
apply (Γ₀.splitting K[X]).hom_ext'
intro A
change _ ≫ (Γ₀.obj K[X]).map θ ≫ _ = _
simp only [Splitting.ι_desc_assoc, assoc, Γ₀.Obj.map_on_summand'_assoc, Splitting.ι_desc]
erw [Γ₀_obj_termwise_mapMono_comp_PInfty_assoc X (image.ι (θ.unop ≫ A.e))]
dsimp only [toKaroubi]
simp only [← X.map_comp]
congr 2
simp only [← op_comp]
exact Quiver.Hom.unop_inj (A.fac_pull θ) }
comm := by
apply (Γ₀.splitting K[X]).hom_ext
intro n
dsimp [N₁]
simp only [← Splitting.cofan_inj_id, Splitting.ι_desc, comp_id, Splitting.ι_desc_assoc, assoc,
PInfty_f_idem_assoc] }
naturality {X Y}
f := by
ext1
apply (Γ₀.splitting K[X]).hom_ext
intro n
dsimp [N₁, toKaroubi]
simp only [← Splitting.cofan_inj_id, Splitting.ι_desc, Splitting.ι_desc_assoc, assoc, PInfty_f_idem_assoc,
PInfty_f_naturality_assoc, NatTrans.naturality, Splitting.IndexSet.id_fst, unop_op, len_mk]
