Timeline for Reference request: filter tends to filter along map
Current License: CC BY-SA 4.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 13, 2019 at 22:15 | comment | added | Todd Trimble | @PatrickMassot Thanks for clarifying. | |
| Mar 13, 2019 at 21:46 | comment | added | Patrick Massot | @ToddTrimble this is an interesting paper, but it makes to reference to limits. I'm looking for a source which explicitly says: you can compose many kinds of limits using the filter functor. | |
| Mar 12, 2019 at 13:28 | comment | added | Todd Trimble | @PatrickMassot If you mean a reference for the filter functor: this has been known essentially forever, but here is one (which characterizes the algebras of the filter monad as continuous lattices): books.google.com/… | |
| Mar 12, 2019 at 7:45 | comment | added | Patrick Massot | This reference still doesn't seem to cover the main use of this idea, because it doesn't fix the underlying set. Say you want to prove that limits compose (limits of sequences, of function at a point, at infinity, from the left or right, all in one proof...). With Kevin notations, it means for all $f: X\to Y$, $g : Y \to Z$, and filters $F$, $G$, $H$ on $X$, $Y$ and $Z$, $F\to^f G$ and $G \to^g H$ implies $F \to^{g\circ f} H$. Here you need that $X \mapsto Filter(X)$ is a functor from $\mathbf{Set}$ to the category of posets. I'd like to know a reference for this observation. | |
| Mar 11, 2019 at 23:44 | comment | added | Andreas Blass | And I still don't have a good name for these morphisms. What does exist, though I apparently didn't know about it when I wrote that paper, is a standard terminology for "there exists a morphism from $F$ to $G$"; this is the Katetov ordering of filters, written $F\geq_KG$. (Its specialization to ultrafilters is called the Rudin-Keisler ordering.) So one could express "tendsto $\phi F G$" by "$\phi$ witnesses that $F\geq_KG$"; I would not, however, recommend expressing it this way, especially in an introductory talk. | |
| Mar 11, 2019 at 22:52 | comment | added | Kevin Buzzard | Yes, this is the one! In the definition in the original Lean code there is $\le$ and in the paper there is $\supseteq$, but these are the same thing because the partial order on filters is defined this way (the more sets there are, the smaller the "limit" is). Unfortunately I still don't see notation, because Blass defines the category and then just refers to the arrows as morphisms or $\mathcal{F}$-morphisms :-) | |
| Mar 11, 2019 at 22:47 | vote | accept | Kevin Buzzard | ||
| Mar 11, 2019 at 22:16 | history | edited | Joseph Van Name | CC BY-SA 4.0 |
added 9 characters in body
|
| Mar 11, 2019 at 22:11 | history | answered | Joseph Van Name | CC BY-SA 4.0 |