English
In an abelian setting with suitable cofibrations, the inclusionOfMooreComplexMap X is a split mono; its retraction is given by PInftyToNormalizedMooreComplex X and satisfies the usual split-id condition.
Русский
В абелевой категории с подходящими кофибриками включение inclusionOfMooreComplexMap X является разделимым монохом; обратное отображение задано PInftyToNormalizedMooreComplex X и удовлетворяет свойству разложения.
LaTeX
$$SplitMono (inclusionOfMooreComplexMap X) with retraction $PInftyToNormalizedMooreComplex X$ and $PInftyToNormalizedMooreComplex X \circ inclusionOfMooreComplexMap X = \mathrm{id}$.$$
Lean4
/-- `inclusionOfMooreComplexMap X` is a split mono. -/
def splitMonoInclusionOfMooreComplexMap (X : SimplicialObject A) : SplitMono (inclusionOfMooreComplexMap X)
where
retraction := PInftyToNormalizedMooreComplex X
id := by
simp only [← cancel_mono (inclusionOfMooreComplexMap X), assoc, id_comp,
PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap, inclusionOfMooreComplexMap_comp_PInfty]
