English
The Q_q morphisms are natural with respect to maps of simplicial objects; they commute with f in the same way as P_q does for the f-components.
Русский
Морфизмы Q_q естественны по отношению к отображениям симплициальных объектов; они commuting с f так же, как и P_q для компонент f.
LaTeX
$$$\forall q,n,\; f:\, X \to Y,\; f_{obj} \circ (Q_q).f n = (Q_q).f n \circ f_{obj}$.$$
Lean4
theorem map_P {D : Type*} [Category D] [Preadditive D] (G : C ⥤ D) [G.Additive] (X : SimplicialObject C) (q n : ℕ) :
G.map ((P q : K[X] ⟶ _).f n) = (P q : K[((whiskering C D).obj G).obj X] ⟶ _).f n := by
induction q with
| zero =>
simp only [P_zero]
apply G.map_id
| succ q hq =>
simp only [P_succ, comp_add, HomologicalComplex.comp_f, HomologicalComplex.add_f_apply, comp_id, Functor.map_add,
Functor.map_comp, hq, map_Hσ]
