postComp
plain-language theorem explainer
Post-composition with a morphism g of ℤ-modules, packaged as a ℤ-linear map Hom(ℤ,M)→Hom(ℤ,N). Singular-subdivision lemmas cite it to move boundaries, induced chain maps, and subdivision operators past the toChain embedding. The body is the composite f↦f≫g, with additivity and scalar laws from the preadditive structure on ModuleCat.
Claim. For $\mathbb{Z}$-modules $M,N$ and a morphism $g:M\to N$, the assignment $f\mapsto f\circ g$ defines a $\mathbb{Z}$-linear map $\mathrm{Hom}_{\mathbb{Z}}(\mathbb{Z},M)\to\mathrm{Hom}_{\mathbb{Z}}(\mathbb{Z},N)$.
background
The module Foundation.SingularSubdivision builds the bridge between affine simplicial chains on the standard simplex and singular chains on a topological space $X$. Generators are continuous maps $\sigma:\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin}(n+1))\to X$, and toChain sends an affine simplex to the corresponding singular generator (a morphism out of $\mathbb{Z}$ in ModuleCat).
In an abelian category of modules, morphisms out of $\mathbb{Z}$ behave like elements of the target. Post-composition with a fixed $g:M\to N$ therefore acts on those "elements" and must itself be $\mathbb{Z}$-linear. That linear map is exactly what this definition records, so later lemmas can write (postComp g).comp (toChain …) without unpacking category composition by hand.
Sibling infrastructure includes affine boundary abnd, affine cone, and the barycentric subdivision operator; the singular side has bnd, chainMap, and sdOp.
proof idea
Definitional construction, not a theorem. The underlying function is ordinary categorical post-composition f ≫ g. Additivity is discharged by rewriting with Preadditive.add_comp; scalar compatibility uses RingHom.id_apply and Preadditive.zsmul_comp. No external lemmas beyond the preadditive API of ModuleCat are required.
why it matters
Local plumbing for the singular-subdivision package. Three intertwining lemmas depend on it: toChain_comp_abnd (toChain intertwines affine and singular boundary), toChain_comp_chainMap (toChain intertwines post-composition with the induced chain map of a continuous map), and toChain_comp_sdOp (toChain intertwines singular subdivision sdOp with affine barycentric subdivision). Without a named linear post-composition operator those equalities cannot be stated as compositions of LinearMaps. The declaration itself is pure homological algebra; it does not invoke Recognition forcing (T0–T8), the J-cost, or the phi ladder, but it supports the chain-level geometry those foundations later sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.