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:

• cocone_nonempty [FinCategory J] [IsFiltered C] (F : J ⥤ C) : Nonempty (Cocone F) More generally, for any finite collection of objects and morphisms between them in a filtered category (even if not closed under composition) there exists some object Z receiving maps from all of them, so that all the triangles (one edge from the finite set, two from morphisms to Z) commute. This formulation is often more useful in practice and is available via sup_exists, which takes a finset of objects, and an indexed family (indexed by source and target) of finsets of morphisms.

We also prove the converse of cocone_nonempty as of_cocone_nonempty.

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.

There is another characterization of filtered categories, namely that whenever F : J ⥤ C is a functor from a finite category, there is X : C such that Nonempty (limit (F.op ⋙ yoneda.obj X)). This is shown in CategoryTheory.Limits.Filtered.

class CategoryTheory.IsFilteredOrEmpty (C : Type u) [CategoryTheory.Category.{v, u} C] : Prop

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.

• cocone_objs : ∀ (X Y : C), ∃ (Z : C) (x : X ⟶ Z) (x : Y ⟶ Z), True

  for every pair of objects there exists another object "to the right"

• cocone_maps : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), ∃ (Z : C) (h : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h

  for every pair of parallel morphisms there exists a morphism to the right so the compositions are equal

class CategoryTheory.IsFiltered (C : Type u) [CategoryTheory.Category.{v, u} C] extends CategoryTheory.IsFilteredOrEmpty : Prop

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 . (They also define a diagram being filtered.)

• cocone_objs : ∀ (X Y : C), ∃ (Z : C) (x : X ⟶ Z) (x : Y ⟶ Z), True
• cocone_maps : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), ∃ (Z : C) (h : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h
• nonempty : Nonempty C

  a filtered category must be non empty

instance CategoryTheory.isFilteredOrEmpty_of_semilatticeSup (α : Type u) [SemilatticeSup α] : CategoryTheory.IsFilteredOrEmpty α

Equations

• ⋯ = ⋯

instance CategoryTheory.isFiltered_of_semilatticeSup_nonempty (α : Type u) [SemilatticeSup α] [Nonempty α] : CategoryTheory.IsFiltered α

Equations

• ⋯ = ⋯

instance CategoryTheory.isFilteredOrEmpty_of_directed_le (α : Type u) [Preorder α] [IsDirected α fun (x x_1 : α) => x ≤ x_1] : CategoryTheory.IsFilteredOrEmpty α

Equations

• ⋯ = ⋯

instance CategoryTheory.isFiltered_of_directed_le_nonempty (α : Type u) [Preorder α] [IsDirected α fun (x x_1 : α) => x ≤ x_1] [Nonempty α] : CategoryTheory.IsFiltered α

Equations

• ⋯ = ⋯

instance CategoryTheory.instIsFilteredDiscretePUnitDiscreteCategory : CategoryTheory.IsFiltered (CategoryTheory.Discrete PUnit.{u_1 + 1} )

Equations

• CategoryTheory.instIsFilteredDiscretePUnitDiscreteCategory = ⋯

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

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

Equations

• CategoryTheory.IsFiltered.max j j' = Exists.choose ⋯

noncomputable def CategoryTheory.IsFiltered.leftToMax {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] (j : C) (j' : C) : j ⟶ CategoryTheory.IsFiltered.max j j'

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

Equations

• CategoryTheory.IsFiltered.leftToMax j j' = Exists.choose ⋯

noncomputable def CategoryTheory.IsFiltered.rightToMax {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] (j : C) (j' : C) : j' ⟶ CategoryTheory.IsFiltered.max j j'

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

Equations

• CategoryTheory.IsFiltered.rightToMax j j' = Exists.choose ⋯

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.

Equations

• CategoryTheory.IsFiltered.coeq f f' = Exists.choose ⋯

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

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.

Equations

• CategoryTheory.IsFiltered.coeqHom f f' = Exists.choose ⋯

theorem CategoryTheory.IsFiltered.coeq_condition_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {j : C} {j' : C} (f : j ⟶ j') (f' : j ⟶ j') {Z : C} (h : CategoryTheory.IsFiltered.coeq f f' ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.IsFiltered.coeqHom f f') h) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp (CategoryTheory.IsFiltered.coeqHom f f') h)

theorem CategoryTheory.IsFiltered.coeq_condition {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {j : C} {j' : C} (f : j ⟶ j') (f' : j ⟶ j') : CategoryTheory.CategoryStruct.comp f (CategoryTheory.IsFiltered.coeqHom f f') = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.IsFiltered.coeqHom f f')

coeq_condition f f', for morphisms f f' : j ⟶ j', is the proof that f ≫ coeqHom f f' = f' ≫ coeqHom f f'.

theorem CategoryTheory.IsFilteredOrEmpty.of_right_adjoint {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] {L : CategoryTheory.Functor D C} {R : CategoryTheory.Functor C D} (h : L ⊣ R) : CategoryTheory.IsFilteredOrEmpty D

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

theorem CategoryTheory.IsFilteredOrEmpty.of_isRightAdjoint {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (R : CategoryTheory.Functor C D) [CategoryTheory.IsRightAdjoint R] : CategoryTheory.IsFilteredOrEmpty D

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

theorem CategoryTheory.IsFilteredOrEmpty.of_equivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (h : C ≌ D) : CategoryTheory.IsFilteredOrEmpty D

Being filtered or empty is preserved by equivalence of categories.

theorem CategoryTheory.IsFiltered.sup_objs_exists {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered C] (O : Finset C) : ∃ (S : C), ∀ {X : C}, X ∈ O → Nonempty (X ⟶ S)

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 : C) (T : {X : C} → X ∈ O → (X ⟶ S)), ∀ {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 } } } } ∈ H → CategoryTheory.CategoryStruct.comp f (T mY) = T 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.

Equations

• CategoryTheory.IsFiltered.sup O H = Exists.choose ⋯

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) : X ⟶ CategoryTheory.IsFiltered.sup O H

The morphisms to sup O H.

Equations

• CategoryTheory.IsFiltered.toSup O H m = Exists.choose ⋯ m

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) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.IsFiltered.toSup O H mY) = CategoryTheory.IsFiltered.toSup O H mX

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

theorem CategoryTheory.IsFiltered.cocone_nonempty {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered C] {J : Type w} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (F : CategoryTheory.Functor J C) : Nonempty (CategoryTheory.Limits.Cocone F)

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

noncomputable def CategoryTheory.IsFiltered.cocone {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered C] {J : Type w} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (F : CategoryTheory.Functor J C) : CategoryTheory.Limits.Cocone F

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

Equations

• CategoryTheory.IsFiltered.cocone F = Nonempty.some ⋯

theorem CategoryTheory.IsFiltered.of_right_adjoint {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] {L : CategoryTheory.Functor D C} {R : CategoryTheory.Functor C D} (h : L ⊣ R) : CategoryTheory.IsFiltered D

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

theorem CategoryTheory.IsFiltered.of_isRightAdjoint {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (R : CategoryTheory.Functor C D) [CategoryTheory.IsRightAdjoint R] : CategoryTheory.IsFiltered D

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

theorem CategoryTheory.IsFiltered.of_equivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (h : C ≌ D) : CategoryTheory.IsFiltered D

Being filtered is preserved by equivalence of categories.

theorem CategoryTheory.IsFiltered.of_cocone_nonempty (C : Type u) [CategoryTheory.Category.{v, u} C] (h : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.FinCategory J] (F : CategoryTheory.Functor J C), Nonempty (CategoryTheory.Limits.Cocone F)) : CategoryTheory.IsFiltered C

If every finite diagram in C admits a cocone, then C is filtered. It is sufficient to verify this for diagrams whose shape lives in any one fixed universe.

theorem CategoryTheory.IsFiltered.of_hasFiniteColimits (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.IsFiltered C

theorem CategoryTheory.IsFiltered.of_isTerminal (C : Type u) [CategoryTheory.Category.{v, u} C] {X : C} (h : CategoryTheory.Limits.IsTerminal X) : CategoryTheory.IsFiltered C

instance CategoryTheory.IsFiltered.of_hasTerminal (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.IsFiltered C

Equations

• ⋯ = ⋯

theorem CategoryTheory.IsFiltered.iff_cocone_nonempty (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.IsFiltered C ↔ ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.FinCategory J] (F : CategoryTheory.Functor J C), Nonempty (CategoryTheory.Limits.Cocone F)

For every universe w, C is filtered if and only if every finite diagram in C with shape in w admits a cocone.

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.

Equations

• CategoryTheory.IsFiltered.max₃ j₁ j₂ j₃ = CategoryTheory.IsFiltered.max (CategoryTheory.IsFiltered.max j₁ j₂) j₃

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

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

Equations

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

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

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

Equations

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

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

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

Equations

• CategoryTheory.IsFiltered.thirdToMax₃ j₁ j₂ j₃ = CategoryTheory.IsFiltered.rightToMax (CategoryTheory.IsFiltered.max j₁ j₂) j₃

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.

Equations

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

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₂) : j₂ ⟶ CategoryTheory.IsFiltered.coeq₃ f g h

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.

Equations

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

theorem CategoryTheory.IsFiltered.coeq₃_condition₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {j₁ : C} {j₂ : C} (f : j₁ ⟶ j₂) (g : j₁ ⟶ j₂) (h : j₁ ⟶ j₂) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.IsFiltered.coeq₃Hom f g h) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.IsFiltered.coeq₃Hom f g h)

theorem CategoryTheory.IsFiltered.coeq₃_condition₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {j₁ : C} {j₂ : C} (f : j₁ ⟶ j₂) (g : j₁ ⟶ j₂) (h : j₁ ⟶ j₂) : CategoryTheory.CategoryStruct.comp g (CategoryTheory.IsFiltered.coeq₃Hom f g h) = CategoryTheory.CategoryStruct.comp h (CategoryTheory.IsFiltered.coeq₃Hom f g h)

theorem CategoryTheory.IsFiltered.coeq₃_condition₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {j₁ : C} {j₂ : C} (f : j₁ ⟶ j₂) (g : j₁ ⟶ j₂) (h : j₁ ⟶ j₂) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.IsFiltered.coeq₃Hom f g h) = CategoryTheory.CategoryStruct.comp h (CategoryTheory.IsFiltered.coeq₃Hom f g h)

theorem CategoryTheory.IsFiltered.span {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {i : C} {j : C} {j' : C} (f : i ⟶ j) (f' : i ⟶ j') : ∃ (k : C) (g : j ⟶ k) (g' : j' ⟶ k), CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f' g'

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₂) : ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), CategoryTheory.CategoryStruct.comp f₁ α = CategoryTheory.CategoryStruct.comp g₁ β ∧ CategoryTheory.CategoryStruct.comp f₂ α = CategoryTheory.CategoryStruct.comp g₂ β

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) : ∃ (s : C) (α : k₁ ⟶ s) (β : l ⟶ s) (γ : k₂ ⟶ s), CategoryTheory.CategoryStruct.comp f₁ α = CategoryTheory.CategoryStruct.comp g₁ β ∧ CategoryTheory.CategoryStruct.comp f₂ α = CategoryTheory.CategoryStruct.comp f₃ γ ∧ CategoryTheory.CategoryStruct.comp f₄ γ = CategoryTheory.CategoryStruct.comp g₂ β

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.

class CategoryTheory.IsCofilteredOrEmpty (C : Type u) [CategoryTheory.Category.{v, u} C] : Prop

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.

• cone_objs : ∀ (X Y : C), ∃ (W : C) (x : W ⟶ X) (x : W ⟶ Y), True

  for every pair of objects there exists another object "to the left"

• cone_maps : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), ∃ (W : C) (h : W ⟶ X), CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g

  for every pair of parallel morphisms there exists a morphism to the left so the compositions are equal

class CategoryTheory.IsCofiltered (C : Type u) [CategoryTheory.Category.{v, u} C] extends CategoryTheory.IsCofilteredOrEmpty : Prop

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 .

• cone_objs : ∀ (X Y : C), ∃ (W : C) (x : W ⟶ X) (x : W ⟶ Y), True
• cone_maps : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), ∃ (W : C) (h : W ⟶ X), CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g
• nonempty : Nonempty C

  a cofiltered category must be non empty

instance CategoryTheory.isCofilteredOrEmpty_of_semilatticeInf (α : Type u) [SemilatticeInf α] : CategoryTheory.IsCofilteredOrEmpty α

Equations

• ⋯ = ⋯

instance CategoryTheory.isCofiltered_of_semilatticeInf_nonempty (α : Type u) [SemilatticeInf α] [Nonempty α] : CategoryTheory.IsCofiltered α

Equations

• ⋯ = ⋯

instance CategoryTheory.isCofilteredOrEmpty_of_directed_ge (α : Type u) [Preorder α] [IsDirected α fun (x x_1 : α) => x ≥ x_1] : CategoryTheory.IsCofilteredOrEmpty α

Equations

• ⋯ = ⋯

instance CategoryTheory.isCofiltered_of_directed_ge_nonempty (α : Type u) [Preorder α] [IsDirected α fun (x x_1 : α) => x ≥ x_1] [Nonempty α] : CategoryTheory.IsCofiltered α

Equations

• ⋯ = ⋯

instance CategoryTheory.instIsCofilteredDiscretePUnitDiscreteCategory : CategoryTheory.IsCofiltered (CategoryTheory.Discrete PUnit.{u_1 + 1} )

Equations

• CategoryTheory.instIsCofilteredDiscretePUnitDiscreteCategory = ⋯

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

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

Equations

• CategoryTheory.IsCofiltered.min j j' = Exists.choose ⋯

noncomputable def CategoryTheory.IsCofiltered.minToLeft {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] (j : C) (j' : C) : CategoryTheory.IsCofiltered.min j j' ⟶ j

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

Equations

• CategoryTheory.IsCofiltered.minToLeft j j' = Exists.choose ⋯

noncomputable def CategoryTheory.IsCofiltered.minToRight {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] (j : C) (j' : C) : CategoryTheory.IsCofiltered.min j j' ⟶ j'

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

Equations

• CategoryTheory.IsCofiltered.minToRight j j' = Exists.choose ⋯

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.

Equations

• CategoryTheory.IsCofiltered.eq f f' = Exists.choose ⋯

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

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.

Equations

• CategoryTheory.IsCofiltered.eqHom f f' = Exists.choose ⋯

theorem CategoryTheory.IsCofiltered.eq_condition_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {j : C} {j' : C} (f : j ⟶ j') (f' : j ⟶ j') {Z : C} (h : j' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.IsCofiltered.eqHom f f') (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.IsCofiltered.eqHom f f') (CategoryTheory.CategoryStruct.comp f' h)

theorem CategoryTheory.IsCofiltered.eq_condition {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {j : C} {j' : C} (f : j ⟶ j') (f' : j ⟶ j') : CategoryTheory.CategoryStruct.comp (CategoryTheory.IsCofiltered.eqHom f f') f = CategoryTheory.CategoryStruct.comp (CategoryTheory.IsCofiltered.eqHom f f') f'

eq_condition f f', for morphisms f f' : j ⟶ j', is the proof that eqHom f f' ≫ f = eqHom f f' ≫ f'.

theorem CategoryTheory.IsCofiltered.cospan {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {i : C} {j : C} {j' : C} (f : j ⟶ i) (f' : j' ⟶ i) : ∃ (k : C) (g : k ⟶ j) (g' : k ⟶ j'), CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.comp g' f'

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

theorem CategoryTheory.Functor.ranges_directed {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] (F : CategoryTheory.Functor C (Type u_1)) (j : C) : Directed (fun (x x_1 : Set (F.obj j)) => x ⊇ x_1) fun (f : (i : C) ×' (i ⟶ j)) => Set.range (F.map f.snd)

theorem CategoryTheory.IsCofilteredOrEmpty.of_left_adjoint {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : CategoryTheory.IsCofilteredOrEmpty D

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

theorem CategoryTheory.IsCofilteredOrEmpty.of_isLeftAdjoint {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (L : CategoryTheory.Functor C D) [CategoryTheory.IsLeftAdjoint L] : CategoryTheory.IsCofilteredOrEmpty D

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

theorem CategoryTheory.IsCofilteredOrEmpty.of_equivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (h : C ≌ D) : CategoryTheory.IsCofilteredOrEmpty D

Being cofiltered or empty is preserved by equivalence of categories.

theorem CategoryTheory.IsCofiltered.inf_objs_exists {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered C] (O : Finset C) : ∃ (S : C), ∀ {X : C}, X ∈ O → Nonempty (S ⟶ X)

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 : C) (T : {X : C} → X ∈ O → (S ⟶ X)), ∀ {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 } } } } ∈ H → CategoryTheory.CategoryStruct.comp (T mX) f = T 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.

Equations

• CategoryTheory.IsCofiltered.inf O H = Exists.choose ⋯

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) : CategoryTheory.IsCofiltered.inf O H ⟶ X

The morphisms from inf O H.

Equations

• CategoryTheory.IsCofiltered.infTo O H m = Exists.choose ⋯ m

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) : CategoryTheory.CategoryStruct.comp (CategoryTheory.IsCofiltered.infTo O H mX) f = CategoryTheory.IsCofiltered.infTo O H mY

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

theorem CategoryTheory.IsCofiltered.cone_nonempty {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered C] {J : Type w} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (F : CategoryTheory.Functor J C) : Nonempty (CategoryTheory.Limits.Cone F)

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

noncomputable def CategoryTheory.IsCofiltered.cone {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered C] {J : Type w} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (F : CategoryTheory.Functor J C) : CategoryTheory.Limits.Cone F

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

Equations

• CategoryTheory.IsCofiltered.cone F = Nonempty.some ⋯

theorem CategoryTheory.IsCofiltered.of_left_adjoint {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : CategoryTheory.IsCofiltered D

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

theorem CategoryTheory.IsCofiltered.of_isLeftAdjoint {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (L : CategoryTheory.Functor C D) [CategoryTheory.IsLeftAdjoint L] : CategoryTheory.IsCofiltered D

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

theorem CategoryTheory.IsCofiltered.of_equivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (h : C ≌ D) : CategoryTheory.IsCofiltered D

Being cofiltered is preserved by equivalence of categories.

theorem CategoryTheory.IsCofiltered.of_cone_nonempty (C : Type u) [CategoryTheory.Category.{v, u} C] (h : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.FinCategory J] (F : CategoryTheory.Functor J C), Nonempty (CategoryTheory.Limits.Cone F)) : CategoryTheory.IsCofiltered C

If every finite diagram in C admits a cone, then C is cofiltered. It is sufficient to verify this for diagrams whose shape lives in any one fixed universe.

theorem CategoryTheory.IsCofiltered.of_hasFiniteLimits (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.IsCofiltered C

theorem CategoryTheory.IsCofiltered.of_isInitial (C : Type u) [CategoryTheory.Category.{v, u} C] {X : C} (h : CategoryTheory.Limits.IsInitial X) : CategoryTheory.IsCofiltered C

instance CategoryTheory.IsCofiltered.of_hasInitial (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.IsCofiltered C

Equations

• ⋯ = ⋯

@[deprecated CategoryTheory.IsCofiltered.of_hasFiniteLimits]

theorem CategoryTheory.cofiltered_of_hasFiniteLimits (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.IsCofiltered C

Alias of CategoryTheory.IsCofiltered.of_hasFiniteLimits.

theorem CategoryTheory.IsCofiltered.iff_cone_nonempty (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.IsCofiltered C ↔ ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.FinCategory J] (F : CategoryTheory.Functor J C), Nonempty (CategoryTheory.Limits.Cone F)

For every universe w, C is filtered if and only if every finite diagram in C with shape in w admits a cocone.

instance CategoryTheory.isCofilteredOrEmpty_op_of_isFilteredOrEmpty (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] : CategoryTheory.IsCofilteredOrEmpty Cᵒᵖ

Equations

• ⋯ = ⋯

instance CategoryTheory.isCofiltered_op_of_isFiltered (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered C] : CategoryTheory.IsCofiltered Cᵒᵖ

Equations

• ⋯ = ⋯

instance CategoryTheory.isFilteredOrEmpty_op_of_isCofilteredOrEmpty (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] : CategoryTheory.IsFilteredOrEmpty Cᵒᵖ

Equations

• ⋯ = ⋯

instance CategoryTheory.isFiltered_op_of_isCofiltered (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered C] : CategoryTheory.IsFiltered Cᵒᵖ

Equations

• ⋯ = ⋯

theorem CategoryTheory.isCofilteredOrEmpty_of_isFilteredOrEmpty_op (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty Cᵒᵖ] : CategoryTheory.IsCofilteredOrEmpty C

If Cᵒᵖ is filtered or empty, then C is cofiltered or empty.

theorem CategoryTheory.isFilteredOrEmpty_of_isCofilteredOrEmpty_op (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty Cᵒᵖ] : CategoryTheory.IsFilteredOrEmpty C

If Cᵒᵖ is cofiltered or empty, then C is filtered or empty.

theorem CategoryTheory.isCofiltered_of_isFiltered_op (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered Cᵒᵖ] : CategoryTheory.IsCofiltered C

If Cᵒᵖ is filtered, then C is cofiltered.

theorem CategoryTheory.isFiltered_of_isCofiltered_op (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered Cᵒᵖ] : CategoryTheory.IsFiltered C

If Cᵒᵖ is cofiltered, then C is filtered.

instance CategoryTheory.instIsFilteredULiftUliftCategory (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered C] : CategoryTheory.IsFiltered (ULift.{u₂, u} C)

Equations

• ⋯ = ⋯

instance CategoryTheory.instIsCofilteredULiftUliftCategory (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered C] : CategoryTheory.IsCofiltered (ULift.{u₂, u} C)

Equations

• ⋯ = ⋯

instance CategoryTheory.instIsFilteredULiftHomCategory (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered C] : CategoryTheory.IsFiltered (CategoryTheory.ULiftHom C)

Equations

• ⋯ = ⋯

instance CategoryTheory.instIsCofilteredULiftHomCategory (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered C] : CategoryTheory.IsCofiltered (CategoryTheory.ULiftHom C)

Equations

• ⋯ = ⋯

instance CategoryTheory.instIsFilteredAsSmallInstSmallCategoryAsSmall (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered C] : CategoryTheory.IsFiltered (CategoryTheory.AsSmall C)

Equations

• ⋯ = ⋯

instance CategoryTheory.instIsCofilteredAsSmallInstSmallCategoryAsSmall (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered C] : CategoryTheory.IsCofiltered (CategoryTheory.AsSmall C)

Equations

• ⋯ = ⋯