Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Derived Cell Attachment

Abstract

The simultaneous, arbitrary-size actual cell attachments tested in the unbounded derived category. New proofs, released under Apache 2.0.

Theorem 1.1 (solid Cells Attachment derived Precomp bijective).

Lean statement: D5/S3/HomologicalAlgebra/Solid/DerivedCellAttachment.solidCellsAttachment_derivedPrecomp_bijective

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

Source. Repository-derived.

Commentary.

Simultaneous attachment of an arbitrary family of the protected cells has a universal derived comparison to each derived-local target.

Theorem 1.2 (solid Cellular Step derived Precomp bijective).

Lean statement: D5/S3/HomologicalAlgebra/Solid/DerivedCellAttachment.solidCellularStep_derivedPrecomp_bijective

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

Source. Repository-derived.

Commentary.

The actual saved attachment step, along all maps from all defining cells, has the proved universal derived comparison.

References