Foundation Singular Subdivision T Op Chain Homotopy Zero

The zero-degree chain homotopy

In algebraic topology, a chain complex is a sequence of abelian groups connected by boundary maps that square to zero. The Recognition Science framework's machine-checked library of formal theorems builds such complexes for topological spaces, and one of its central constructions is the subdivision operator sdOp, which refines a space's simplicial structure by subdividing each simplex into smaller pieces. A related operator tOp plays the role of a correction term in the subdivision process. The theorem tOp_chain_homotopy_zero states that at dimension zero, the composition of tOp with the boundary map equals the identity map minus the subdivision operator.

Concretely, the statement reads: tOp X 0 ∘ bnd X 0 = 1 (Cgrp X 0) - sdOp X 0. Here X is a topological space, 0 is the lowest dimension (points), bnd is the boundary map, and Cgrp X 0 is the group of zero-dimensional chains. The equality says that applying the boundary after tOp gives the same result as taking the identity and subtracting the subdivision operator. This is a formal theorem, proved in the library with no unproved assumptions beyond the standard axioms of the underlying type theory.

The theorem is the base case of a family of results. The companion theorem tOp_chain_homotopy_succ extends the pattern to higher dimensions, showing that a similar identity holds for every dimension n. Together they establish that tOp is a chain homotopy between the identity and the subdivision operator, a standard tool in algebraic topology used to show that subdivision does not change homology groups. The zero-dimensional case is the simplest instance, but it is the one that anchors the induction.

In Recognition Science, this result supports the framework's treatment of topological spaces as combinatorial objects. The framework models spaces through their singular chains and uses subdivision to relate different resolutions of the same space. The theorem does not claim that tOp is an isomorphism, nor that it commutes with boundary maps in the naive sense. It only asserts the specific equality at dimension zero, which is a stepping stone for the full chain homotopy statement. The framework's broader claims about space and dimension rest on later theorems, not on this single lemma.

/-- 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]

/-- 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]

/-- 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

What this page does not claim

The theorem does not claim that tOp is an isomorphism or that it commutes with boundary maps in the naive sense. The theorem does not by itself establish any claim about the number of spatial dimensions. The theorem does not claim that subdivision preserves homology groups; that would require the full 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: