d_comp_ε — Mathlib

English

The differential composed with the augmentation map ε is zero in the standard resolution.

Русский

Дифференциал, скомпонованный с аугментацией, равен нулю в стандартном резолюционном комплексе.

LaTeX

$$$d_{1,0} \\circ \\varepsilon = 0$$$

Lean4

theorem d_comp_ε : (standardComplex k G).d 1 0 ≫ ε k G = 0 :=
  by
  ext : 3
  have : (forget₂ToModuleCat k G).d 1 0 ≫ (forget₂ (Rep k G) (ModuleCat.{u} k)).map (ε k G) = 0 :=
    by
    rw [← forget₂ToModuleCatHomotopyEquiv_f_0_eq, ← (forget₂ToModuleCatHomotopyEquiv k G).1.2 1 0 rfl]
    exact comp_zero
  exact LinearMap.ext_iff.1 (ModuleCat.hom_ext_iff.mp this) _

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