English
A succinct form of map_epi_on_summand_id', showing that the computation reduces to the identity once Δ and Δ' are aligned, reflecting the functorial behavior on identity morphisms at the summand level.
Русский
Краткая форма map_epi_on_summand_id', показывающая, что вычисление сводится к тождеству, если Δ и Δ′ согласованы, что отражает функториальность по тождественному отображению на уровне сумманд.
LaTeX
$$map_epi_on_summand_id'(K,i) = Id$$
Lean4
/-- The functor `Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C`, on morphisms. -/
@[simps]
def map {K K' : ChainComplex C ℕ} (f : K ⟶ K') : obj K ⟶ obj K'
where
app Δ := (Γ₀.splitting K).desc Δ fun A => f.f A.1.unop.len ≫ ((Γ₀.splitting K').cofan _).inj A
naturality {Δ' Δ}
θ := by
apply (Γ₀.splitting K).hom_ext'
intro A
simp only [(splitting K).ι_desc_assoc, Obj.map_on_summand'_assoc K _ θ, (splitting K).ι_desc, assoc,
Obj.map_on_summand' K' _ θ]
apply Obj.Termwise.mapMono_naturality_assoc
