Zulip Chat Archive

Stream: maths

Topic: directed map


view this post on Zulip 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})

view this post on Zulip Mario Carneiro (Nov 06 2018 at 06:08):

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

view this post on Zulip Mario Carneiro (Nov 06 2018 at 06:11):

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

view this post on Zulip Mario Carneiro (Nov 06 2018 at 06:11):

"prefilter" just occurred to me

view this post on Zulip Patrick Massot (Nov 06 2018 at 06:57):

What is a preorder filter?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip Floris van Doorn (Nov 06 2018 at 16:14):

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

view this post on Zulip Sebastien Gouezel (Nov 06 2018 at 16:15):

order_filter and filter?

view this post on Zulip 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