Documentation

Mathlib.CategoryTheory.Limits.Constructions.Filtered

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ᵒᵖ.

source
@[simp]
theorem CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj_obj {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasFiniteCoproducts C] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C) (s : Finset (CategoryTheory.Discrete α)) :
(CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj F).obj s = ∐ fun (x : { x : CategoryTheory.Discrete α // x ∈ s }) => F.obj ↑x
source
@[simp]
theorem CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj_map {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasFiniteCoproducts C] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C) :
∀ {x Y : Finset (CategoryTheory.Discrete α)} (h : x ⟶ Y), (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj F).map h = CategoryTheory.Limits.Sigma.desc fun (y : { x_1 : CategoryTheory.Discrete α // x_1 ∈ x }) => CategoryTheory.Limits.Sigma.ι (fun (x : { x : CategoryTheory.Discrete α // x ∈ Y }) => F.obj ↑x) ⟨↑y, ⋯⟩
source
def CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasFiniteCoproducts C] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C) :
CategoryTheory.Functor (Finset (CategoryTheory.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.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone_cocone_pt {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v, u} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C) :
    (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone F).cocone.pt = CategoryTheory.Limits.colimit (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj F)
    source
    @[simp]
    theorem CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone_isColimit_desc {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v, u} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C) (s : CategoryTheory.Limits.Cocone F) :
    (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone F).isColimit.desc s = CategoryTheory.Limits.colimit.desc (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj F) { pt := s.pt, ι := { app := fun (t : Finset (CategoryTheory.Discrete α)) => CategoryTheory.Limits.Sigma.desc fun (x : { x : CategoryTheory.Discrete α // x ∈ t }) => s.ι.app ↑x, naturality := ⋯ } }
    source
    @[simp]
    theorem CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone_cocone_ι_app {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v, u} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C) (j : CategoryTheory.Discrete α) :
    (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone F).cocone.ι.app j = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : { x : CategoryTheory.Discrete α // x ∈ {j} }) => F.obj ↑x) ⟨j, ⋯⟩) (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj F) {j})
    source
    def CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v, u} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C) :
    CategoryTheory.Limits.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.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset_obj_obj (C : Type u) [CategoryTheory.Category.{v, u} C] (α : Type w) [CategoryTheory.Limits.HasFiniteCoproducts C] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C) (s : Finset (CategoryTheory.Discrete α)) :
      ((CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset C α).obj F).obj s = ∐ fun (x : { x : CategoryTheory.Discrete α // x ∈ s }) => F.obj ↑x
      source
      @[simp]
      theorem CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset_obj_map (C : Type u) [CategoryTheory.Category.{v, u} C] (α : Type w) [CategoryTheory.Limits.HasFiniteCoproducts C] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C) :
      ∀ {x Y : Finset (CategoryTheory.Discrete α)} (h : x ⟶ Y), ((CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset C α).obj F).map h = CategoryTheory.Limits.Sigma.desc fun (y : { x_1 : CategoryTheory.Discrete α // x_1 ∈ x }) => CategoryTheory.Limits.Sigma.ι (fun (x : { x : CategoryTheory.Discrete α // x ∈ Y }) => F.obj ↑x) ⟨↑y, ⋯⟩
      source
      @[simp]
      theorem CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset_map_app (C : Type u) [CategoryTheory.Category.{v, u} C] (α : Type w) [CategoryTheory.Limits.HasFiniteCoproducts C] :
      ∀ {X Y : CategoryTheory.Functor (CategoryTheory.Discrete α) C} (β : X ⟶ Y) (x : Finset (CategoryTheory.Discrete α)), ((CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset C α).map β).app x = CategoryTheory.Limits.Sigma.map fun (x_1 : { x_1 : CategoryTheory.Discrete α // x_1 ∈ x }) => β.app ↑x_1
      source
      def CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset (C : Type u) [CategoryTheory.Category.{v, u} C] (α : Type w) [CategoryTheory.Limits.HasFiniteCoproducts C] :
      CategoryTheory.Functor (CategoryTheory.Functor (CategoryTheory.Discrete α) C) (CategoryTheory.Functor (Finset (CategoryTheory.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.
      Instances For
        source
        theorem CategoryTheory.Limits.hasCoproducts_of_finite_and_filtered {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v, u} C] :
        CategoryTheory.Limits.HasCoproducts C
        source
        theorem CategoryTheory.Limits.has_colimits_of_finite_and_filtered {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v, u} C] :
        CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u} C
        source
        theorem CategoryTheory.Limits.hasProducts_of_finite_and_cofiltered {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w, w, v, u} C] :
        CategoryTheory.Limits.HasProducts C
        source
        theorem CategoryTheory.Limits.has_limits_of_finite_and_cofiltered {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w, w, v, u} C] :
        CategoryTheory.Limits.HasLimitsOfSize.{w, w, v, u} C
        source
        theorem CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimIso_aux_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v, u} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C) {J : Finset (CategoryTheory.Discrete α)} (j : { x : CategoryTheory.Discrete α // x ∈ J }) {Z : C} (h : CategoryTheory.Limits.colimit F ⟶ Z) :
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : { x : CategoryTheory.Discrete α // x ∈ J }) => F.obj ↑x) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj F) J) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.isoColimitCocone (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone F)).inv h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F ↑j) h
        source
        theorem CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimIso_aux {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v, u} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C) {J : Finset (CategoryTheory.Discrete α)} (j : { x : CategoryTheory.Discrete α // x ∈ J }) :
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : { x : CategoryTheory.Discrete α // x ∈ J }) => F.obj ↑x) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj F) J) (CategoryTheory.Limits.colimit.isoColimitCocone (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone F)).inv) = CategoryTheory.Limits.colimit.ι F ↑j

        Helper construction for liftToFinsetColimIso.

        source
        def CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimIso {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v, u} C] :
        (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset C α).comp CategoryTheory.Limits.colim ≅ CategoryTheory.Limits.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.
        Instances For