English
The family PInfty respects the f-naturality: for any morphism f between simplicial objects, the square with PInfty and f commutes.
Русский
Семейство PInfty сохраняет естественность по f: для любого отображения f между простейшими объектами диаграмма с PInfty и f коммутирует.
LaTeX
$$$f.app(\!op\;\langle n \rangle) \;\circ\; PInfty.f_n = PInfty.f_n \;\circ\; f.app(\!op\;\langle n \rangle)$$$
Lean4
/-- The endomorphism `PInfty : K[X] ⟶ K[X]` obtained from the `P q` by passing to the limit. -/
noncomputable def PInfty : K[X] ⟶ K[X] :=
ChainComplex.ofHom _ _ _ _ _ _ (fun n => ((P n).f n : X _⦋n⦌ ⟶ _)) fun n => by
simpa only [← P_is_eventually_constant (show n ≤ n by rfl), AlternatingFaceMapComplex.obj_d_eq] using
(P (n + 1) : K[X] ⟶ _).comm (n + 1) n
