suppOf
plain-language theorem explainer
Support of a finitely supported integer tuple in the coproduct ∐_κ ℤ, returned as a Finset of indices. Algebraic topology proofs that rebuild chains from coordinates (Mayer–Vietoris middle exactness, compact-support lifts for arc complements) cite it. The body is the direct-sum isomorphism followed by DFinsupp.support.
Claim. For $z \in \coprod_{\kappa} \mathbb{Z}$ (as an object of $\mathbf{Mod}_{\mathbb{Z}}$), $\mathrm{supp}(z)$ is the finite set of indices $i \in \kappa$ at which the $i$-th coordinate of $z$ is nonzero.
background
In the singular Mayer–Vietoris setup, free singular chains are assembled from generators indexed by a type $\kappa$ of singular simplices (or small simplices after subdivision). The ambient abelian group is the coproduct $\coprod_{\kappa} \mathbb{Z}$ in $\mathbf{Mod}_{\mathbb{Z}}$, i.e. finite integer linear combinations of those generators.
Mathlib identifies that coproduct with the direct sum of copies of $\mathbb{Z}$, whose underlying type is a finitely supported function $\kappa \to \mathbb{Z}$. The support of such a function is the finite set of indices with nonzero value; that is the combinatorial footprint of a chain.
The module lives inside SingularMayerVietoris, which builds the MV short complex from inclusions of open sets $U,V$ and their intersection, using the small-complex and subdivision infrastructure imported from SingularPrism, SingularPair, and SingularSubdivision.
proof idea
Definition, not a proof. Map $z$ across ModuleCat.coprodIsoDirectSum into the direct-sum presentation, then take the DFinsupp.support of the image. Noncomputable only because the isomorphism is.
why it matters
This is the bookkeeping primitive for every place the MV or arc-complement arguments must know which generators appear in a chain. Downstream, mem_suppOf_iff equates membership in the support with a nonzero coordinate; sum_coordAt_smul_unitOf rebuilds $z$ as the finite sum of its coordinates times unit generators, summing only over suppOf z.
mv_middle_exact (heart of Mayer–Vietoris exactness: a cancelling pair of chains on $U$ and $V$ comes from a chain on $U \cap V$) uses the support to assemble the preimage. Outside the module, exists_chain_lift (compact-support lifting for complements) quantifies over suppOf c to guarantee a chain on a larger complement pushes forward correctly, and that lemma feeds arcComplementsAcyclic (Hatcher 2B.1, arc case: $H_1$-acyclic complements of embedded arcs in $S^D$).
In the Recognition forcing chain the same singular toolkit underwrites dimension and linking statements tied to T8 ($D=3$) and high-dimensional vanishing; the support definition is pure linear algebra underneath those geometric claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.