PInftyToNormalizedMooreComplex_naturality

English

For each n, the inclusion maps of the normalized Moore complex objX X n factor through PInfty.f n, i.e. PInfty encodes the filtered image of the Moore data.

Русский

Для каждого n включения нормализованного Moore-комплекса objX X n факторизуют через PInfty.f n, то есть PInfty кодирует фильтрованное изображение Moore-данных.

LaTeX

$$$\mathrm{Subobject}.Factors (\mathrm{NormalizedMooreComplex.objX} X\, n) (PInfty.f\, n)$$$

Lean4

@[reassoc (attr := simp)]
theorem PInftyToNormalizedMooreComplex_naturality {X Y : SimplicialObject A} (f : X ⟶ Y) :
    AlternatingFaceMapComplex.map f ≫ PInftyToNormalizedMooreComplex Y =
      PInftyToNormalizedMooreComplex X ≫ NormalizedMooreComplex.map f :=
  by cat_disch

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