bibkey: differentialgeometry2026finitecells
authors: The DifferentialGeometry contributors
year: 2026
title: Maximal simplicial cells and finite cell induction
doi: null
url: https://github.com/qinz1yang/differential-geometry/tree/afc0a69081be678c24cb55c5111236af329bfda1
claim: Every finite simplicial set satisfies induction from the initial case and pushouts attaching standard simplices along their entire boundaries.
strata_touched:
  - D5/S3/Geometry/FiniteSimplicialCellInduction
license: Apache-2.0, Copyright 2026 The DifferentialGeometry contributors
triage: anchor

Maximal simplicial cells and finite cell induction

Verified locator

The immutable source is https://github.com/qinz1yang/differential-geometry/tree/afc0a69081be678c24cb55c5111236af329bfda1. The corresponding Lean files are MaximalCell.lean and FiniteCellInduction.lean. Their declarations are costar_preimage_cellMap, costar_cell_isPushout, card_costar_nondegenerate_lt, and finite_cell_induction, with the characteristic and attaching maps used in these statements.

Maximal cell decomposition

For a simplicial set $X$ and a nondegenerate simplex $s$, let $C_s$ be the subcomplex of simplices $x$ for which the cell generated by $s$ is not contained in the cell generated by $x$. The preimage of $C_s$ under the characteristic map ${\Delta }^{\dim s}\to X$ is its entire boundary. That characteristic map is injective away from the boundary, even when boundary faces are identified. If $s$ is maximal in the order on nondegenerate simplices, its generated cell and $C_s$ cover $X$. These facts construct the pushout

$$X\cong C_s{\cup }_{\partial {\Delta }^{\dim s}}{\Delta }^{\dim s}.$$

The nondegenerate simplices of $C_s$ are exactly the nondegenerate simplices $t$ of $X$ with $s\nleqq t$. For finite $X$, their number is strictly smaller than that of $X$, since the inclusion misses $s$.

Finite cell induction

Let $P$ be a proposition on simplicial sets in a fixed universe. Suppose $P$ holds for every initial simplicial set and is preserved by every pushout that attaches a standard simplex along its boundary, provided $P$ holds both for the preceding simplicial set and for that boundary. Then $P$ holds for every finite simplicial set. The proof uses induction first on a finite dimension bound and then on the number of nondegenerate simplices. The boundary has a smaller dimension bound, and the costar has fewer nondegenerate simplices. This applies to simplicial sets with identifications and requires no regularity hypothesis on the boundary attaching map.

These are existing upstream results. Their cell decomposition supports later comparisons between simplicial and singular homology; the induction theorem alone makes no Euler-characteristic or surface-classification assertion.

Source port and retirement

The supplier pins Lean 4.33.1; the receiving repository pins Lean 4.33.0 with mathlib revision db584cd6d46c92f209a44c0f1c829460d327499d. The source port combines the two source modules in one mathematical namespace, preserves their statements and proof bodies, and omits an unused automatic association lemma. The complete upstream license and NOTICE accompany the Lean source. This is licensed reuse without a mathematical novelty claim.

Use equivalent statements directly from this repository’s own pinned Mathlib when that pin supplies the same hypotheses and conclusions; the exact application and equivalence must be verified at that pin. Acceptance by another repository is not the retirement condition.