Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Localization Defect

Abstract

The exact unbounded locality test for the protected solidification reflector. This constructs the actual two-term defect, not a replacement hypothesis. Its vanishing detects solid homology in every integer degree. A universal local replacement and its comparison with DerivedCategory Solid remain separate mathematical obligations.

Theorem 1.1 (is Zero solid Complex Defect iff).

Lean statement: D5/S3/HomologicalAlgebra/Solid/LocalizationDefect.isZero_solidComplexDefect_iff

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

Source. Repository-derived.

Commentary.

The defect vanishes in the derived category precisely for complexes whose homology is solid; no bound on degrees is imposed.

Theorem 1.2 (is Iso solid Derived Endomorphism Q iff).

Lean statement: D5/S3/HomologicalAlgebra/Solid/LocalizationDefect.isIso_solidDerivedEndomorphism_Q_iff

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

Source. Repository-derived.

Commentary.

The derived natural transformation on the localization of any complex has the same exact all-degree locality criterion.

References