Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Singular Projective

Abstract

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

Theorem 1.1 (singular Chains Qh map bijective).

Lean statement: D5/S3/HomologicalAlgebra/Solid/Supplier/SingularProjective.singularChains_Qh_map_bijective

Proof. Machine-checked in Lean as D5/S3/HomologicalAlgebra/Solid/Supplier/SingularProjective.singularChains_Qh_map_bijective (✓ std3). ∎

Source. Repository-derived.

Commentary.

Morphisms from protected singular chains into any derived object represented in the homotopy category are precisely homotopy classes of chain maps.

References