Filtered categories — categories whose finite diagrams have a cocone. More...

#include <concepts>
#include <functional>
import dedekind.category:thin;

Include dependency graph for filtered.cppm:

Classes
struct	dedekind::category::is_directed< T, Rel >
	Trait to mark a relation as directed: every pair of elements has an upper bound. More...
struct	dedekind::category::is_directed< T, Rel >
	Discovery: types may opt in via a nested `is_directed_v` template member, mirroring the `is_reflexive_v` / `is_transitive_v` / `is_antisymmetric_v` discovery pattern. More...
struct	dedekind::category::is_directed< T, std::less_equal< T > >
	A reflexive, connex `<=` is directed: of `a` and `b` one is above the other, and it bounds both (reflexivity bounds itself). Derived from the certificates (:mereology), not from the syntactic `std::totally_ordered<T>`, which `double` satisfies (#1043). More...
struct	dedekind::category::is_codirected< T, Rel >
	Trait to mark a relation as codirected: every pair of elements has a lower bound. More...
struct	dedekind::category::is_codirected< T, Rel >
	Discovery: types may opt in via a nested `is_codirected_v` template member, mirroring the sibling trait patterns. More...
struct	dedekind::category::is_codirected< T, std::less_equal< T > >
	A reflexive, connex `<=` is codirected: the lesser of `a` and `b` bounds both from below (#1043, as `is_directed`). More...

Namespaces
namespace	dedekind::category

Concepts
concept	dedekind::category::IsDirected
	Formal verification of the directedness axiom: ∀ a, b ∈ T. ∃ c ∈ T. Rel(a, c) ∧ Rel(b, c).
concept	dedekind::category::IsCodirected
	Formal verification of the codirectedness axiom: ∀ a, b ∈ T. ∃ c ∈ T. Rel(c, a) ∧ Rel(c, b).
concept	dedekind::category::IsFilteredCategory
	A thin category whose every finite subset of objects has an upper bound (directedness).

Variables
template<typename T, typename Rel>
constexpr bool	dedekind::category::is_directed_v = is_directed<T, Rel>::value
template<typename T, typename Rel>
constexpr bool	dedekind::category::is_codirected_v = is_codirected<T, Rel>::value

Detailed Description

Filtered categories — categories whose finite diagrams have a cocone.

@partition :filtered

filtered__Categorical_Definition

A filtered category is one in which every finite diagram has a cocone (an upper bound, in poset terms). The standard textbook definition is three-fold:

The category is nonempty.
For every pair of objects (a, b), there exists an object c and morphisms a → c, b → c (binary upper bound).
For every parallel pair f, g : a → b, there exists h : b → c equalising them.

filtered__Thin_Case

In a thin category (hom-sets propositional), the third clause is automatic: parallel morphisms are equal by thinness, so any choice of h coequalises trivially. Filtered then reduces to:

nonempty + ∀ a, b ∈ T. ∃ c ∈ T. Rel(a, c) ∧ Rel(b, c)

By induction on finite-subset size, the binary case extends to arbitrary finite subsets — that's exactly the directedness axiom captured by is_directed_v (below).

filtered__Form_Chain_Row_3

IsFilteredCategory is row 3 of the lattice Form-chain (#698):

IsThinCategory        (row 1, preorder)
   ↓ + antisymmetry
IsPosetal             (row 2, poset)
 
IsThinCategory        (row 1, parallel branch)
   ↓ + directedness
IsFilteredCategory    (row 3, this partition)
 
row 2 + row 3 + cofiltered + universality
   ↓
IsLatticeCategory     (row 4, Form-chain home — Slice 3)

Filtered cats are not refinements of posetal — they need only thin + directed, NOT antisymmetric. The textbook example of a filtered non-poset is a preorder with two distinct maximal elements that are mutually ≤; under thin+directed it counts as filtered, but it is not a poset.

filtered__Why_Filtered_Matters

Filtered categories are the natural indexing shape for filtered colimits, which preserve finite limits. In the context of :sets::mereology and the subobject classifier reading (#698):

Unrestricted-fusion mereology (Leśniewskian gunk-friendly variants) needs arbitrary colimits in Sub(X) — these require filtered cocompleteness of the ambient.
Filtered Ind-objects on Sub(X) name "limits of finite parts" — the categorical machinery behind "arbitrary fusion".

Whether the project ever needs this gunk-axis machinery is open; :filtered names the row regardless, so the IsLatticeCategory assembly in Slice 3 can encode the faithful inclusion IsLatticeCategory ⊊ IsFilteredCategory definitionally.

filtered__Boolean_Witness

bool with std::less_equal is filtered: true is the upper bound of every pair (its reflexive, connex <= witnesses is_directed_v through the specialisation below). The 2-element thin category is also filtered.

See also: https://en.wikipedia.org/wiki/Filtered_category; https://ncatlab.org/nlab/show/filtered+category

Copyright: 2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.

Note: "Pas à pas, on va loin." (Step by step, one goes far.) — French proverb; here the steps are slices of #698.

Classes

Namespaces