Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Reflection

Abstract

This module supplies the indicated step in the unbounded solidification construction.

Theorem 1.1 (is Solid iff is Local).

Lean statement: D5/S3/HomologicalAlgebra/Solid/Reflection.isSolid_iff_isLocal

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. This module supplies the indicated step in the unbounded solidification construction.

Theorem 1.2 (reflection right Adjoint).

Lean statement: D5/S3/HomologicalAlgebra/Solid/Reflection.reflection_rightAdjoint

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

Source. Repository-derived.

Commentary.

Orthogonal reflection applies because the generating maps have finitely presentable domains and codomains.

References

  • Truth anchor: D5/S3/HomologicalAlgebra/Solid/Reflection.isSolid_iff_isLocal
  • Truth anchor: D5/S3/HomologicalAlgebra/Solid/Reflection.reflection_rightAdjoint
  • Dependency: D5/S3/HomologicalAlgebra/Solid/Filtered