singleFunctorsPostcompQIso_hom_hom

English

The hom component of the isomorphism singleFunctorsPostcompQIso is the identity on objects, i.e., each n-level hom map is the identity morphism in the derived picture.

Русский

Гом-компонента изоморфизма singleFunctorsPostcompQIso равна тождественному морфизму на соответствующих объектах; каждый гомоморфизм уровня n является тождественным в получившейся производной картине.

LaTeX

$$$(singleFunctorsPostcompQIso C).hom.hom n = \mathrm{Id} _$$$

Lean4

theorem singleFunctorsPostcompQIso_hom_hom (n : ℤ) : (singleFunctorsPostcompQIso C).hom.hom n = 𝟙 _ :=
  by
  ext X
  dsimp [singleFunctorsPostcompQIso, HomotopyCategory.singleFunctorsPostcompQuotientIso, quotientCompQhIso,
    HomologicalComplexUpToQuasiIso.quotientCompQhIso]
  rw [CategoryTheory.Functor.map_id, Category.id_comp]
  erw [Category.id_comp]
  rfl

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