Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Singular Solid

Abstract

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

Theorem 1.1 (singular Chain Group is Solid).

Lean statement: D5/S3/HomologicalAlgebra/Solid/SingularSolid.singularChainGroup_isSolid

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

Source. Repository-derived.

Commentary.

Discrete integral singular chain groups are solid in every homological degree, for every topological space.

Theorem 1.2 (singular Chains Complex is Solid).

Lean statement: D5/S3/HomologicalAlgebra/Solid/SingularSolid.singularChainsComplex_isSolid

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

Source. Repository-derived.

Commentary.

Every term of the exact protected reindexed singular-chain complex is solid.

References