directed map

Stream: maths

[Mario Carneiro]

Does this concept look familiar to anyone?

variables [preorder α] [preorder β] (m : α → β)
class directed_map : Prop :=
(mono : monotone m)
(dir : ∀ x, directed_on (≥) {a | x ≤ m a})

[Mario Carneiro]

Turns out this is what you need to map a preorder filter. It's a category

[Mario Carneiro]

By the way, does anyone have any naming suggestions for preorder filters vs set filters?

[Mario Carneiro]

"prefilter" just occurred to me

[Patrick Massot]

What is a preorder filter?

[Mario Carneiro]

It is a subset of a preorder which is nonempty, upward closed, and has an element below any two elements in the filter (downward directed)

[Mario Carneiro]

basically you generalize the part about filters being sets of sets to sets in a more general ordered structure

[Reid Barton]

It looks similar to (and implies) the notion of (co)final functor, but I don't remember seeing this exact notion before.

[Reid Barton]

I like the name "directed map", because you have the property: \a is directed if and only if the unique map \a \to unit is directed

[Reid Barton]

"prefilter" however strikes me as a word which should mean a filter minus some property, or something like a filter basis. Compare presheaf/sheaf, (historically) prescheme/scheme = (scheme/separated scheme).

[Reid Barton]

I suppose using filter for both cases is infeasible, or you wouldn't be asking the question?

[Floris van Doorn]

filter and set_filter? Or is renaming the current one out of the question?

[Sebastien Gouezel]

order_filter and filter?

[Reid Barton]

We could also make use of namespacing perhaps