Directed systems

Stream: mathlib4

[Antoine Chambert-Loir]

In mathlib (outside of the category theory framework), directed systems (docs#DirectedSystem) are defined as

class DirectedSystem {ι : Type u_1} [Preorder ι] (F : ι → Type u_4) (f : ⦃i j : ι⦄ → i ≤ j → F i → F j) :
Prop

which contains two fields expressing the functor property ($f_{ii}$ is the identity and $f_{jk}\circ f_{ij}=f_{ik}$).

Now, when a directed system is used, the directed system property is stored as a type class but one needs to repeat a lot of information. For example, to indicate its limit in docs#DirectLimit, one has to copy Fand f . I find this annoying to write and painful to use.

I propose to refactor this so as to make directed systems a definition, containing the fields F and f, and the functorial properties, keeping the dot notation so that one can say, if Dis some directed system, D.limit. I expect that it will be easier to formulate and use directed systems. The bulk of the constructions shouldn't change though. (And it still will only be applicable to algebraic cases of universal algebra where the direct limit of the directed system has naturally an algebraic structure of the same nature as the objects in the system.)

Does this make sense? @Junyan Xu , what do you think?

[Joël Riou]

It is probably reasonable to redefine DirectedSystem as functors ι ⥤ Type u and factor out the duplication of code between the construction in Order.DirectedInverseSystem and the construction in CategoryTheory.Limits.TypesFiltered.