English
The functor Γ₀ sends a chain complex K to a simplicial object, by mapping a Δ to the direct sum of summands Σ_k X_k indexed by Splitting.IndexSet Δ, with the structure maps defined via the above summand maps.
Русский
Функтор Γ₀ отправляет комплекс цепей K в симплициальный объект, сопоставляя каждому Δ прямую сумму сумманд Σ_k X_k, индексируемых Splitting.IndexSet Δ, с структурами отображений, заданными через соответствующие отображения сумманд.
LaTeX
$$$Γ₀.obj(K): Δ \mapsto \bigoplus_{A ∈ Splitting.IndexSet Δ} K.X A.1.len$$$
Lean4
@[reassoc]
theorem map_on_summand {Δ Δ' : SimplexCategoryᵒᵖ} (A : Splitting.IndexSet Δ) (θ : Δ ⟶ Δ') {Δ'' : SimplexCategory}
{e : Δ'.unop ⟶ Δ''} {i : Δ'' ⟶ A.1.unop} [Epi e] [Mono i] (fac : e ≫ i = θ.unop ≫ A.e) :
((Γ₀.splitting K).cofan Δ).inj A ≫ (Γ₀.obj K).map θ =
Γ₀.Obj.Termwise.mapMono K i ≫ ((Γ₀.splitting K).cofan Δ').inj (Splitting.IndexSet.mk e) :=
by
dsimp [Splitting.cofan]
change (_ ≫ (Γ₀.obj K).map A.e.op) ≫ (Γ₀.obj K).map θ = _
rw [assoc, ← Functor.map_comp]
dsimp [splitting]
rw [Γ₀.Obj.map_on_summand₀ K (Splitting.IndexSet.id A.1)
(show e ≫ i = ((Splitting.IndexSet.e A).op ≫ θ).unop ≫ 𝟙 _ by rw [comp_id, fac]; rfl)]
dsimp only [Splitting.IndexSet.id_fst, Splitting.IndexSet.mk, op_unop, Splitting.IndexSet.e]
rw [Γ₀.Obj.map_on_summand₀ K (Splitting.IndexSet.id (op Δ'')) (show e ≫ 𝟙 Δ'' = e.op.unop ≫ 𝟙 _ by simp),
Termwise.mapMono_id]
dsimp only [Splitting.IndexSet.id_fst]
rw [id_comp]
rfl