# mathlibdocumentation

category_theory.filtered

# 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 category_theory/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 [fin_category J] [is_filtered 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 provide all of the above API for cofiltered categories.

In category_theory.limits.filtered_colimit_commutes_finite_limit we show that filtered colimits commute with finite limits.

## Future work #

• Forgetful functors for algebraic categories typically preserve filtered colimits.
@[class]
structure category_theory.is_filtered_or_empty (C : Type u)  :
Prop
• cocone_objs : ∀ (X Y : C), ∃ (Z : C) (f : X Z) (g : Y Z), true
• cocone_maps : ∀ ⦃X Y : C⦄ (f g : X Y), ∃ (Z : C) (h : Y Z), f h = g h

A category is_filtered_or_empty 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
@[class]
structure category_theory.is_filtered (C : Type u)  :
Prop
• to_is_filtered_or_empty :
• nonempty :

A category is_filtered 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
@[instance]
@[instance]
@[instance]
def category_theory.is_filtered.max {C : Type u} (j 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 is_filtered.

Equations
def category_theory.is_filtered.left_to_max {C : Type u} (j j' : C) :

left_to_max j j' is an arbitrarily choice of morphism from j to max j j', whose existence is ensured by is_filtered.

Equations
def category_theory.is_filtered.right_to_max {C : Type u} (j j' : C) :

right_to_max j j' is an arbitrarily choice of morphism from j' to max j j', whose existence is ensured by is_filtered.

Equations
def category_theory.is_filtered.coeq {C : Type u} {j j' : C} (f f' : j j') :
C

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

Equations
def category_theory.is_filtered.coeq_hom {C : Type u} {j j' : C} (f f' : j j') :

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

Equations
@[simp]
theorem category_theory.is_filtered.coeq_condition {C : Type u} {j j' : C} (f f' : j j') :

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

@[simp]
theorem category_theory.is_filtered.coeq_condition_assoc {C : Type u} {j j' : C} (f f' : j j') {X' : C} (f'_1 : X') :
f = f'
theorem category_theory.is_filtered.sup_objs_exists {C : Type u} (O : finset C) :
∃ (S : C), ∀ {X : C}, X Ononempty (X S)

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

theorem category_theory.is_filtered.sup_exists {C : Type u} (O : finset C) (H : finset (Σ' (X Y : C) (mX : X O) (mY : 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}, X, Y, mX, mY, f⟩ Hf 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.

def category_theory.is_filtered.sup {C : Type u} (O : finset C) (H : finset (Σ' (X Y : C) (mX : X O) (mY : 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
def category_theory.is_filtered.to_sup {C : Type u} (O : finset C) (H : finset (Σ' (X Y : C) (mX : X O) (mY : Y O), X Y)) {X : C} (m : X O) :

The morphisms to sup O H.

Equations
theorem category_theory.is_filtered.to_sup_commutes {C : Type u} (O : finset C) (H : finset (Σ' (X Y : C) (mX : X O) (mY : Y O), X Y)) {X Y : C} (mX : X O) (mY : Y O) {f : X Y} (mf : X, Y, mX, mY, f⟩ H) :

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

theorem category_theory.is_filtered.cocone_nonempty {C : Type u} {J : Type v} (F : J C) :

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

def category_theory.is_filtered.cocone {C : Type u} {J : Type v} (F : J C) :

An arbitrary choice of cocone over F : J ⥤ C, for fin_category J and is_filtered C.

Equations
theorem category_theory.is_filtered.of_right_adjoint {C : Type u} {D : Type u₁} {L : D C} {R : C D} (h : L R) :

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

theorem category_theory.is_filtered.of_is_right_adjoint {C : Type u} {D : Type u₁} (R : C D)  :

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

theorem category_theory.is_filtered.of_equivalence {C : Type u} {D : Type u₁} (h : C D) :

Being filtered is preserved by equivalence of categories.

@[class]
structure category_theory.is_cofiltered_or_empty (C : Type u)  :
Prop
• cocone_objs : ∀ (X Y : C), ∃ (W : C) (f : W X) (g : W Y), true
• cocone_maps : ∀ ⦃X Y : C⦄ (f g : X Y), ∃ (W : C) (h : W X), h f = h g

A category is_cofiltered_or_empty 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
@[class]
structure category_theory.is_cofiltered (C : Type u)  :
Prop
• to_is_cofiltered_or_empty :
• nonempty :

A category is_cofiltered 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.
Instances
@[instance]
@[instance]
def category_theory.is_cofiltered.min {C : Type u} (j 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 is_cofiltered.

Equations
def category_theory.is_cofiltered.min_to_left {C : Type u} (j j' : C) :

min_to_left j j' is an arbitrarily choice of morphism from min j j' to j, whose existence is ensured by is_cofiltered.

Equations
def category_theory.is_cofiltered.min_to_right {C : Type u} (j j' : C) :

min_to_right j j' is an arbitrarily choice of morphism from min j j' to j', whose existence is ensured by is_cofiltered.

Equations
def category_theory.is_cofiltered.eq {C : Type u} {j j' : C} (f f' : j j') :
C

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

Equations
def category_theory.is_cofiltered.eq_hom {C : Type u} {j j' : C} (f f' : j j') :

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

Equations
@[simp]
theorem category_theory.is_cofiltered.eq_condition_assoc {C : Type u} {j j' : C} (f f' : j j') {X' : C} (f'_1 : j' X') :
f f'_1 = f' f'_1
@[simp]
theorem category_theory.is_cofiltered.eq_condition {C : Type u} {j j' : C} (f f' : j j') :

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

theorem category_theory.is_cofiltered.inf_objs_exists {C : Type u} (O : finset C) :
∃ (S : C), ∀ {X : C}, X Ononempty (S X)

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

theorem category_theory.is_cofiltered.inf_exists {C : Type u} (O : finset C) (H : finset (Σ' (X Y : C) (mX : X O) (mY : 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}, X, Y, mX, mY, f⟩ HT 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.

def category_theory.is_cofiltered.inf {C : Type u} (O : finset C) (H : finset (Σ' (X Y : C) (mX : X O) (mY : 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
def category_theory.is_cofiltered.inf_to {C : Type u} (O : finset C) (H : finset (Σ' (X Y : C) (mX : X O) (mY : Y O), X Y)) {X : C} (m : X O) :

The morphisms from inf O H.

Equations
theorem category_theory.is_cofiltered.inf_to_commutes {C : Type u} (O : finset C) (H : finset (Σ' (X Y : C) (mX : X O) (mY : Y O), X Y)) {X Y : C} (mX : X O) (mY : Y O) {f : X Y} (mf : X, Y, mX, mY, f⟩ H) :

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

theorem category_theory.is_cofiltered.cone_nonempty {C : Type u} {J : Type v} (F : J C) :

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

def category_theory.is_cofiltered.cone {C : Type u} {J : Type v} (F : J C) :

An arbitrary choice of cone over F : J ⥤ C, for fin_category J and is_cofiltered C.

Equations
theorem category_theory.is_cofiltered.of_left_adjoint {C : Type u} {D : Type u₁} {L : C D} {R : D C} (h : L R) :

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

theorem category_theory.is_cofiltered.of_is_left_adjoint {C : Type u} {D : Type u₁} (L : C D)  :

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

theorem category_theory.is_cofiltered.of_equivalence {C : Type u} {D : Type u₁} (h : C D) :

Being cofiltered is preserved by equivalence of categories.

@[instance]
@[instance]