Documentation

Mathlib.CategoryTheory.Filtered.Basic

Filtered categories #

A category is filtered if every finite diagram admits a cocone. We give a simple characterisation of this condition as

  1. for every pair of objects there exists another object "to the right",
  2. for every pair of parallel morphisms there exists a morphism to the right so the compositions are equal, and
  3. there exists some object.

Filtered colimits are often better behaved than arbitrary colimits. See CategoryTheory/Limits/Types for some details.

Filtered categories are nice because colimits indexed by filtered categories tend to be easier to describe than general colimits (and more often preserved by functors).

In this file we show that any functor from a finite category to a filtered category admits a cocone:

Furthermore, we give special support for two diagram categories: The bowtie and the tulip. This is because these shapes show up in the proofs that forgetful functors of algebraic categories (e.g. MonCat, CommRingCat, ...) preserve filtered colimits.

All of the above API, except for the bowtie and the tulip, is also provided for cofiltered categories.

See also #

In CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit we show that filtered colimits commute with finite limits.

A category IsFilteredOrEmpty if

  1. for every pair of objects there exists another object "to the right", and
  2. for every pair of parallel morphisms there exists a morphism to the right so the compositions are equal.
Instances

    A category IsFiltered if

    1. for every pair of objects there exists another object "to the right",
    2. for every pair of parallel morphisms there exists a morphism to the right so the compositions are equal, and
    3. there exists some object.

    See https://stacks.math.columbia.edu/tag/002V. (They also define a diagram being filtered.)

    Instances

      max j j' is an arbitrary choice of object to the right of both j and j', whose existence is ensured by IsFiltered.

      Instances For

        leftToMax j j' is an arbitrary choice of morphism from j to max j j', whose existence is ensured by IsFiltered.

        Instances For

          rightToMax j j' is an arbitrary choice of morphism from j' to max j j', whose existence is ensured by IsFiltered.

          Instances For
            noncomputable def CategoryTheory.IsFiltered.coeq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {j : C} {j' : C} (f : j j') (f' : j j') :
            C

            coeq f f', for morphisms f f' : j ⟶ j', is an arbitrary choice of object which admits a morphism coeqHom f f' : j' ⟶ coeq f f' such that coeq_condition : f ≫ coeqHom f f' = f' ≫ coeqHom f f'. Its existence is ensured by IsFiltered.

            Instances For

              coeqHom f f', for morphisms f f' : j ⟶ j', is an arbitrary choice of morphism coeqHom f f' : j' ⟶ coeq f f' such that coeq_condition : f ≫ coeqHom f f' = f' ≫ coeqHom f f'. Its existence is ensured by IsFiltered.

              Instances For

                If C is filtered or emtpy, and we have a functor R : C ⥤ D with a left adjoint, then D is filtered or empty.

                If C is filtered or empty, and we have a right adjoint functor R : C ⥤ D, then D is filtered or empty.

                Any finite collection of objects in a filtered category has an object "to the right".

                theorem CategoryTheory.IsFiltered.sup_exists {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered C] (O : Finset C) (H : Finset ((X : C) ×' (Y : C) ×' (_ : X O) ×' (_ : Y O) ×' (X Y))) :
                S T, ∀ {X Y : C} (mX : X O) (mY : Y O) {f : X Y}, { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } HCategoryTheory.CategoryStruct.comp f (T Y mY) = T X mX

                Given any Finset of objects {X, ...} and indexed collection of Finsets of morphisms {f, ...} in C, there exists an object S, with a morphism T X : X ⟶ S from each X, such that the triangles commute: f ≫ T Y = T X, for f : X ⟶ Y in the Finset.

                noncomputable def CategoryTheory.IsFiltered.sup {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered C] (O : Finset C) (H : Finset ((X : C) ×' (Y : C) ×' (_ : X O) ×' (_ : Y O) ×' (X Y))) :
                C

                An arbitrary choice of object "to the right" of a finite collection of objects O and morphisms H, making all the triangles commute.

                Instances For
                  noncomputable def CategoryTheory.IsFiltered.toSup {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered C] (O : Finset C) (H : Finset ((X : C) ×' (Y : C) ×' (_ : X O) ×' (_ : Y O) ×' (X Y))) {X : C} (m : X O) :

                  The morphisms to sup O H.

                  Instances For
                    theorem CategoryTheory.IsFiltered.toSup_commutes {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered C] (O : Finset C) (H : Finset ((X : C) ×' (Y : C) ×' (_ : X O) ×' (_ : Y O) ×' (X Y))) {X : C} {Y : C} (mX : X O) (mY : Y O) {f : X Y} (mf : { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H) :

                    The triangles of consisting of a morphism in H and the maps to sup O H commute.

                    If we have IsFiltered C, then for any functor F : J ⥤ C with FinCategory J, there exists a cocone over F.

                    An arbitrary choice of cocone over F : J ⥤ C, for FinCategory J and IsFiltered C.

                    Instances For

                      If C is filtered, and we have a functor R : C ⥤ D with a left adjoint, then D is filtered.

                      If C is filtered, and we have a right adjoint functor R : C ⥤ D, then D is filtered.

                      Being filtered is preserved by equivalence of categories.

                      noncomputable def CategoryTheory.IsFiltered.max₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] (j₁ : C) (j₂ : C) (j₃ : C) :
                      C

                      max₃ j₁ j₂ j₃ is an arbitrary choice of object to the right of j₁, j₂ and j₃, whose existence is ensured by IsFiltered.

                      Instances For

                        firstToMax₃ j₁ j₂ j₃ is an arbitrary choice of morphism from j₁ to max₃ j₁ j₂ j₃, whose existence is ensured by IsFiltered.

                        Instances For

                          secondToMax₃ j₁ j₂ j₃ is an arbitrary choice of morphism from j₂ to max₃ j₁ j₂ j₃, whose existence is ensured by IsFiltered.

                          Instances For

                            thirdToMax₃ j₁ j₂ j₃ is an arbitrary choice of morphism from j₃ to max₃ j₁ j₂ j₃, whose existence is ensured by IsFiltered.

                            Instances For
                              noncomputable def CategoryTheory.IsFiltered.coeq₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {j₁ : C} {j₂ : C} (f : j₁ j₂) (g : j₁ j₂) (h : j₁ j₂) :
                              C

                              coeq₃ f g h, for morphisms f g h : j₁ ⟶ j₂, is an arbitrary choice of object which admits a morphism coeq₃Hom f g h : j₂ ⟶ coeq₃ f g h such that coeq₃_condition₁, coeq₃_condition₂ and coeq₃_condition₃ are satisfied. Its existence is ensured by IsFiltered.

                              Instances For
                                noncomputable def CategoryTheory.IsFiltered.coeq₃Hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {j₁ : C} {j₂ : C} (f : j₁ j₂) (g : j₁ j₂) (h : j₁ j₂) :

                                coeq₃Hom f g h, for morphisms f g h : j₁ ⟶ j₂, is an arbitrary choice of morphism j₂ ⟶ coeq₃ f g h such that coeq₃_condition₁, coeq₃_condition₂ and coeq₃_condition₃ are satisfied. Its existence is ensured by IsFiltered.

                                Instances For

                                  For every span j ⟵ i ⟶ j', there exists a cocone j ⟶ k ⟵ j' such that the square commutes.

                                  theorem CategoryTheory.IsFiltered.bowtie {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {j₁ : C} {j₂ : C} {k₁ : C} {k₂ : C} (f₁ : j₁ k₁) (g₁ : j₁ k₂) (f₂ : j₂ k₁) (g₂ : j₂ k₂) :

                                  Given a "bowtie" of morphisms

                                   j₁   j₂
                                   |\  /|
                                   | \/ |
                                   | /\ |
                                   |/  \∣
                                   vv  vv
                                   k₁  k₂
                                  

                                  in a filtered category, we can construct an object s and two morphisms from k₁ and k₂ to s, making the resulting squares commute.

                                  theorem CategoryTheory.IsFiltered.tulip {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {j₁ : C} {j₂ : C} {j₃ : C} {k₁ : C} {k₂ : C} {l : C} (f₁ : j₁ k₁) (f₂ : j₂ k₁) (f₃ : j₂ k₂) (f₄ : j₃ k₂) (g₁ : j₁ l) (g₂ : j₃ l) :

                                  Given a "tulip" of morphisms

                                   j₁    j₂    j₃
                                   |\   / \   / |
                                   | \ /   \ /  |
                                   |  vv    vv  |
                                   \  k₁    k₂ /
                                    \         /
                                     \       /
                                      \     /
                                       \   /
                                        v v
                                         l
                                  

                                  in a filtered category, we can construct an object s and three morphisms from k₁, k₂ and l to s, making the resulting squares commute.

                                  A category IsCofilteredOrEmpty if

                                  1. for every pair of objects there exists another object "to the left", and
                                  2. for every pair of parallel morphisms there exists a morphism to the left so the compositions are equal.
                                  Instances

                                    A category IsCofiltered if

                                    1. for every pair of objects there exists another object "to the left",
                                    2. for every pair of parallel morphisms there exists a morphism to the left so the compositions are equal, and
                                    3. there exists some object.

                                    See https://stacks.math.columbia.edu/tag/04AZ.

                                    Instances

                                      min j j' is an arbitrary choice of object to the left of both j and j', whose existence is ensured by IsCofiltered.

                                      Instances For

                                        minToLeft j j' is an arbitrary choice of morphism from min j j' to j, whose existence is ensured by IsCofiltered.

                                        Instances For

                                          minToRight j j' is an arbitrary choice of morphism from min j j' to j', whose existence is ensured by IsCofiltered.

                                          Instances For
                                            noncomputable def CategoryTheory.IsCofiltered.eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {j : C} {j' : C} (f : j j') (f' : j j') :
                                            C

                                            eq f f', for morphisms f f' : j ⟶ j', is an arbitrary choice of object which admits a morphism eqHom f f' : eq f f' ⟶ j such that eq_condition : eqHom f f' ≫ f = eqHom f f' ≫ f'. Its existence is ensured by IsCofiltered.

                                            Instances For

                                              eqHom f f', for morphisms f f' : j ⟶ j', is an arbitrary choice of morphism eqHom f f' : eq f f' ⟶ j such that eq_condition : eqHom f f' ≫ f = eqHom f f' ≫ f'. Its existence is ensured by IsCofiltered.

                                              Instances For

                                                For every cospan j ⟶ i ⟵ j', there exists a cone j ⟵ k ⟶ j' such that the square commutes.

                                                If C is cofiltered or empty, and we have a functor L : C ⥤ D with a right adjoint, then D is cofiltered or empty.

                                                If C is cofiltered or empty, and we have a left adjoint functor L : C ⥤ D, then D is cofiltered or empty.

                                                Any finite collection of objects in a cofiltered category has an object "to the left".

                                                theorem CategoryTheory.IsCofiltered.inf_exists {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered C] (O : Finset C) (H : Finset ((X : C) ×' (Y : C) ×' (_ : X O) ×' (_ : Y O) ×' (X Y))) :
                                                S T, ∀ {X Y : C} (mX : X O) (mY : Y O) {f : X Y}, { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } HCategoryTheory.CategoryStruct.comp (T X mX) f = T Y mY

                                                Given any Finset of objects {X, ...} and indexed collection of Finsets of morphisms {f, ...} in C, there exists an object S, with a morphism T X : S ⟶ X from each X, such that the triangles commute: T X ≫ f = T Y, for f : X ⟶ Y in the Finset.

                                                noncomputable def CategoryTheory.IsCofiltered.inf {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered C] (O : Finset C) (H : Finset ((X : C) ×' (Y : C) ×' (_ : X O) ×' (_ : Y O) ×' (X Y))) :
                                                C

                                                An arbitrary choice of object "to the left" of a finite collection of objects O and morphisms H, making all the triangles commute.

                                                Instances For
                                                  noncomputable def CategoryTheory.IsCofiltered.infTo {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered C] (O : Finset C) (H : Finset ((X : C) ×' (Y : C) ×' (_ : X O) ×' (_ : Y O) ×' (X Y))) {X : C} (m : X O) :

                                                  The morphisms from inf O H.

                                                  Instances For
                                                    theorem CategoryTheory.IsCofiltered.infTo_commutes {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered C] (O : Finset C) (H : Finset ((X : C) ×' (Y : C) ×' (_ : X O) ×' (_ : Y O) ×' (X Y))) {X : C} {Y : C} (mX : X O) (mY : Y O) {f : X Y} (mf : { fst := X, snd := { fst := Y, snd := { fst := mX, snd := { fst := mY, snd := f } } } } H) :

                                                    The triangles consisting of a morphism in H and the maps from inf O H commute.

                                                    If we have IsCofiltered C, then for any functor F : J ⥤ C with FinCategory J, there exists a cone over F.

                                                    An arbitrary choice of cone over F : J ⥤ C, for FinCategory J and IsCofiltered C.

                                                    Instances For

                                                      If C is cofiltered, and we have a functor L : C ⥤ D with a right adjoint, then D is cofiltered.

                                                      If C is cofiltered, and we have a left adjoint functor L : C ⥤ D, then D is cofiltered.