FiniteSimplicialSet

Coproduct (disjoint union) of two finite simplicial sets, (X + Y)_n = X_n + Y_n -- no degeneracy interaction between the two factors, unlike product: a generator's faces stay entirely within whichever side it came from, so this is just tagging generators with Left/Right and delegating.

Every simplex of a finitely-generated simplicial set is, by the same Eilenberg-Zilber normal-form theorem SSetElement itself is built on, uniquely (word, generator) with generator non-degenerate of some dimension p <= n and word a size-(n - p) subset of {0, ..., n-1} (sorted decreasing) -- so this enumerates ALL of X_n, not just its generators, by pairing every generator at every dimension p <= n with every such subset. Needed to build product, which has to consider every element of X_n x Y_n, not just the non-degenerate ones, before filtering down to the pairs that are non-degenerate in the product.

Ergonomic layer over quotient for the common case: identify PAIRS of same-dimension generators with each other directly (never a degenerate collapse down a dimension -- see quotient's own doc for that more general case). Computes the quotient map via a small union-find over the transitive closure of pairs, implemented fresh right here rather than reusing streams.UnionFind: cells sits below streams in this codebase's package layering (algebra -> cells -> streams -> homology), so importing it here would be a backwards dependency, and a hand-built, small-scale set of generators has no performance need for anything beyond the simplest union-find anyway. Each connected component's Ordering[G]-minimum member is its canonical representative -- a deterministic, reproducible choice rather than an arbitrary one.

Product of two finite simplicial sets, (X x Y)_n = X_n x Y_n degreewise.

Top dimension is provably maxDim(x) + maxDim(y), not merely an analogy to CW-complex dimension: a non-degenerate pair (a,b) at dimension n needs a.word/b.word to be disjoint subsets of an n-element set, and each has size n - dim(generator) >= n - maxDim (since dim(generator) <= maxDim), so disjointness forces (n - maxDim(x)) + (n - maxDim(y)) <= n, i.e. n <= maxDim(x) + maxDim(y) -- beyond that bound, no pair can possibly be non-degenerate, permanently, not just at that one dimension.

Face maps reuse faceOf on each side independently; the result can come back degenerate IN THE PRODUCT even when the input pair wasn't (a nonempty common word entry can appear on both sides after taking a face), so it's re-normalized by stripping the common degeneracy set J from both words and wrapping the stripped pair as a new generator degenerate by exactly J -- valid for the same diagonal reason above: an s_j present in both sides' own normal form at once is exactly the product's own s_j applied to what's left.

Quotient of a finite simplicial set by an arbitrary map from generators to elements: quotientMap(g) says what g becomes in the quotient -- either a genuine surviving representative (SSetElement(Nil, g), a FIXED POINT) or a properly degenerate collapse (SSetElement(word, rep) for some OTHER representative rep). This is deliberately more general than G => G (generator-to-generator only), because identifying cells can crush one of them down a dimension, not just merge same-dimension cells with a peer. Concretely: Hatcher's own single-2-simplex Delta-complex model of RP^2 (Algebraic Topology, Example 2.4 -- cross-validated against the independently-hand-built SimplicialSetFixtures.realProjectiveSpace(2) in SimplicialSetConstructionsSpec) glues two of a filled triangle's three edges together into one loop, but the THIRD edge doesn't glue to anything else -- it collapses entirely to a degenerate point over the surviving vertex. A G => G quotient map cannot express that third case at all, only G => SSetElement[G] can (identify, below, covers the common generator-to-generator case ergonomically without ever needing this extra generality itself).

quotientMap must be dimension-consistent (dimOf(quotientMap(g).generator) + quotientMap(g).word.length == dimOf(g)) and every generator must resolve to a fixed point IN ONE STEP (some generator rep with quotientMap(rep) == SSetElement(Nil, rep)) -- quotientMap is not itself iterated to a fixpoint, so a chain (quotientMap(a) = SSetElement(Nil, b), quotientMap(b) = SSetElement(Nil, c), b never a fixed point) is a caller error, checked explicitly below rather than left to validate(): validate()'s own structural check only inspects faces(g) for g already in the surviving generatorsByDim, so a chain would slip through silently whenever no surviving cell's face happens to target the broken link directly (identify is immune to this by construction -- its own find always path-compresses to a genuine root -- so this exposure is specific to a hand-written quotientMap passed to quotient directly).

facesOf reuses the ORIGINAL face data of a surviving representative, then pushes each face's own target through quotientMap too, composing the two degeneracy words via insertOuter one step at a time (word.foldRight(mapped.word)(insertOuter)) -- a face that was already degenerate, whose target ALSO collapses further under the quotient, needs both effects combined into one normalized word, exactly the composition s_word(s_word2(rep2)) that insertOuter is built to accumulate.

validate() on the RESULT is a necessary precondition beyond the fixed-point check above -- it will flag a quotientMap that isn't dimension-consistent as a structural error -- but NOT a sufficient correctness check: it verifies the simplicial identities hold, not that the quotient is the intended one, and an over-eager quotientMap can produce an internally-consistent but topologically wrong space. Homology cross-checks against an independently-derived expectation are what actually establish correctness.