module module moderate

`IndisputableMonolith.Foundation.SingularSubdivision`

Defines the free abelian group of affine n-chains on a set α, together with the affine boundary, cone, and elementary subdivision operators needed for singular homology. Algebraic topologists working the RS foundation cite it when building Mayer–Vietoris sequences or computing sphere homology. The module is largely definitional: it packages Mathlib singular-simplex data with explicit affine maps and verifies the usual chain-homotopy identities by direct Fin-arithmetic.

claimFor a set $\alpha$ and $n\in\mathbb{N}$, let $AC_n(\alpha)$ be the free abelian group on maps $\mathrm{Fin}(n+1)\to\alpha$ (affine $n$-simplices). The module supplies the affine boundary $\partial:AC_n\to AC_{n-1}$, the cone operator from a basepoint, and the elementary subdivision operator $\varepsilon$, satisfying the standard identities $\partial\circ\mathrm{cone}+\mathrm{cone}\circ\partial=\mathrm{id}$ and $\partial\varepsilon=\varepsilon\partial$.

background

Singular homology in Mathlib is built from continuous maps out of the standard simplex. For Recognition Science foundation work one often needs a purely combinatorial intermediate: affine chains whose vertices lie in an arbitrary set $\alpha$ (typically a convex subset of a real vector space). The group $AC_n(\alpha)$ is the free $\mathbb{Z}$-module on all functions $\mathrm{Fin}(n+1)\to\alpha$.

The upstream module SingularPrism supplies the prism operator that realises the chain homotopy between the identity and a subdivision. The present module specialises that apparatus to the affine setting: it defines the affine simplex constructor, the induced boundary $\partial$, the cone from a fixed vertex, and the elementary subdivision map $\varepsilon$ that inserts barycentres.

Local conventions follow Mathlib's SingularHomology.Basic: chains are finitely supported, coefficients are $\mathbb{Z}$, and face maps are realised by precomposition with the standard coface embeddings $\mathrm{succAbove}$.

proof idea

This is primarily a definition module. The core objects (AC, asimplex, abnd, acone, eps) are introduced by direct constructors. The few lemmas (cons_comp_succAbove_*, abnd_comp_acone, and the corresponding statements for eps) are proved by unfolding the Fin-arithmetic of face and degeneracy maps and applying the corresponding identities already available from SingularPrism and Mathlib's simplex category. No deep homological algebra is required; the arguments are equational.

why it matters in Recognition Science

Affine subdivision is the technical engine that lets the foundation compute singular homology of spheres and run Mayer–Vietoris arguments without leaving the combinatorial category. Downstream, SingularMayerVietoris imports the cone and subdivision operators to obtain the long exact sequence of a pair, while SingularSphere uses the same operators to identify $H_n(S^n)$ with $\mathbb{Z}$. In the broader RS forcing chain these homology computations underwrite topological constraints (dimension, orientability) that feed the T8 derivation of $D=3$ spatial dimensions and the eight-tick octave structure.

scope and limits

Does not construct continuous singular chains; only affine combinatorial chains on a set.
Does not prove the full Eilenberg–Steenrod axioms; only supplies operators used by later modules.
Does not identify AC with Mathlib's singular chain complex; that comparison lives elsewhere.
Does not treat infinite or locally finite chains; support remains finite.
Does not address coefficients other than $\mathbb{Z}$.

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Foundation.SingularMayerVietoris module_import
IndisputableMonolith.Foundation.SingularSphere module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.SingularPrism module_import

declarations in this module (114)

abbrev AC L93
def asimplex L96
lemma lift_asimplex L109
def abnd L116
lemma abnd_asimplex L122
def acone L129
lemma acone_asimplex L133
def eps L138
lemma eps_asimplex L141
lemma cons_comp_succAbove_zero L147
lemma cons_comp_succAbove_succ L153
theorem abnd_comp_acone L164
theorem abnd_comp_acone_zero L179
theorem abnd_comp_abnd L201
theorem eps_comp_abnd L285
def asub L301
lemma asub_zero L308
lemma asub_asimplex L311
theorem abnd_comp_asub L318
def atee L353
lemma atee_zero L360
lemma atee_asimplex L363
theorem abnd_comp_atee_zero L371
theorem abnd_comp_atee L377
def asubIter L415
lemma asubIter_zero L421
lemma asubIter_succ L424
theorem abnd_comp_asubIter L428
def ateeIter L440
lemma ateeIter_zero L446
lemma ateeIter_succ L449
lemma asubIter_comp_asub L454
theorem abnd_comp_ateeIter L463
def amap L506
lemma amap_asimplex L509
lemma amap_comp_abnd L514
lemma amap_comp_acone L524
theorem amap_comp_asub L538
theorem amap_comp_atee L564
def affineMapFun L602
lemma affineMapFun_mem L606
lemma continuous_affineMapFun L622
def affineMap L630
lemma affineMap_apply_coe L635
lemma affineMap_vertex L640
theorem affineMap_comp L656
def idTuple L667
lemma affineMap_idTuple L671
lemma affineMap_comp_idTuple L686
lemma stdSimplex_map_eq_affineMap L692
lemma affineMap_comp_face L709
def sbary L723
lemma sbary_apply L741
lemma sbary_affineMap L747
def postComp L776
def simplexEquiv L785
lemma simplexEquiv_ L790
lemma simplexEquiv_map L796
def pushSimplex L803
lemma simplexEquiv_pushSimplex L807
def toChain L814
lemma toChain_asimplex L818
lemma pushSimplex_idTuple L833
lemma toChain_asimplex_idTuple L838
lemma toChain_comp_abnd L853
lemma toChain_comp_chainMap L863
lemma toChain_amap L875
def baryFn L888
def sdGen L893
def sdOp L898
lemma gen_sdOp L901
def tGen L905
def tOp L910
lemma gen_tOp L913
lemma gen_pushSimplex_comp_sdOp L918
lemma gen_pushSimplex_comp_tOp L936
theorem sdOp_comp_bnd L954
theorem sdOp_zero L978
theorem tOp_zero L988
theorem tOp_chain_homotopy_succ L998

… and 34 more