Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Realized Adjunction

Abstract

Copyright (c) 2026. Released under the Apache 2.0 license. The genuine unbounded adjunction into the protected D(Solid), obtained from the proved realization equivalence and the actual local reflector. The right adjoint is exactly the protected derivedInclusion.

Definition 1.1 (realized Derived Solidification).

Lean statement: D5/S3/HomologicalAlgebra/Solid/RealizedAdjunction.realizedDerivedSolidification

Formalization. D5/S3/HomologicalAlgebra/Solid/RealizedAdjunction.realizedDerivedSolidification (✓ std3).

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. Copyright (c) 2026. Released under the Apache 2.0 license. The genuine unbounded adjunction into the protected D(Solid), obtained from the proved realization equivalence and the actual local reflector. The right adjoint is exactly the protected derivedInclusion.

Definition 1.2 (realized Derived Solidification Adjunction).

Lean statement: D5/S3/HomologicalAlgebra/Solid/RealizedAdjunction.realizedDerivedSolidificationAdjunction

Formalization. D5/S3/HomologicalAlgebra/Solid/RealizedAdjunction.realizedDerivedSolidificationAdjunction (✓ std3).

Source. Repository-derived.

Commentary.

The actual adjunction has no existence, realization or full-faithfulness premise. Its equivalence is constructed by the unbounded resolution proof.

References

  • Truth anchor: D5/S3/HomologicalAlgebra/Solid/RealizedAdjunction.realizedDerivedSolidification
  • Truth anchor: D5/S3/HomologicalAlgebra/Solid/RealizedAdjunction.realizedDerivedSolidificationAdjunction
  • Dependency: D5/S3/HomologicalAlgebra/Solid/DerivedRealization