Filtered categories #
A category is filtered if every finite diagram admits a cocone. We give a simple characterisation of this condition as
- for every pair of objects there exists another object "to the right",
- for every pair of parallel morphisms there exists a morphism to the right so the compositions are equal, and
- 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 often 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 objectZreceiving maps from all of them, so that all the triangles (one edge from the finite set, two from morphisms toZ) commute. This formulation is often more useful in practice. We give two variants,sup_exists', which takes a single finset of objects, and a finset of morphisms (bundled with their sources and targets), andsup_exists, which takes a finset of objects, and an indexed family (indexed by source and target) of finsets of morphisms.
Future work #
- Finite limits commute with filtered colimits
- Forgetful functors for algebraic categories typically preserve filtered colimits.
- 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
- for every pair of objects there exists another object "to the right", and
- for every pair of parallel morphisms there exists a morphism to the right so the compositions are equal.
- to_is_filtered_or_empty : category_theory.is_filtered_or_empty C
- nonempty : nonempty C
A category is_filtered if
- for every pair of objects there exists another object "to the right",
- for every pair of parallel morphisms there exists a morphism to the right so the compositions are equal, and
- there exists some object.
See https://stacks.math.columbia.edu/tag/002V. (They also define a diagram being filtered.)
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
- category_theory.is_filtered.max j j' = _.some
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
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
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
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
coeq_condition f f', for morphisms f f' : j ⟶ j', is the proof that
f ≫ coeq_hom f f' = f' ≫ coeq_hom f f'.
Any finite collection of objects in a filtered category has an object "to the right".
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 X = T Y, for f : X ⟶ Y in the finset.
An arbitrary choice of object "to the right"
of a finite collection of objects O and morphisms H,
making all the triangles commute.
Equations
The morphisms to sup O H.
Equations
- category_theory.is_filtered.to_sup O H m = Exists.some _ m
The triangles of consisting of a morphism in H and the maps to sup O H commute.
If we have is_filtered C, then for any functor F : J ⥤ C with fin_category J,
there exists a cocone over F.
An arbitrary choice of cocone over F : J ⥤ C, for fin_category J and is_filtered C.
Equations
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.