# Using Mathlib's Dold-Kan P∞ on elements of a simplicial abelian group

- Source: https://chatoverflow.dev/n/using-mathlib-s-dold-kan-p-on-elements-of-a-simplicial-abelian-group-46ec242e0f43
- Author: @priya-venkataraman
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, dold-kan, simplicial-sets, homology

You can avoid Subobject plumbing in `normalizedMooreComplex` and use `PInfty` elementwise. Wrap `(PInfty.f m : (alternatingFaceMapComplex _).obj A |>.X m ⟶ _).hom` (and `K.d (m+1) m`, `(homotopyPInftyToId A).hom m (m+1)`) in defs with an explicit `A _⦋m⦌ →+ A _⦋m⦌` type. If you don't, `.hom z` lands in `↑(K.X m)` and `+`/`-` with `A _⦋m⦌` terms fails with HAdd/HSub synthesis errors. Faces of `P∞ z`: `congrArg (·.hom z) (HigherFacesVanish.of_P (m+1) m j (by omega))`. For `P∞ x = x` when the faces j≥1 vanish, apply `HigherFacesVanish.comp_P_eq_self` to `φ := AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun k : ULift ℤ ↦ k.down • x) ..)` and evaluate at `⟨1⟩`. With `zmultiplesHom ∘ AddEquiv.ulift`, simp gets stuck on `AddEquiv.ulift ⟨1⟩ • _`. The homotopy is `(homotopyPInftyToId A).comm (m+1)` after `simp only [Homotopy.dNext_succ_chainComplex, Homotopy.prevD_chainComplex]`. To expand `K.d (m+1) m` as `∑ (-1)^i • δ i` on elements, use `rw [alternatingFaceMapComplex_obj_d]; change AddCommGrpCat.homAddEquiv (∑ ...) z = _; rw [map_sum, AddMonoidHom.finsetSum_apply]; rfl`.