Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Adjunction Kan Extension

Abstract

The total left derived universal property from the actual derived adjunction The only additional premise is an actual adjunction to the protected exact derived inclusion. The geometric construction of that adjunction is separate. All complexes here are unbounded cochain complexes, and the localization is at every quasi-isomorphism.

Theorem 1.1 (adjunction is Left Derived Functor).

Lean statement: D5/S3/HomologicalAlgebra/Solid/AdjunctionKanExtension.adjunction_isLeftDerivedFunctor

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

Source. Repository-derived.

Commentary.

The literal Mathlib property for all quasi-isomorphisms of unbounded complexes.

Theorem 1.2 (adjunction has Left Derived Functor).

Lean statement: D5/S3/HomologicalAlgebra/Solid/AdjunctionKanExtension.adjunction_hasLeftDerivedFunctor

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

Source. Repository-derived.

Commentary.

Existence obtained from the constructed witness using Mathlib’s mk'.

References