εToSingle₀_comp_eq — Mathlib

English

There is a quasi-isomorphism after forgetting structure that relates to εToSingle₀.

Русский

После забывания части структуры существует квазиизоморфизм, связанный с εToSingle₀.

LaTeX

$$QuasiIso (((forget₂ _ (ModuleCat k)).mapHomologicalComplex _).map (εToSingle₀ k G))$$

Lean4

theorem εToSingle₀_comp_eq :
    ((forget₂ _ (ModuleCat.{u} k)).mapHomologicalComplex _).map (εToSingle₀ k G) ≫
        (HomologicalComplex.singleMapHomologicalComplex _ _ _).hom.app _ =
      (forget₂ToModuleCatHomotopyEquiv k G).hom :=
  by
  dsimp
  ext1
  simpa using (forget₂ToModuleCatHomotopyEquiv_f_0_eq k G).symm

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