Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Finite simplicial cell induction

Abstract

Finite simplicial sets admit induction by boundary attachments.

Definition 1.1 (The costar of a nondegenerate simplex).

Lean statement: D5/S3/Geometry/FiniteSimplicialCellInduction.costar

Formalization. D5/S3/Geometry/FiniteSimplicialCellInduction.costar (✓ std3).

Citation. The DifferentialGeometry contributors (2026). Maximal simplicial cells and finite cell induction. URL: https://github.com/qinz1yang/differential-geometry/tree/afc0a69081be678c24cb55c5111236af329bfda1.

Commentary.

For a simplicial set X in an arbitrary universe and a nondegenerate simplex s of X, the costar contains exactly those simplices x for which the subcomplex generated by s is not contained in the subcomplex generated by x. The functorial map condition makes this a subcomplex of X.

Definition 1.2 (The characteristic simplex map).

Lean statement: D5/S3/Geometry/FiniteSimplicialCellInduction.nondegenerateCellMap

Formalization. D5/S3/Geometry/FiniteSimplicialCellInduction.nondegenerateCellMap (✓ std3).

Citation. The DifferentialGeometry contributors (2026). Maximal simplicial cells and finite cell induction. URL: https://github.com/qinz1yang/differential-geometry/tree/afc0a69081be678c24cb55c5111236af329bfda1.

Commentary.

For each nondegenerate simplex s of dimension n in X, the Yoneda correspondence supplies the map from the standard simplicial n-simplex to X determined by s.

Theorem 1.3 (The removed cell meets the costar in its boundary).

Lean statement: D5/S3/Geometry/FiniteSimplicialCellInduction.costar_preimage_cellMap

Proof. Machine-checked in Lean as D5/S3/Geometry/FiniteSimplicialCellInduction.costar_preimage_cellMap (✓ std3). ∎

Citation. The DifferentialGeometry contributors (2026). Maximal simplicial cells and finite cell induction. URL: https://github.com/qinz1yang/differential-geometry/tree/afc0a69081be678c24cb55c5111236af329bfda1.

Commentary.

For every simplicial set X and nondegenerate simplex s, the preimage of the costar under the characteristic simplex map is exactly the boundary of the standard simplex of dimension s.dim. This equality needs no maximality hypothesis.

Theorem 1.4 (A maximal cell and its costar cover the space).

Lean statement: D5/S3/Geometry/FiniteSimplicialCellInduction.costar_sup_cell_eq_top

Proof. Machine-checked in Lean as D5/S3/Geometry/FiniteSimplicialCellInduction.costar_sup_cell_eq_top (✓ std3). ∎

Citation. The DifferentialGeometry contributors (2026). Maximal simplicial cells and finite cell induction. URL: https://github.com/qinz1yang/differential-geometry/tree/afc0a69081be678c24cb55c5111236af329bfda1.

Commentary.

For every simplicial set X and maximal nondegenerate simplex s in the nondegenerate-simplex order, the supremum of the costar subcomplex and the subcomplex generated by s is the top subcomplex of X.

Theorem 1.5 (Characteristic maps are injective away from the boundary).

Lean statement: D5/S3/Geometry/FiniteSimplicialCellInduction.nondegenerateCellMap_injOn_compl_boundary

Proof. Machine-checked in Lean as D5/S3/Geometry/FiniteSimplicialCellInduction.nondegenerateCellMap_injOn_compl_boundary (✓ std3). ∎

Citation. The DifferentialGeometry contributors (2026). Maximal simplicial cells and finite cell induction. URL: https://github.com/qinz1yang/differential-geometry/tree/afc0a69081be678c24cb55c5111236af329bfda1.

Commentary.

For a nondegenerate simplex s of X and every natural number m, the degree-m characteristic map is injective on the complement of the degree-m boundary. The uniqueness of nondegenerate presentations proves this even when boundary faces are identified.

Definition 1.6 (The boundary attaching map into the costar).

Lean statement: D5/S3/Geometry/FiniteSimplicialCellInduction.costarAttachingMap

Formalization. D5/S3/Geometry/FiniteSimplicialCellInduction.costarAttachingMap (✓ std3).

Citation. The DifferentialGeometry contributors (2026). Maximal simplicial cells and finite cell induction. URL: https://github.com/qinz1yang/differential-geometry/tree/afc0a69081be678c24cb55c5111236af329bfda1.

Commentary.

For every nondegenerate simplex s, the characteristic map restricted to the standard boundary factors through the costar. This factorization defines the boundary attaching map.

Theorem 1.7 (The attaching square commutes).

Lean statement: D5/S3/Geometry/FiniteSimplicialCellInduction.costarAttachingMap_inclusion

Proof. Machine-checked in Lean as D5/S3/Geometry/FiniteSimplicialCellInduction.costarAttachingMap_inclusion (✓ std3). ∎

Citation. The DifferentialGeometry contributors (2026). Maximal simplicial cells and finite cell induction. URL: https://github.com/qinz1yang/differential-geometry/tree/afc0a69081be678c24cb55c5111236af329bfda1.

Commentary.

For every nondegenerate simplex s, composing the attaching map with the inclusion of the costar equals composing the inclusion of the standard boundary with the characteristic simplex map.

Theorem 1.8 (The boundary intersection is a pullback).

Lean statement: D5/S3/Geometry/FiniteSimplicialCellInduction.costar_cell_isPullback

Proof. Machine-checked in Lean as D5/S3/Geometry/FiniteSimplicialCellInduction.costar_cell_isPullback (✓ std3). ∎

Citation. The DifferentialGeometry contributors (2026). Maximal simplicial cells and finite cell induction. URL: https://github.com/qinz1yang/differential-geometry/tree/afc0a69081be678c24cb55c5111236af329bfda1.

Commentary.

For every nondegenerate simplex s, the attaching map to the costar and the inclusion into the standard simplex, together with their respective maps to X, form a pullback square in simplicial sets.

Theorem 1.9 (A maximal cell gives a pushout decomposition).

Lean statement: D5/S3/Geometry/FiniteSimplicialCellInduction.costar_cell_isPushout

Proof. Machine-checked in Lean as D5/S3/Geometry/FiniteSimplicialCellInduction.costar_cell_isPushout (✓ std3). ∎

Citation. The DifferentialGeometry contributors (2026). Maximal simplicial cells and finite cell induction. URL: https://github.com/qinz1yang/differential-geometry/tree/afc0a69081be678c24cb55c5111236af329bfda1.

Commentary.

If a nondegenerate simplex s of X is maximal, the standard boundary inclusion and its attaching map into the costar, followed by the characteristic map and the costar inclusion into X, form a pushout square. The proof checks the square degree by degree using the boundary pullback, the covering equality, and injectivity off the boundary.

Definition 1.10 (Nondegenerate simplices of the costar).

Lean statement: D5/S3/Geometry/FiniteSimplicialCellInduction.costarNondegenerateEquiv

Formalization. D5/S3/Geometry/FiniteSimplicialCellInduction.costarNondegenerateEquiv (✓ std3).

Citation. The DifferentialGeometry contributors (2026). Maximal simplicial cells and finite cell induction. URL: https://github.com/qinz1yang/differential-geometry/tree/afc0a69081be678c24cb55c5111236af329bfda1.

Commentary.

For every nondegenerate simplex s of X, the nondegenerate simplices of its costar are equivalent to the nondegenerate simplices t of X for which s is not below t. Both directions retain the actual simplex and its nondegeneracy proof.

Theorem 1.11 (Removing a cell strictly reduces the finite count).

Lean statement: D5/S3/Geometry/FiniteSimplicialCellInduction.card_costar_nondegenerate_lt

Proof. Machine-checked in Lean as D5/S3/Geometry/FiniteSimplicialCellInduction.card_costar_nondegenerate_lt (✓ std3). ∎

Citation. The DifferentialGeometry contributors (2026). Maximal simplicial cells and finite cell induction. URL: https://github.com/qinz1yang/differential-geometry/tree/afc0a69081be678c24cb55c5111236af329bfda1.

Commentary.

If X is a finite simplicial set and s is any nondegenerate simplex of X, the number of nondegenerate simplices in its costar is strictly less than the number in X. The inclusion is injective and misses s.

Definition 1.12 (An empty nondegenerate carrier is initial).

Lean statement: D5/S3/Geometry/FiniteSimplicialCellInduction.isInitial_of_isEmpty_nondegenerate

Formalization. D5/S3/Geometry/FiniteSimplicialCellInduction.isInitial_of_isEmpty_nondegenerate (✓ std3).

Citation. The DifferentialGeometry contributors (2026). Maximal simplicial cells and finite cell induction. URL: https://github.com/qinz1yang/differential-geometry/tree/afc0a69081be678c24cb55c5111236af329bfda1.

Commentary.

For every simplicial set X whose type of nondegenerate simplices is empty, X is initial in the category of simplicial sets. The equality of its bottom and top subcomplexes gives the initial object structure.

Theorem 1.13 (Induction by finite simplex attachment).

Lean statement: D5/S3/Geometry/FiniteSimplicialCellInduction.finite_cell_induction

Proof. Machine-checked in Lean as D5/S3/Geometry/FiniteSimplicialCellInduction.finite_cell_induction (✓ std3). ∎

Citation. The DifferentialGeometry contributors (2026). Maximal simplicial cells and finite cell induction. URL: https://github.com/qinz1yang/differential-geometry/tree/afc0a69081be678c24cb55c5111236af329bfda1.

Commentary.

Let P be a proposition on simplicial sets in any fixed universe. Assume P for every initial simplicial set. For every natural number n and simplicial sets X and Y, every attaching map g from the standard n-simplex boundary to X, characteristic map r from the standard n-simplex to Y, and map b from X to Y, assume P of Y whenever the square with the boundary inclusion, g, r and b is a pushout and both P of that boundary and P of X hold. Then P holds for every finite simplicial set. The proof first inducts on a dimension bound and then on the number of nondegenerate simplices, using a maximal cell and its costar. No regularity or injectivity of boundary attaching maps is assumed.

References