English
There is a natural quasi-isomorphism between the forgetful image of the standard resolution and the augmentation-into-1-skeleton, compatible with the εToSingle₀ map.
Русский
Существует естественный квазиизоморфизм между отображением забывания стандартного резолюционного комплекса и аугментацией в нулевую компоненту, совместимый с εToSingle₀.
LaTeX
$$QuasiIso (forget₂ _ (ModuleCat k)).mapHomologicalComplex (εToSingle₀ k G).$$
Lean4
/-- The homotopy equivalence of complexes of `k`-modules between the standard resolution of `k` as
a trivial `G`-representation, and the complex which is `k` at 0 and 0 everywhere else, acts as
`∑ nᵢgᵢ ↦ ∑ nᵢ : k[G¹] → k` at 0. -/
theorem forget₂ToModuleCatHomotopyEquiv_f_0_eq :
(forget₂ToModuleCatHomotopyEquiv k G).1.f 0 = (forget₂ (Rep k G) _).map (ε k G) :=
by
refine ModuleCat.hom_ext <| Finsupp.lhom_ext fun (x : Fin 1 → G) r => ?_
change mapDomain _ _ _ = Finsupp.linearCombination _ _ _
simp only [HomotopyEquiv.ofIso, Iso.symm_hom, compForgetAugmented, compForgetAugmentedIso, eqToIso.inv,
HomologicalComplex.eqToHom_f]
change mapDomain _ (single x r) _ = _
simp [Unique.eq_default (terminal.from _), single_apply, if_pos (Subsingleton.elim _ _)]
