Foundation Circle H1 Computation Reduced Cellular To Ordinary Comp Ordinary Cell

The circle's two chain models

In algebraic topology, a circle has a single one-dimensional hole. That fact is usually written H₁(S¹; ℤ) ≅ ℤ, meaning the first homology group, the group that counts one-dimensional holes, is the integers. The Recognition Science library's homology workbench builds two small algebraic models of the circle and proves they are equivalent at the level of this hole count. The declaration named reducedCellularToOrdinary_comp_ordinaryCellularToReduced is part of that proof.

The two models are the ordinary cellular circle chain model and the reduced cellular circle chain model. The ordinary model places a copy of the integers in degree 0 and another in degree 1, with all boundary maps equal to zero. The reduced model places a single copy of the integers in degree 1 and nothing in degree 0. The declaration proves that composing the map from the reduced model to the ordinary model with the map from the ordinary model back to the reduced model gives the identity map on the degree-1 object. This is the algebraic core of showing the two models have the same first homology, both isomorphic to the integers.

This equivalence is a theorem in the machine-checked library of formal theorems, not a paper derivation. The relevant declaration is ordinaryCellularToReduced_comp_reducedCellularToOrdinary_f_one, which states that the composite map at degree 1 equals the identity. A companion theorem, ordinaryCellularToReducedChainMap_quasiIsoAt_one, states that the map from the ordinary to the reduced model induces an isomorphism on first homology. Together they establish that the two chain models are interchangeable for the purpose of computing H₁.

The declaration does not claim that either model is the actual singular homology of the geometric circle. The workbench docstring is explicit: it does not replace TopCat.sphere 1 and does not feed the strict T8 bridge until a real equivalence to Mathlib's imported singular homology object is proved. The bridge, circleH1GeometricBridge, is a separate proposition that remains open. The algebraic equivalence is a necessary ingredient, not the final topological transport.

What this means for the reader is that the framework has a solid algebraic foundation for the circle's first homology, but the connection to the standard geometric object is still a target. The two chain models are proven interchangeable, and each is proven to have first homology the integers. The step from these algebraic models to the topological sphere is the missing piece, and it is named explicitly as open.

/-- The other composite need not be the identity on the ordinary two-cell
complex, because the ordinary model has an additional degree-`0` generator.
It is, however, the identity in degree `1`, the degree relevant to the circle
homology computation. -/
theorem ordinaryCellularToReduced_comp_reducedCellularToOrdinary_f_one :
    (ordinaryCellularToReducedChainMap ≫ reducedCellularToOrdinaryChainMap).f 1 =
      𝟙 (ordinaryCellularCircleChainModel.X 1) := by
  simp [ordinaryCellularToReducedChainMap_f_one,
    reducedCellularToOrdinaryChainMap_f_one]

/-- The collapse from the ordinary two-cell cellular circle model to the reduced
degree-`1` model is a quasi-isomorphism in degree `1`.

The proof uses Mathlib's zero-differential short-complex criterion: in degree
`1`, both relevant short complexes have zero differentials, and the middle
component of the collapse map is an isomorphism on the chosen integer
generator. -/
theorem ordinaryCellularToReducedChainMap_quasiIsoAt_one :
    QuasiIsoAt ordinaryCellularToReducedChainMap 1 := by
  rw [quasiIsoAt_iff]
  rw [ShortComplex.quasiIso_iff_isIso_liftCycles _ (by
    simp [ordinaryCellularCircleChainModel_d_eq_zero]) (by
    simp [ordinaryCellularCircleChainModel_d_eq_zero]) (by
    simp)]
  let S₂ :=
    (HomologicalComplex.shortComplexFunctor (ModuleCat ℤ) (ComplexShape.down ℕ) 1).obj
      reducedCellularCircleChainModel
  let φ :=
    ((HomologicalComplex.shortComplexFunctor (ModuleCat ℤ) (ComplexShape.down ℕ) 1).map
      ordinaryCellularToReducedChainMap)
  let w : φ.τ₂ ≫ S₂.g = 0 := by
    dsimp [S₂, φ]
    simp
  change IsIso (S₂.liftCycles φ.τ₂ w)
  haveI : IsIso S₂.iCycles := S₂.isIso_iCycles (by
    dsimp [S₂])
  haveI : IsIso (S₂.liftCycles φ.τ₂ w ≫ S₂.iCycles) := by
    rw [ShortComplex.liftCycles_i]
    dsimp [S₂, φ]
    rw [ordinaryCellularToReducedChainMap_f_one]
    infer_instance
  exact IsIso.of_isIso_comp_right (S₂.liftCycles φ.τ₂ w) S₂.iCycles

/-- Proposition-facing form of
`reducedCellularCircleChainModelH1IsoInt`. -/
theorem reducedCellularCircleChainModelH1NonemptyIsoInt :
    Nonempty (reducedCellularCircleChainModel.homology 1 ≅ ModuleCat.of ℤ ℤ) :=
  ⟨reducedCellularCircleChainModelH1IsoInt⟩

What this page does not claim

The declaration does not claim that either chain model is the singular homology of the topological circle. The declaration does not claim that the geometric bridge to TopCat.sphere 1 has been proved. The declaration does not claim any result about higher homology groups of the circle.

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/CircleH1Computation.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: