AlgebraicTopology.NormalizedMooreComplex.map.proof_1

theorem AlgebraicTopology.NormalizedMooreComplex.map.proof_1 : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Abelian C] {X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) (n : ℕ), (AlgebraicTopology.NormalizedMooreComplex.objX Y n).Factors (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.NormalizedMooreComplex.objX X n).arrow (f.app (Opposite.op (SimplexCategory.mk n))))

This theorem states that for any category `C` which is an Abelian category, and for any `X` and `Y` which are simplicial objects in `C`, given a morphism `f` from `X` to `Y` and a natural number `n`, there exists a factorisation of the composition `(CategoryTheory.Subobject.arrow (AlgebraicTopology.NormalizedMooreComplex.objX X n))` and `(f.app (Opposite.op (SimplexCategory.mk n)))` through the `n`-th object of the normalized Moore complex of `Y`. In simple terms, it means the arrow from the `n`-th object of the normalized Moore complex of `X` followed by the `n`-th map of `f` factors through the `n`-th object of the normalized Moore complex of `Y`.

More concisely: For any Abelian category `C`, given simplicial objects `X` and `Y` and a morphism `f : X → Y`, there exists a factorization through the `n`-th object of the normalized Moore complex of `Y` for each natural number `n`, of the composition of the `n`-th map of `f` with the arrow from the `n`-th object of the normalized Moore complex of `X`.