Foundation Singular Subdivision T Op Iter Chain Homotopy Succ

A homotopy between subdivision and identity

In algebraic topology, a chain complex is a sequence of abelian groups connected by boundary maps that square to zero. The groups record formal sums of simplices, the basic building blocks of a space; the boundary map sends each simplex to its faces. A chain map between two such complexes is a collection of group homomorphisms that commute with the boundary maps. A chain homotopy between two chain maps is a formal algebraic relation: it says that the two maps, while not equal, differ by a boundary in a way that leaves all homology groups, the invariants that count holes, unchanged.

The classical setting is the singular chain complex of a topological space. For each dimension n, the group Cgrp X n consists of finite formal sums of continuous maps from the standard n-simplex into the space X. The boundary map bnd X n sends each singular simplex to the alternating sum of its faces. Two fundamental operations on this complex are the identity map and the subdivision map sdOp X n, which replaces each simplex by a finer triangulation using barycenters. A third operation, tOp X n, is a chain map that raises dimension by one and is built from the same subdivision data.

The theorem tOp_chain_homotopy_succ states a precise algebraic identity for each dimension n: composing the boundary map with tOp in one order, plus composing tOp with the boundary in the other order, equals the identity minus the subdivision map. In symbols: bnd X n ∘ tOp X n + tOp X (n+1) ∘ bnd X (n+1) = id − sdOp X (n+1). This is exactly the defining equation of a chain homotopy between the identity map and the subdivision map, in dimension n+1. The companion theorem tOp_chain_homotopy_zero establishes the same relation in dimension zero, where it reduces to a simpler identity.

In Recognition Science, this theorem is part of a machine-checked library of formal theorems. The library is a collection of proofs verified by a computer kernel, and this particular result is one link in a chain that the framework uses to build its account of space. The framework models space through such algebraic structures, and the theorem provides a formal guarantee that subdivision, a process of cutting simplices into smaller pieces, is homotopically equivalent to doing nothing. That equivalence is what lets the framework treat subdivision as a harmless operation when studying the large-scale shape of a space.

The theorem does not claim that subdivision equals the identity map on the nose; the two differ by a boundary, which is a weaker and more useful statement. It also does not claim anything about the actual geometry of the space X, since the result holds for every topological space. Finally, it does not assert that the identity and subdivision maps are homotopic in the topological sense of continuous deformations; the homotopy here is purely algebraic, at the level of chain complexes.

/-- The chain homotopy identity in positive degrees:
`∂ ∘ T + T ∘ ∂ = id − S` on the degree-`(n+1)` singular chain group. -/
theorem tOp_chain_homotopy_succ (X : TopCat.{0}) (n : ℕ) :
    bnd X n ≫ tOp X n + tOp X (n + 1) ≫ bnd X (n + 1) =
      𝟙 (Cgrp X (n + 1)) - sdOp X (n + 1) := by
  apply Sigma.hom_ext
  intro s
  rw [Preadditive.comp_add, Preadditive.comp_sub, Category.comp_id]
  -- second summand: `T ∘ ∂` transported to `toChain σ (T (∂ id))`
  have h2 : gen X (n + 1) s ≫ (bnd X n ≫ tOp X n) =
      toChain (simplexEquiv X (n + 1) s) (n + 1)
        (atee (baryFn (n + 1)) n (abnd n (asimplex (idTuple (n + 1))))) := by
    rw [← Category.assoc, gen_d, Preadditive.sum_comp, abnd_asimplex, map_sum,
      map_sum]
    refine Finset.sum_congr rfl fun k _ => ?_
    rw [Preadditive.zsmul_comp, map_smul, map_smul]
    congr 1
    rw [δ_eq_pushSimplex, gen_pushSimplex_comp_tOp]
  -- first summand: `∂ ∘ T` transported to `toChain σ (∂ (T id))`
  have h1 : gen X (n + 1) s ≫ (tOp X (n + 1) ≫ bnd X (n + 1)) =
      toChain (simplexEquiv X (n + 1) s) (n + 1)
        (abnd (n + 1) (atee (baryFn (n + 1)) (n + 1) (asimplex (idTuple (n + 1))))) := by
    rw [← Category.assoc, gen_tOp]
    have h := LinearMap.congr_fun
      (toChain_comp_abnd (simplexEquiv X (n + 1) s) (n + 1))
      (atee (baryFn (n + 1)) (n + 1) (asimplex (idTuple (n + 1))))
    rw [LinearMap.comp_apply, LinearMap.comp_apply] at h
    exact h
  rw [h2, h1, ← map_add, gen_sdOp]
  have hhom := LinearMap.congr_fun (abnd_comp_atee (baryFn (n + 1)) n)
    (asimplex (idTuple (n + 1)))
  simp only [LinearMap.add_apply, LinearMap.comp_apply, LinearMap.sub_apply,
    LinearMap.id_apply] at hhom
  have hsum : atee (baryFn (n + 1)) n (abnd n (asimplex (idTuple (n + 1)))) +
      abnd (n + 1) (atee (baryFn (n + 1)) (n + 1) (asimplex (idTuple (n + 1)))) =
      asimplex (idTuple (n + 1)) -
        asub (baryFn (n + 1)) (n + 1) (asimplex (idTuple (n + 1))) := by
    exact (add_comm _ _).trans hhom
  rw [hsum, map_sub, toChain_asimplex_idTuple]
  rfl

/-- In degree `0`: `∂ ∘ T = id − S` (both sides vanish). -/
theorem tOp_chain_homotopy_zero (X : TopCat.{0}) :
    tOp X 0 ≫ bnd X 0 = 𝟙 (Cgrp X 0) - sdOp X 0 := by
  rw [tOp_zero, sdOp_zero, Limits.zero_comp, sub_self]

What this page does not claim

The theorem does not claim that subdivision equals the identity map on the nose; they differ by a boundary. The theorem does not claim anything about the geometry of a particular space, since it holds for all topological spaces. The theorem does not assert a topological homotopy between maps, only an algebraic chain homotopy.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/SingularSubdivision.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: