Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Derived Realization

Abstract

Copyright (c) 2026. Released under the Apache 2.0 license. Realization in the protected D(Solid) of every object of the actual derived-local category. The concrete free-generator kernel resolution, finite layers, lower telescope and good upper telescope supply the unbounded essential-image argument. Neither solid homology nor the ordinary reflection is treated as a realization theorem. Research: Juan Esteban Rodríguez Camargo, Notes on Solid Geometry, Theorem 3.3.1 and Lemma 3.3.2.

Theorem 1.1 (derived Local Reflection realized complex).

Lean statement: D5/S3/HomologicalAlgebra/Solid/DerivedRealization.derivedLocalReflection_realized_complex

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

Source. Repository-derived.

Commentary.

Every arbitrary unbounded ambient complex has its actual derived-local reflection in the essential image of the protected derived inclusion.

Theorem 1.2 (derived Inclusion To Local ess Surj).

Lean statement: D5/S3/HomologicalAlgebra/Solid/DerivedRealization.derivedInclusionToLocal_essSurj

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

Source. Repository-derived.

Commentary.

The actual unbounded realization theorem, with no generation, full-faithfulness or realization premise.

Definition 1.3 (derived Solid Local Equivalence).

Lean statement: D5/S3/HomologicalAlgebra/Solid/DerivedRealization.derivedSolidLocalEquivalence

Formalization. D5/S3/HomologicalAlgebra/Solid/DerivedRealization.derivedSolidLocalEquivalence (✓ std3).

Source. Repository-derived.

Commentary.

The genuine equivalence preserves the exact protected inclusion.

References