Constructing colimits from finite colimits and filtered colimits #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We construct colimits of size w
from finite colimits and filtered colimits of size w
. Since
w
-sized colimits are constructured from coequalizers and w
-sized coproducts, it suffices to
construct w
-sized coproducts from finite coproducts and w
-sized filtered colimits.
The idea is simple: to construct coproducts of shape α
, we take the colimit of the filtered
diagram of all coproducts of finite subsets of α
.
We also deduce the dual statement by invoking the original statement in Cᵒᵖ
.
If C
has finite coproducts, a functor discrete α ⥤ C
lifts to a functor
finset (discrete α) ⥤ C
by taking coproducts.
Equations
- category_theory.limits.coproducts_from_finite_filtered.lift_to_finset F = {obj := λ (s : finset (category_theory.discrete α)), ∐ λ (x : ↥s), F.obj ↑x, map := λ (s t : finset (category_theory.discrete α)) (h : s ⟶ t), category_theory.limits.sigma.desc (λ (y : ↥s), category_theory.limits.sigma.ι (λ (x : ↥t), F.obj ↑x) ⟨↑y, _⟩), map_id' := _, map_comp' := _}
If C
has finite coproducts and filtered colimits, we can construct arbitrary coproducts by
taking the colimit of the diagram formed by the coproducts of finite sets over the indexing
type.
Equations
- category_theory.limits.coproducts_from_finite_filtered.lift_to_finset_colimit_cocone F = {cocone := {X := category_theory.limits.colimit (category_theory.limits.coproducts_from_finite_filtered.lift_to_finset F) _, ι := category_theory.discrete.nat_trans (λ (j : category_theory.discrete α), category_theory.limits.sigma.ι (λ (x : ↥{j}), F.obj ↑x) ⟨j, _⟩ ≫ category_theory.limits.colimit.ι (category_theory.limits.coproducts_from_finite_filtered.lift_to_finset F) {j})}, is_colimit := {desc := λ (s : category_theory.limits.cocone F), category_theory.limits.colimit.desc (category_theory.limits.coproducts_from_finite_filtered.lift_to_finset F) {X := s.X, ι := {app := λ (t : finset (category_theory.discrete α)), category_theory.limits.sigma.desc (λ (x : ↥t), s.ι.app ↑x), naturality' := _}}, fac' := _, uniq' := _}}