inclusionOfMooreComplexMap_comp_PInfty

English

There is an isomorphism between N₁ and the composition of normalized Moore and Karoubi inclusions, provided by the Karoubi equivalence bookkeeping.

Русский

Существует изоморфизм между N₁ и композицией нормализованного Moore и вложений Karoubi, обеспечиваемый сопоставлением Каруоби-эквивалентности.

LaTeX

$$$N_1 \cong (\text{normalizedMooreComplex}) \circ (\text{toKaroubi})$$$

Lean4

@[reassoc (attr := simp)]
theorem inclusionOfMooreComplexMap_comp_PInfty (X : SimplicialObject A) :
    inclusionOfMooreComplexMap X ≫ PInfty = inclusionOfMooreComplexMap X :=
  by
  ext (_ | n)
  · dsimp
    simp only [comp_id]
  · exact (HigherFacesVanish.inclusionOfMooreComplexMap n).comp_P_eq_self

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