English
Hσ is defined as a certain endomorphism-valued map on the alternating face map complex, built from hσ' by composing with differentials in the complex.
Русский
Hσ задаётся как оператор-эндоморфизм на чередующем составе лицевых карт, строящийся из hσ' путём композиции с дифференциалами комплексa.
LaTeX
$$$$ Hσ : K[X] \to K[X], \quad Hσ = nullHomotopicMap'(hσ') $$$$
Lean4
/-- The maps `hσ' q n m hnm` are compatible with the application of additive functors. -/
theorem map_hσ' {D : Type*} [Category D] [Preadditive D] (G : C ⥤ D) [G.Additive] (X : SimplicialObject C) (q n m : ℕ)
(hnm : c.Rel m n) :
(hσ' q n m hnm : K[((whiskering _ _).obj G).obj X].X n ⟶ _) = G.map (hσ' q n m hnm : K[X].X n ⟶ _) :=
by
unfold hσ' hσ
split_ifs
· simp only [Functor.map_zero, zero_comp]
· simp only [eqToHom_map, Functor.map_comp, Functor.map_zsmul]
rfl
