inclusionOfMooreComplexMap_f — Mathlib

English

The nth component of the inclusion map between Moore and alternating complexes is the arrow given by NormalizedMooreComplex.objX X n.

Русский

n-й компонент включения между Moore и чередующимся комплексом равен стрелке (NormalizedMooreComplex.objX X n).arrow.

LaTeX

$$$(\text{inclusionOfMooreComplexMap } X).f\,n = (\text{NormalizedMooreComplex.objX } X\, n).\mathrm{arrow}$$$

Lean4

@[simp]
theorem inclusionOfMooreComplexMap_f (X : SimplicialObject A) (n : ℕ) :
    (inclusionOfMooreComplexMap X).f n = (NormalizedMooreComplex.objX X n).arrow :=
  by
  dsimp only [inclusionOfMooreComplexMap]
  exact ChainComplex.ofHom_f _ _ _ _ _ _ _ _ n

Похожие утверждения