inclusionOfMooreComplex — Mathlib

English

There is a natural transformation from normalized Moore complex to the alternating face map complex, called inclusionOfMooreComplex.

Русский

Существует естественное преобразование из нормализованного Moore-комплекса в чередующийся лицевой комплекс, называемое inclusionOfMooreComplex.

LaTeX

$$$\text{inclusionOfMooreComplex} : \text{normalizedMooreComplex } A \Rightarrow \text{alternatingFaceMapComplex } A$$$

Lean4

/-- The inclusion map of the Moore complex in the alternating face map complex,
as a natural transformation -/
@[simps]
def inclusionOfMooreComplex : normalizedMooreComplex A ⟶ alternatingFaceMapComplex A where
  app := inclusionOfMooreComplexMap

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