Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Projective Hom Compatibility

Abstract

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

Theorem 1.1 (exact Derived Homology single).

Lean statement: D5/S3/HomologicalAlgebra/Solid/ProjectiveHomCompatibility.exactDerivedHomology_single

Proof. Machine-checked in Lean as D5/S3/HomologicalAlgebra/Solid/ProjectiveHomCompatibility.exactDerivedHomology_single (✓ 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.

Theorem 1.2 (derived Single Homology Map exact).

Lean statement: D5/S3/HomologicalAlgebra/Solid/ProjectiveHomCompatibility.derivedSingleHomologyMap_exact

Proof. Machine-checked in Lean as D5/S3/HomologicalAlgebra/Solid/ProjectiveHomCompatibility.derivedSingleHomologyMap_exact (✓ 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.

References