## Stream: maths

### Topic: directed map

#### Mario Carneiro (Nov 06 2018 at 05:58):

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 (Nov 06 2018 at 06:08):

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

#### Mario Carneiro (Nov 06 2018 at 06:11):

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

#### Mario Carneiro (Nov 06 2018 at 06:11):

"prefilter" just occurred to me

#### Patrick Massot (Nov 06 2018 at 06:57):

What is a preorder filter?

#### Mario Carneiro (Nov 06 2018 at 07:02):

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 (Nov 06 2018 at 07:03):

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

#### Reid Barton (Nov 06 2018 at 15:39):

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

#### Reid Barton (Nov 06 2018 at 15:40):

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 (Nov 06 2018 at 15:47):

"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 (Nov 06 2018 at 15:50):

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

#### Floris van Doorn (Nov 06 2018 at 16:14):

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

#### Sebastien Gouezel (Nov 06 2018 at 16:15):

order_filter and filter?

#### Reid Barton (Nov 06 2018 at 16:17):

We could also make use of namespacing perhaps

Last updated: May 19 2021 at 03:22 UTC