Chain Homology

Abstract

This module supplies the indicated step in the unbounded solidification construction.

Theorem 1.1 (discrete Ab preserves Finite Colimits).

Lean statement: D5/S3/HomologicalAlgebra/Solid/ChainHomology.discreteAb_preservesFiniteColimits

Proof. Machine-checked in Lean as D5/S3/HomologicalAlgebra/Solid/ChainHomology.discreteAb_preservesFiniteColimits (✓ std3). ∎

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. This module supplies the indicated step in the unbounded solidification construction.

Definition 1.2 (singular Chains Derived Homology Iso).

Lean statement: D5/S3/HomologicalAlgebra/Solid/ChainHomology.singularChainsDerivedHomologyIso

Formalization. D5/S3/HomologicalAlgebra/Solid/ChainHomology.singularChainsDerivedHomologyIso (✓ std3).

Source. Repository-derived.

Commentary.

Reindexing the discrete integral singular chains computes the protected homology object in every degree -n. No CW comparison is assumed or used here.

References

• Truth anchor: D5/S3/HomologicalAlgebra/Solid/ChainHomology.discreteAb_preservesFiniteColimits
• Truth anchor: D5/S3/HomologicalAlgebra/Solid/ChainHomology.singularChainsDerivedHomologyIso
• Dependency: D5/S3/HomologicalAlgebra/Solid/Definitions