Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Derived Local Reflection

Abstract

A genuine reflector on the actual unbounded derived category onto its full subcategory of protected derived-local objects. This subcategory has not been identified with DerivedCategory Solid. In particular this file does not declare the protected total-left-derived functor. New proofs, released under the Apache 2.0 license.

Theorem 1.1 (solid Derived Local Degreewise Comparison unit).

Lean statement: D5/S3/HomologicalAlgebra/Solid/DerivedLocalReflection.solidDerivedLocalDegreewiseComparison_unit

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

Source. Repository-derived.

Commentary.

The natural comparison factors the exact original degreewise unit.

Theorem 1.2 (solid Cellular Colimit derived Precomp bijective).

Lean statement: D5/S3/HomologicalAlgebra/Solid/DerivedLocalReflection.solidCellularColimit_derivedPrecomp_bijective

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

Source. Repository-derived.

Commentary.

The actual cellular colimit, not only the telescope, has the full derived universal comparison against all protected derived-local targets.

References

  • Truth anchor: D5/S3/HomologicalAlgebra/Solid/DerivedLocalReflection.solidCellularColimit_derivedPrecomp_bijective
  • Truth anchor: D5/S3/HomologicalAlgebra/Solid/DerivedLocalReflection.solidDerivedLocalDegreewiseComparison_unit
  • Dependency: D5/S3/HomologicalAlgebra/Solid/TelescopeEquivalence