Filtered

Abstract

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

Theorem 1.1 (preserves Filtered Colimits ihom P of pointwise hom).

Lean statement: D5/S3/HomologicalAlgebra/Solid/Filtered.preservesFilteredColimits_ihom_P_of_pointwise_hom

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

Source. Repository-derived.

Commentary.

Reduction from pointwise ordinary hom preservation to internal hom preservation.

Theorem 1.2 (preserves Filtered Colimits ihom P scaffold).

Lean statement: D5/S3/HomologicalAlgebra/Solid/Filtered.preservesFilteredColimits_ihom_P_scaffold

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

Source. Repository-derived.

Commentary.

Final scaffold for the target lemma in LightSolid.lean.

References

• Truth anchor: D5/S3/HomologicalAlgebra/Solid/Filtered.preservesFilteredColimits_ihom_P_of_pointwise_hom
• Truth anchor: D5/S3/HomologicalAlgebra/Solid/Filtered.preservesFilteredColimits_ihom_P_scaffold
• Dependency: D5/S3/HomologicalAlgebra/Solid/Definitions