inclusionOfMooreComplexMap — Mathlib

English

The functor N₂: Karoubi(SimplicialObject C) ⥤ Karoubi(ChainComplex C ℕ) reflects isomorphisms; in particular, an arrow is an isomorphism if its image under N₂ is an isomorphism.

Русский

Функтор N₂: Karoubi(SimplicialObject C) ⥤ Karoubi(ChainComplex C ℕ) отражает изоморфизмы; если образ стрелки под N₂ есть изоморфизм, то стрелка изоморфизм.

LaTeX

$$$N_2 : \mathrm{Karoubi}(\mathrm{SimplicialObject}(C)) \to \mathrm{Karoubi}(\mathrm{ChainComplex}(C,\mathbb{N}))$ reflectsIsomorphisms$$

Lean4

theorem inclusionOfMooreComplexMap (n : ℕ) : HigherFacesVanish (n + 1) ((inclusionOfMooreComplexMap X).f (n + 1)) :=
  fun j _ => by
  dsimp [AlgebraicTopology.inclusionOfMooreComplexMap, NormalizedMooreComplex.objX]
  rw [← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ j (by simp only [Finset.mem_univ])), assoc,
    kernelSubobject_arrow_comp, comp_zero]

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