English
The inclusion of the Moore complex into the alternating face-map complex is a homotopy equivalence; equivalently, there exists a homotopy inverse up to homotopy between these two chain complexes.
Русский
Включение нормированного комплекса Моора в чередующийся комплекс лиц-обратных отображений является гомотопической эквивалентностью; то есть существует гомотопическое обратное отображение между этими двойками цепных комплексов.
LaTeX
$$$\text{incl}_\text{Moore} : (\text{normalizedMooreComplex} ) \to (\text{alternatingFaceMapComplex}) \quad \text{is a homotopy equivalence.}$$$
Lean4
/-- The inclusion of the Moore complex in the alternating face map complex
is a homotopy equivalence -/
@[simps]
def homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex {A : Type*} [Category A] [Abelian A]
{Y : SimplicialObject A} : HomotopyEquiv ((normalizedMooreComplex A).obj Y) ((alternatingFaceMapComplex A).obj Y)
where
hom := inclusionOfMooreComplexMap Y
inv := PInftyToNormalizedMooreComplex Y
homotopyHomInvId := Homotopy.ofEq (splitMonoInclusionOfMooreComplexMap Y).id
homotopyInvHomId :=
Homotopy.trans (Homotopy.ofEq (PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap Y))
(homotopyPInftyToId Y)
