English
A generalization of map_on_summand to the level of η-factors: the map on summands intertwines with the pullback along θ and factoring through A.
Русский
Обобщение map_on_summand для η-факторов: отображение на суммандах согласуется с тягой по θ и факторизацией через A.
LaTeX
$$map_on_summand'(K,A,θ) expresses the compatibility: summand → Γ₀.obj.map θ$$
Lean4
/-- By construction, the simplicial `Γ₀.obj K` is equipped with a splitting. -/
def splitting (K : ChainComplex C ℕ) : SimplicialObject.Splitting (Γ₀.obj K)
where
N n := K.X n
ι n := Sigma.ι (Γ₀.Obj.summand K (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌))
isColimit'
Δ :=
IsColimit.ofIsoColimit (colimit.isColimit _)
(Cofan.ext (Iso.refl _)
(by
intro A
dsimp [Splitting.cofan']
rw [comp_id,
Γ₀.Obj.map_on_summand₀ K (SimplicialObject.Splitting.IndexSet.id A.1)
(show A.e ≫ 𝟙 _ = A.e.op.unop ≫ 𝟙 _ by rfl),
Γ₀.Obj.Termwise.mapMono_id]
dsimp
rw [id_comp]
rfl))
