Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Derived Adjunction

Abstract

Supporting results for the unbounded derived adjunction. These do not assume existence of derived solidification or import the upstream derived gaps.

Theorem 1.1 (map is KProjective of exact right Adjoint).

Lean statement: D5/S3/HomologicalAlgebra/Solid/DerivedAdjunction.map_isKProjective_of_exact_rightAdjoint

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

Source. Repository-derived.

Commentary.

The left adjoint of an exact additive functor sends unbounded K-projective complexes to K-projective complexes.

Theorem 1.2 (reflection map is KProjective).

Lean statement: D5/S3/HomologicalAlgebra/Solid/DerivedAdjunction.reflection_map_isKProjective

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

Source. Repository-derived.

Commentary.

The actual protected reflector preserves K-projectivity. This result asserts no existence of replacements for general light condensed complexes.

References