English
If a morphism i is δ₀ and Δ ≠ Δ′, then the composition mapMono i with the differential is zero; this is a compatibility check for the differential in the summand decomposition.
Русский
Если i является δ₀ и Δ ≠ Δ′, то композиция mapMono i с дифференциалом равна нулю; это согласование для дифференциала в разложении по суммам.
LaTeX
$$mapMono(K,i) = 0 when Δ ≠ Δ′ or i not δ₀$$
Lean4
/-- The simplicial morphism on the simplicial object `Γ₀.obj K` induced by
a morphism `Δ' → Δ` in `SimplexCategory` is defined on each summand
associated to an `A : Splitting.IndexSet Δ` in terms of the epi-mono factorisation
of `θ ≫ A.e`. -/
def map (K : ChainComplex C ℕ) {Δ' Δ : SimplexCategoryᵒᵖ} (θ : Δ ⟶ Δ') : obj₂ K Δ ⟶ obj₂ K Δ' :=
Sigma.desc fun A => Termwise.mapMono K (image.ι (θ.unop ≫ A.e)) ≫ Sigma.ι (summand K Δ') (A.pull θ)
