Constructing colimits from finite colimits and filtered colimits

We construct colimits of size w from finite colimits and filtered colimits of size w. Since w-sized colimits are constructed 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ᵒᵖ.

noncomputable def CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj {C : Type u} [Category.{v, u} C] {α : Type w} [HasFiniteCoproducts C] (F : Functor (Discrete α) C) : Functor (Finset (Discrete α)) C

If C has finite coproducts, a functor Discrete α ⥤ C lifts to a functor Finset (Discrete α) ⥤ C by taking coproducts.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj_map {C : Type u} [Category.{v, u} C] {α : Type w} [HasFiniteCoproducts C] (F : Functor (Discrete α) C) {x✝ Y : Finset (Discrete α)} (h : x✝ ⟶ Y) : (liftToFinsetObj F).map h = Sigma.desc fun (y : ↥x✝) => Sigma.ι (fun (x : ↥Y) => F.obj ↑x) ⟨↑y, ⋯⟩

@[simp]

theorem CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj_obj {C : Type u} [Category.{v, u} C] {α : Type w} [HasFiniteCoproducts C] (F : Functor (Discrete α) C) (s : Finset (Discrete α)) : (liftToFinsetObj F).obj s = ∐ fun (x : ↥s) => F.obj ↑x

noncomputable def CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone {C : Type u} [Category.{v, u} C] {α : Type w} [HasFiniteCoproducts C] [HasColimitsOfShape (Finset (Discrete α)) C] (F : Functor (Discrete α) C) : ColimitCocone F

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

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone_cocone_ι_app {C : Type u} [Category.{v, u} C] {α : Type w} [HasFiniteCoproducts C] [HasColimitsOfShape (Finset (Discrete α)) C] (F : Functor (Discrete α) C) (j : Discrete α) : (liftToFinsetColimitCocone F).cocone.ι.app j = CategoryStruct.comp (Sigma.ι (fun (x : ↥{j}) => F.obj ↑x) ⟨j, ⋯⟩) (colimit.ι (liftToFinsetObj F) {j})

@[simp]

theorem CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone_cocone_pt {C : Type u} [Category.{v, u} C] {α : Type w} [HasFiniteCoproducts C] [HasColimitsOfShape (Finset (Discrete α)) C] (F : Functor (Discrete α) C) : (liftToFinsetColimitCocone F).cocone.pt = colimit (liftToFinsetObj F)

@[simp]

theorem CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone_isColimit_desc {C : Type u} [Category.{v, u} C] {α : Type w} [HasFiniteCoproducts C] [HasColimitsOfShape (Finset (Discrete α)) C] (F : Functor (Discrete α) C) (s : Cocone F) : (liftToFinsetColimitCocone F).isColimit.desc s = colimit.desc (liftToFinsetObj F) { pt := s.pt, ι := { app := fun (x : Finset (Discrete α)) => Sigma.desc fun (x_1 : ↥x) => s.ι.app ↑x_1, naturality := ⋯ } }

noncomputable def CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset (C : Type u) [Category.{v, u} C] (α : Type w) [HasFiniteCoproducts C] : Functor (Functor (Discrete α) C) (Functor (Finset (Discrete α)) C)

The functor taking a functor Discrete α ⥤ C to a functor Finset (Discrete α) ⥤ C by taking coproducts.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset_obj_obj (C : Type u) [Category.{v, u} C] (α : Type w) [HasFiniteCoproducts C] (F : Functor (Discrete α) C) (s : Finset (Discrete α)) : ((liftToFinset C α).obj F).obj s = ∐ fun (x : ↥s) => F.obj ↑x

@[simp]

theorem CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset_obj_map (C : Type u) [Category.{v, u} C] (α : Type w) [HasFiniteCoproducts C] (F : Functor (Discrete α) C) {x✝ Y : Finset (Discrete α)} (h : x✝ ⟶ Y) : ((liftToFinset C α).obj F).map h = Sigma.desc fun (y : ↥x✝) => Sigma.ι (fun (x : ↥Y) => F.obj ↑x) ⟨↑y, ⋯⟩

@[simp]

theorem CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset_map_app (C : Type u) [Category.{v, u} C] (α : Type w) [HasFiniteCoproducts C] {X✝ Y✝ : Functor (Discrete α) C} (β : X✝ ⟶ Y✝) (x✝ : Finset (Discrete α)) : ((liftToFinset C α).map β).app x✝ = Sigma.map fun (x : ↥x✝) => β.app ↑x

noncomputable def CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone {C : Type u} [Category.{v, u} C] {α : Type w} [HasFiniteCoproducts C] (f : α → C) [HasCoproduct f] : Cocone (liftToFinsetObj (Discrete.functor f))

The converse of the construction in liftToFinsetColimitCocone: we can form a cocone on the coproduct of f whose legs are the coproducts over the finite subsets of α.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone_pt {C : Type u} [Category.{v, u} C] {α : Type w} [HasFiniteCoproducts C] (f : α → C) [HasCoproduct f] : (finiteSubcoproductsCocone f).pt = ∐ f

@[simp]

theorem CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone_ι_app {C : Type u} [Category.{v, u} C] {α : Type w} [HasFiniteCoproducts C] (f : α → C) [HasCoproduct f] (S : Finset (Discrete α)) : (finiteSubcoproductsCocone f).ι.app S = Sigma.desc fun (s : ↥S) => Sigma.ι f (↑s).as

noncomputable def CategoryTheory.Limits.CoproductsFromFiniteFiltered.isColimitFiniteSubproductsCocone {C : Type u} [Category.{v, u} C] {α : Type w} [HasFiniteCoproducts C] (f : α → C) [HasColimitsOfShape (Finset (Discrete α)) C] [HasCoproduct f] : IsColimit (finiteSubcoproductsCocone f)

The cocone finiteSubcoproductsCocone is a colimit cocone.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.hasCoproducts_of_finite_and_filtered {C : Type u} [Category.{v, u} C] [HasFiniteCoproducts C] [HasFilteredColimitsOfSize.{w, w, v, u} C] : HasCoproducts C

theorem CategoryTheory.Limits.has_colimits_of_finite_and_filtered {C : Type u} [Category.{v, u} C] [HasFiniteColimits C] [HasFilteredColimitsOfSize.{w, w, v, u} C] : HasColimitsOfSize.{w, w, v, u} C

theorem CategoryTheory.Limits.hasProducts_of_finite_and_cofiltered {C : Type u} [Category.{v, u} C] [HasFiniteProducts C] [HasCofilteredLimitsOfSize.{w, w, v, u} C] : HasProducts C

theorem CategoryTheory.Limits.has_limits_of_finite_and_cofiltered {C : Type u} [Category.{v, u} C] [HasFiniteLimits C] [HasCofilteredLimitsOfSize.{w, w, v, u} C] : HasLimitsOfSize.{w, w, v, u} C

theorem CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimIso_aux {C : Type u} [Category.{v, u} C] {α : Type w} [HasFiniteCoproducts C] [HasColimitsOfShape (Finset (Discrete α)) C] [HasColimitsOfShape (Discrete α) C] (F : Functor (Discrete α) C) {J : Finset (Discrete α)} (j : ↥J) : CategoryStruct.comp (Sigma.ι (fun (x : ↥J) => F.obj ↑x) j) (CategoryStruct.comp (colimit.ι (liftToFinsetObj F) J) (colimit.isoColimitCocone (liftToFinsetColimitCocone F)).inv) = colimit.ι F ↑j

Helper construction for liftToFinsetColimIso.

theorem CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimIso_aux_assoc {C : Type u} [Category.{v, u} C] {α : Type w} [HasFiniteCoproducts C] [HasColimitsOfShape (Finset (Discrete α)) C] [HasColimitsOfShape (Discrete α) C] (F : Functor (Discrete α) C) {J : Finset (Discrete α)} (j : ↥J) {Z : C} (h : colimit F ⟶ Z) : CategoryStruct.comp (Sigma.ι (fun (x : ↥J) => F.obj ↑x) j) (CategoryStruct.comp (colimit.ι (liftToFinsetObj F) J) (CategoryStruct.comp (colimit.isoColimitCocone (liftToFinsetColimitCocone F)).inv h)) = CategoryStruct.comp (colimit.ι F ↑j) h

Helper construction for liftToFinsetColimIso.

noncomputable def CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimIso {C : Type u} [Category.{v, u} C] {α : Type w} [HasFiniteCoproducts C] [HasColimitsOfShape (Finset (Discrete α)) C] [HasColimitsOfShape (Discrete α) C] : (liftToFinset C α).comp colim ≅ colim

The liftToFinset functor, precomposed with forming a colimit, is a coproduct on the original functor.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetEvaluationIso {C : Type u} [Category.{v, u} C] {α : Type w} [HasFiniteCoproducts C] (I : Finset (Discrete α)) : (liftToFinset C α).comp ((evaluation (Finset (Discrete α)) C).obj I) ≅ ((Functor.whiskeringLeft (Discrete ↥I) (Discrete α) C).obj (Discrete.functor fun (x : ↥I) => ↑x)).comp colim

liftToFinset, when composed with the evaluation functor, results in the whiskering composed with colim.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj {C : Type u} [Category.{v, u} C] {α : Type w} [HasFiniteProducts C] (F : Functor (Discrete α) C) : Functor (Finset (Discrete α))ᵒᵖ C

If C has finite coproducts, a functor Discrete α ⥤ C lifts to a functor Finset (Discrete α) ⥤ C by taking coproducts.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj_map {C : Type u} [Category.{v, u} C] {α : Type w} [HasFiniteProducts C] (F : Functor (Discrete α) C) {Y x✝ : (Finset (Discrete α))ᵒᵖ} (h : Y ⟶ x✝) : (liftToFinsetObj F).map h = Pi.lift fun (y : ↥(Opposite.unop x✝)) => Pi.π (fun (x : ↥(Opposite.unop Y)) => F.obj ↑x) ⟨↑y, ⋯⟩

@[simp]

theorem CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj_obj {C : Type u} [Category.{v, u} C] {α : Type w} [HasFiniteProducts C] (F : Functor (Discrete α) C) (s : (Finset (Discrete α))ᵒᵖ) : (liftToFinsetObj F).obj s = ∏ᶜ fun (x : ↥(Opposite.unop s)) => F.obj ↑x

noncomputable def CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone {C : Type u} [Category.{v, u} C] {α : Type w} [HasFiniteProducts C] [HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C] (F : Functor (Discrete α) C) : LimitCone F

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

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_isLimit_lift {C : Type u} [Category.{v, u} C] {α : Type w} [HasFiniteProducts C] [HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C] (F : Functor (Discrete α) C) (s : Cone F) : (liftToFinsetLimitCone F).isLimit.lift s = limit.lift (liftToFinsetObj F) { pt := s.pt, π := { app := fun (x : (Finset (Discrete α))ᵒᵖ) => Pi.lift fun (x_1 : ↥(Opposite.unop x)) => s.π.app ↑x_1, naturality := ⋯ } }

@[simp]

theorem CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_cone_pt {C : Type u} [Category.{v, u} C] {α : Type w} [HasFiniteProducts C] [HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C] (F : Functor (Discrete α) C) : (liftToFinsetLimitCone F).cone.pt = limit (liftToFinsetObj F)

@[simp]

theorem CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_cone_π_app {C : Type u} [Category.{v, u} C] {α : Type w} [HasFiniteProducts C] [HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C] (F : Functor (Discrete α) C) (j : Discrete α) : (liftToFinsetLimitCone F).cone.π.app j = CategoryStruct.comp (limit.π (liftToFinsetObj F) (Opposite.op {j})) (Pi.π (fun (x : ↥{j}) => F.obj ↑x) ⟨j, ⋯⟩)

noncomputable def CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone {C : Type u} [Category.{v, u} C] {α : Type w} [HasFiniteProducts C] (f : α → C) [HasProduct f] : Cone (liftToFinsetObj (Discrete.functor f))

The converse of the construction in liftToFinsetLimitCone: we can form a cone on the product of f whose legs are the products over the finite subsets of α.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone_π_app {C : Type u} [Category.{v, u} C] {α : Type w} [HasFiniteProducts C] (f : α → C) [HasProduct f] (S : (Finset (Discrete α))ᵒᵖ) : (finiteSubproductsCone f).π.app S = Pi.lift fun (s : ↥(Opposite.unop S)) => Pi.π f (↑s).as

@[simp]

theorem CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone_pt {C : Type u} [Category.{v, u} C] {α : Type w} [HasFiniteProducts C] (f : α → C) [HasProduct f] : (finiteSubproductsCone f).pt = ∏ᶜ f

noncomputable def CategoryTheory.Limits.ProductsFromFiniteCofiltered.isLimitFiniteSubproductsCone {C : Type u} [Category.{v, u} C] {α : Type w} [HasFiniteProducts C] (f : α → C) [HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C] [HasProduct f] : IsLimit (finiteSubproductsCone f)

The cone finiteSubproductsCone is a limit cone.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset (C : Type u) [Category.{v, u} C] (α : Type w) [HasFiniteProducts C] : Functor (Functor (Discrete α) C) (Functor (Finset (Discrete α))ᵒᵖ C)

The functor taking a functor Discrete α ⥤ C to a functor Finset (Discrete α) ⥤ C by taking coproducts.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset_map_app (C : Type u) [Category.{v, u} C] (α : Type w) [HasFiniteProducts C] {X✝ Y✝ : Functor (Discrete α) C} (β : X✝ ⟶ Y✝) (x✝ : (Finset (Discrete α))ᵒᵖ) : ((liftToFinset C α).map β).app x✝ = Pi.map fun (x : ↥(Opposite.unop x✝)) => β.app ↑x

@[simp]

theorem CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset_obj_map (C : Type u) [Category.{v, u} C] (α : Type w) [HasFiniteProducts C] (F : Functor (Discrete α) C) {Y x✝ : (Finset (Discrete α))ᵒᵖ} (h : Y ⟶ x✝) : ((liftToFinset C α).obj F).map h = Pi.lift fun (y : ↥(Opposite.unop x✝)) => Pi.π (fun (x : ↥(Opposite.unop Y)) => F.obj ↑x) ⟨↑y, ⋯⟩

@[simp]

theorem CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset_obj_obj (C : Type u) [Category.{v, u} C] (α : Type w) [HasFiniteProducts C] (F : Functor (Discrete α) C) (s : (Finset (Discrete α))ᵒᵖ) : ((liftToFinset C α).obj F).obj s = ∏ᶜ fun (x : ↥(Opposite.unop s)) => F.obj ↑x

noncomputable def CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimIso (C : Type u) [Category.{v, u} C] (α : Type w) [HasFiniteProducts C] [HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C] [HasLimitsOfShape (Discrete α) C] : (liftToFinset C α).comp lim ≅ lim

The liftToFinset functor, precomposed with forming a colimit, is a coproduct on the original functor.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetEvaluationIso (C : Type u) [Category.{v, u} C] (α : Type w) [HasFiniteProducts C] (I : Finset (Discrete α)) : (liftToFinset C α).comp ((evaluation (Finset (Discrete α))ᵒᵖ C).obj (Opposite.op I)) ≅ ((Functor.whiskeringLeft (Discrete ↥I) (Discrete α) C).obj (Discrete.functor fun (x : ↥I) => ↑x)).comp lim

liftToFinset, when composed with the evaluation functor, results in the whiskering composed with colim.

Equations

• One or more equations did not get rendered due to their size.