Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Colimits

Abstract

Preservation of coproducts from finite coproducts and filtered colimits This file adds a preservation counterpart to mathlib’s construction of coproducts from finite coproducts and filtered colimits.

Theorem 1.1 (preserves Colimits Of Shape discrete of preserves Finite Coproducts and filtered Colimits).

Lean statement: D5/S3/HomologicalAlgebra/Solid/Colimits.preservesColimitsOfShape_discrete_of_preservesFiniteCoproducts_and_filteredColimits

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

Source. Repository-derived.

Commentary.

A functor preserving finite coproducts and filtered colimits preserves coproducts.

Theorem 1.2 (is Solid coproduct).

Lean statement: D5/S3/HomologicalAlgebra/Solid/Colimits.isSolid_coproduct

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

Source. Repository-derived.

Commentary.

Any small coproduct of solid objects is solid.

References

  • Truth anchor: D5/S3/HomologicalAlgebra/Solid/Colimits.isSolid_coproduct
  • Truth anchor: D5/S3/HomologicalAlgebra/Solid/Colimits.preservesColimitsOfShape_discrete_of_preservesFiniteCoproducts_and_filteredColimits
  • Dependency: D5/S3/HomologicalAlgebra/Solid/Reflection