congruence of filters for tendsto

Stream: Is there code for X?

[Max Bobbin]

I don't think this is possible, but I wanted to check. I'm trying to show that if a function tends to the same value along two different filters, then those filters are the same. Of course, under the requirement, the function only hits that value once. I'm not sure how to state that last part in Lean, though so its missing from the mwe. So, for instance, for the function f x =1/x, if f approaches positive infinity along filter 1 and it approaches positive infinity along filter 2, then filter 1 and filter 2 must be the same. I have a feeling that this doesn't work, for a similar reason as to why we have to say an unbounded function has a local minimum, instead of calling it a global minimum.

mwe:

example
{f : ℝ → ℝ}
{l₁ l₂ : filter ℝ}
(h1 : filter.tendsto f l₁ filter.at_top)
(h2 : filter.tendsto f l₂ filter.at_top)
--a premise that f only appraoches filter.at_top once
: l₁ = l₂ :=
begin

end

[Patrick Massot]

This isn't true.

[Jireh Loreaux]

The function f x := 1 / x approaches at_top along many filters.

[Patrick Massot]

And I don't see any true statement that would look like this. Under assumption tendsto f l₁ at_top, any filter l₂ such that l₂ ≤ l₁ will satisfy tendsto f l₂ at_top.

[Jireh Loreaux]

e.g., 𝓝[s] 0 where s is any set of positive numbers whose only limit point is 0.

[Patrick Massot]

Max I think your intuition of filters isn't sufficiently good. Shameless self-advertisement: I think you should try to watch the beginning of https://icerm.brown.edu/video_archive/?play=2899

[Max Bobbin]

Ok, this is what I thought. I'm trying to replicate a derivation from a scientific paper, and they do something similar to this with limits. They want to say that since the function approaches infinity when you approach this, and, since we want the function to approach infinity when we approach this specific constant, these two constants are equal

[Max Bobbin]

It most definitely isn't. I'm just trying to convert filters to my knowledge of limits

[Jireh Loreaux]

that might be possible, just replace arbitrary filters with neighborhood filters.

[Jireh Loreaux]

example
{f : ℝ → ℝ}
{l₁ l₂ : filter ℝ}
(h1 : filter.tendsto f (𝓝 a) filter.at_top)
(h2 : filter.tendsto f (𝓝 b) filter.at_top)
--a premise that f only appraoches filter.at_top once
: a = b := sorry

[Max Bobbin]

I think thats what I mean. As pointed out above, my knowledge of filters is not good, so I just used general filter. However, yes that may be what I mean

[Mario Carneiro]

That theorem sounds false as well: what about something like sec x? This approaches infinity at lots of different points

[Max Bobbin]

My assumption is that the premise I have in the comments would have to bound the function to require it approach the value only once. So for sec x, it would have to be bounded

[Mario Carneiro]

it's bounded, and approaches infinity?

[Max Bobbin]

Would 1/x bounded from (-1,1) still approach infinity at zero?

[Jireh Loreaux]

Mario, there is a premise missing in the code I wrote, it's in a comment.

[Mario Carneiro]

only from above

[Reid Barton]

I'm not sure how you would express that premise in a way that makes your theorem non-trivial (i.e., not just applying the hypotheses to each other)

[Jireh Loreaux]

I think Max want's something like: "this function has a limit of ∞ at a, and is bounded on a complement of a neighborhood of a"

[Mario Carneiro]

sec x is also bounded on a complement of a neighborhood of any of its poles

[Mario Carneiro]

the neighborhood would just encompass both poles

[Mario Carneiro]

oh wait, sec x isn't a good example, (sec x)^2 is better

[Jireh Loreaux]

Sorry, I should have said, "bounded on the complement of anything in a filter basis for 𝓝 a"

[Jireh Loreaux]

I think that makes it work (but I agree it's really messy and there are probably better ways to go about it).

[Mario Carneiro]

I think that has the same issue, you can just choose a weird filter base with a member that happens to span the other poles

[Jireh Loreaux]

not every element of that filter basis can contain the other pole if the filter in question is 𝓝 a

[Jireh Loreaux]

or am I being silly?

[Mario Carneiro]

sure, but you just said there exists one

[Jireh Loreaux]

No, I'm saying this: "there exists a filter basis for 𝓝 a such that for every element in this basis f is bounded on the complement of that set"

[Mario Carneiro]

oh I see, that's more plausible

[Jireh Loreaux]

The filter basis isn't really necessary I guess, you just want bounded on the complement of any neighborhood.

[Mario Carneiro]

That sounds like it should be a general filter definition, some kind of co-tendsto

[Mario Carneiro]

def co_tendsto {α β} (f : α → β) (l₁ : filter α) (l₂ : filter β) :=
  ∀ s ∈ l₁, (f '' sᶜ)ᶜ ∈ l₂

[Jireh Loreaux]

maybe it's that the comap of the cobounded filter along f is contained in 𝓝 a?

[Mario Carneiro]

oh nice, mem_comap_iff_compl says exactly that s ∈ comap f l ↔ (f '' sᶜ)ᶜ ∈ l

[Mario Carneiro]

so this really is co-tendsto

[Jireh Loreaux]

Yeah, I think saying that f : α → β is bounded on complements of neighborhoods of a is equivalent to filter.comap f (cobounded β) ≤ 𝓝 a.

[Mario Carneiro]

This isn't the cobounded filter though

[Mario Carneiro]

I think

[Jireh Loreaux]

what isn't the cobounded filter?

[Mario Carneiro]

the definition I gave is equivalent to l₂.comap f ≤ l₁

[Jireh Loreaux]

oh okay, we're talking about different things I think. You're talking about a "co-tendsto" and I'm still talking about the specific thing.

[Mario Carneiro]

To apply to the specific thing you would use co_tendsto f (N a) at_top

[Mario Carneiro]

I'm not sure exactly what cobounded means here, I found is_cobounded which isn't what we want and cobounded is a typeclass (I have no idea what bornology is)

[Adam Topaz]

docs#bornology.cobounded supposedly?

[Mario Carneiro]

yes, but that's a typeclass like I said, I don't know what the filter actually is

[Adam Topaz]

but the reals have the bornology from the metric.

[Jireh Loreaux]

in a metric space, the cobounded filter consists of exactly the complements of bounded sets.

[Mario Carneiro]

So these are not exactly the same thing, I'm interpreting it as co-bounded above (at_top) and not just metrically co-bounded

[Jireh Loreaux]

Mario, a bornology is just an abstraction of boundedness. It's a collection of sets which is closed under finite unions, subsets and contains all singletons. But in mathlib we dualize it so that it's just a filter smaller than the cofinite filter.

[Jireh Loreaux]

No, I agree, they are not exactly the same thing.

[Jireh Loreaux]

My condition (bounded away from a) seemed like what the OP as getting at (which implies your condition since the at_top filter is smaller than the cobounded filter), and I was just trying to formalize that.

[Mario Carneiro]

So the interesting theorem here is that co_tendsto f l₁ l₂ and tendsto f l₁' l₂ implies l₁ ≤ l₁':

import order.filter.basic

def co_tendsto {α β} (f : α → β) (l₁ : filter α) (l₂ : filter β) :=
  l₂.comap f ≤ l₁

open filter
example {α β} (f : α → β) (l₁ l₁' : filter α) (l₂ : filter β)
  (h1 : tendsto f l₁ l₂) (h2 : co_tendsto f l₁' l₂) : l₁ ≤ l₁' :=
(map_le_iff_le_comap.1 h1).trans h2

[Jireh Loreaux]

I mean, isn't this just something to do with the fact that map and comap are a Galois connection?

[Mario Carneiro]

yes, it's a quite trivial proof as you can see

[Mario Carneiro]

but it means that if co_tendsto f (𝓝 a) at_top and tendsto f (𝓝 b) at_top then 𝓝 a <= 𝓝 b so a = b if the top space is hausdorff

[Jireh Loreaux]

Right, but I mean, it's just a lemma about Galois connections that's already in the library, presumably.

[Mario Carneiro]

I don't think co_tendsto is

[Mario Carneiro]

I mean I just made it up

[Mario Carneiro]

note that map_le_iff_le_comap is the galois connection lemma

[Jireh Loreaux]

sorry, I didn't actually read the proof :sheep:

[Max Bobbin]

Thank you. This is really helpful. I will have to watch those videos linked and learn more so I can understand whats happening

[Jireh Loreaux]

So are you saying we should actually have a definition for co_tendsto, as opposed to the expanded version? I thought we have tendsto primarily because limits occur everywhere. Do we have a lot of use cases for co_tendsto outside of the above lemma?

[Mario Carneiro]

it seems to be similarly "foundational" to tendsto, but it's possible we don't have a lot of applications just like we don't have many uses for coinductive types

[Mario Carneiro]

I would defer to someone else who works with the topology / filter library more for whether this is actually a good idea for a library definition. @Patrick Massot , any thoughts?

[Patrick Massot]

I haven't read this conversation, I'm playing with semantic highlighting. I want to finish writing doc about that and then I'll come back here if I don't forget.

[Mario Carneiro]

The question is whether it would make sense to have a definition for "co-tendsto" (name TBD), which says something like "it is consistent that f converges to l2 at l1". It has a nice duality with tendsto:

• tendsto f l₁ l₂ ↔ l₁ ≤ l₂.comap f
• co_tendsto f l₁ l₂ ↔ l₂.comap f ≤ l₁

[Mario Carneiro]

it will have a ton of monotonicity and galois connection style theorems, so it would actually be some work to add

[Jireh Loreaux]

Mario Carneiro said:

... "it is consistent that f converges to l2 at l1".

That doesn't seem like the right description in English to me, but maybe I'm wrong.

[Mario Carneiro]

It's a bit abstract, not sure how best to gloss it. "f definitely doesn't converge to l2 anywhere other than l1"

[Eric Rodriguez]

Patrick Massot said:

Max I think your intuition of filters isn't sufficiently good. Shameless self-advertisement: I think you should try to watch the beginning of https://icerm.brown.edu/video_archive/?play=2899

thanks for this talk, this was very interesting! just to check the exercises: they are the stuff in https://leanprover-community.github.io/mathematics_in_lean/01_Introduction.html#getting-started, right?

[Jireh Loreaux]

Mario, that reads more correct to me.

[Anatole Dedecker]

The only case I can think of is in the hypothesis of docs#cauchy.comap. I will read this conversation again tomorrow because I’m half sleeping right now

[Patrick Massot]

Now that I posted my semantic highlighting stuff I read that discussion. I'm not convinced the "cotendsto" definition is useful in mathlib.

[Patrick Massot]

Mario Carneiro said:

it seems to be similarly "foundational" to tendsto

I disagree. The definition of tendsto f F G is much nicer because you can phrase it both as map f F ≤ G and F ≤ comap f G. Your definition doesn't have this symmetry.

[Mario Carneiro]

That's true. You can make it higher order, like \forall l', l' <= l₂.comap f -> l' <= l₁ and this latter thing can be rewritten in terms of map (since it's just a tendsto)

[Mario Carneiro]

I suspect there is some name for this operation with adjunctions but I don't know

[Mario Carneiro]

there should also be a version of this on the other side: l₂ ≤ l₁.map f

[Mario Carneiro]

so perhaps it's not a "co-" thing exactly but more like a left adjunction or something like that

[Patrick Massot]

I don't understand what you're trying to say, but it's getting late here.

[Junyan Xu]

I looked into https://ncatlab.org/nlab/show/adjoint+string and https://mathoverflow.net/questions/46877/natural-examples-of-sequences-of-adjoint-functors but found no examples about filters.

[Patrick Massot]

Do you mean you hoped that map f could be right adjoint or comap f could be a left adjoint? This is simply wrong.

[Patrick Massot]

Remember that for maps between complete lattices the adjoint functor theorem is extremely simple to state (and prove): a map is a left (resp. right) adjoint iff it commutes with sup (resp. inf).

[Mario Carneiro]

Fair enough. I think the most I want to claim at this point is that for an arbitrary galois connection u b <= a is a relation you can say, and it sometimes has uses

[Mario Carneiro]

I will certainly agree it's not nearly as well behaved as a <= u b

[Junyan Xu]

Patrick Massot said:

Remember that for maps between complete lattices the adjoint functor theorem is extremely simple to state (and prove): a map is a left (resp. right) adjoint iff it commutes with sup (resp. inf).

That's a nice theorem to know! But it seems we have both docs#filter.comap_infi and docs#filter.comap_supr ?

[Patrick Massot]

Oh yes, I wrote too fast for comap f.

[Patrick Massot]

I never noticed that.

[Junyan Xu]

We only have docs#filter.map_infi_le so the adjunction chain can't be extended that way (at least for general m : α → β).

[Patrick Massot]

Now we have a nice exercise to do: figure out a concrete description of the right-adjoint to comap f

[Patrick Massot]

I'm really tired because I should have remember that set.preimage f is also a left adjoint.

[Patrick Massot]

So it's not surprising that its extension to filters is both a right and a left adjoint.

[Mario Carneiro]

IIRC we actually have the definition for sets

[Mario Carneiro]

docs#set.kern_image

[Patrick Massot]

I have difficulties switching at high frequency between Lean 4 meta-programming and adjunctions at 1am.

[Patrick Massot]

Maybe I just disproved the theory claiming that programming monads belong to category theory.

[Junyan Xu]

So set.image f doesn't admit a left adjoint unless f is a bijection, because it doesn't preserve intersections unless f is injective and doesn't preserve nullary intersection unless f is surjective, and similarly set.kern_image f doesn't admit a right adjoint because it's just (f '' sᶜ)ᶜ.

I've worked out the right adjoint to docs#filter.comap, which I call filter.kern_map, and it also admits a simple description: for m : α → β and f : filter α, (f.kern_map m).sets is exactly the image of f.sets under set.kern_image m. Compare this to (f.map m).sets, which is exactly the preimage of f.sets under set.preimage m. The appearance of docs#set.kern_image is because docs#filter.mem_comap' says exactly (is defeq to) s ∈ g.comap m ↔ s.kern_image m ∈ g.

import order.filter.basic

variables {α β : Type*} (m : α → β)

namespace set

lemma kern_image_eq_compl (s : set α) : s.kern_image m = (m '' sᶜ)ᶜ :=
begin
  ext1,
  simp only [kern_image, mem_set_of_eq, mem_compl_eq, mem_image, not_exists, not_and],
  exact forall_congr (λ _, not_imp_not.symm),
end

variables {s : set α} {t : set β}

lemma image_downward_closed (h : t ⊆ m '' s) : m '' (s ∩ m ⁻¹' t) = t :=
by rwa [image_inter_preimage, inter_eq_right_iff_subset]

lemma kern_image_upward_closed (h : s.kern_image m ⊆ t) : (s ∪ m ⁻¹' t).kern_image m = t :=
begin
  rw [kern_image_eq_compl, compl_subset_comm] at h,
  rw [kern_image_eq_compl, compl_union, ← preimage_compl, image_downward_closed m h, compl_compl],
end

end set

namespace filter

open set

lemma mem_comap'' (s : set α) (g : filter β) : s ∈ g.comap m ↔ s.kern_image m ∈ g := mem_comap'

def kern_map (f : filter α) : filter β :=
{ sets := (kern_image m) '' f.sets,
  univ_sets := ⟨univ, f.univ_sets, by simp [kern_image_eq_compl]⟩,
  sets_of_superset := begin
    rintro _ t ⟨s, hm, rfl⟩ hi,
    use [s ∪ m ⁻¹' t, f.sets_of_superset hm (subset_union_left s _)],
    exact kern_image_upward_closed m hi,
  end,
  inter_sets := begin
    rintro _ _ ⟨s₁, h₁, rfl⟩ ⟨s₂, h₂, rfl⟩,
    use [s₁ ∩ s₂, f.inter_sets h₁ h₂],
    simp only [kern_image_eq_compl, compl_inter, image_union, compl_union],
  end }

lemma comap_kern_map (m : α → β) : galois_connection (comap m) (kern_map m) :=
λ g f, begin
  simp_rw [le_def, mem_comap''], split,
  { rintro h _ ⟨s, hs, rfl⟩, exact h s hs },
  { intros h s hs, exact h _ ⟨s, hs, rfl⟩ },
end

end filter


-- miscellaneous lemmas unnecessary for the Galois connection

namespace set

variables {s : set α} {t : set β}

lemma image_downward_closed' (h : t ⊆ m '' s) : t ∈ set.range (set.image m) :=
by { rw [← inter_eq_right_iff_subset, ← image_inter_preimage] at h, exact ⟨_, h⟩ }

lemma image_downward_closed'' (h : t ⊆ m '' s) : m '' (m ⁻¹' t) = t :=
begin
  rw [← inter_eq_right_iff_subset, ← image_inter_preimage] at h,
  apply subset_antisymm,
  { apply image_preimage_subset },
  { conv_lhs { rw ← h }, apply image_subset, apply inter_subset_right },
end

lemma kern_image_upward_closed' (h : s.kern_image m ⊆ t) : t ∈ set.range (set.kern_image m) :=
begin
  rw [kern_image_eq_compl, compl_subset_comm] at h,
  obtain ⟨s', h'⟩ := image_downward_closed' m h,
  use s'ᶜ, simp only [kern_image_eq_compl, compl_compl, h'],
end

lemma kern_image_upward_closed'' (h : s.kern_image m ⊆ t) : (m ⁻¹' t).kern_image m = t :=
begin
  rw [kern_image_eq_compl, compl_subset_comm] at h,
  rw [kern_image_eq_compl, ← preimage_compl, image_downward_closed'' m h, compl_compl],
end

lemma kern_image_mono {s₁ s₂ : set α} (h : s₁ ⊆ s₂) : s₁.kern_image m ⊆ s₂.kern_image m :=
begin
  simp only [kern_image_eq_compl, compl_subset_compl],
  apply image_subset m (compl_subset_compl.2 h),
end

end set

[Junyan Xu]

Let me also mention
extension of scalars ⊣ restriction of scalars ⊣ coextension of scalars
(#15529, functors between module categories induced by a ring hom)
which is apparently analogous the example
$f^*\dashv f_*\dashv f^!$ (functors between derived categories of sheaves induced by a proper morphism between algebraic varieties, see https://mathoverflow.net/a/46928/3332)

[Patrick Massot]

Nice! It can be used at least to simplify the proof of docs#filter.comap_supr

[Patrick Massot]

But please stop using dot notation for the only purpose of reversing the order you would write things on paper. Once you open the relevant namespaces it's not longer to write map f F than F.map f and it makes it much clear that you are applying the function map f to F, and the same with kern_image m s.

[Junyan Xu]

Haha, I think dot notation allows me to use the declaration name as an infix operator, just like in m '' s; I don't care so much about the order. I used the same notations '', ^-1 and ^k for filters on the scratch paper.

[Eric Rodriguez]

also, there's 50 different maps and now opening namespaces means you can get clashes with map_{xyz} lemmas.

[Patrick Massot]

There are no serious name clashes. I always start Lean 3 files with open set function filter before thinking.

[Patrick Massot]

Junyan, what you do is not the analogue of writing m '' s with an infix '', it is the analogue of writing s '' m to mean m '' s.

[Junyan Xu]

It seems there's special support in pretty printer/doc-gen for this purpose? For example in docs#multiset.sum_map_mul_left, multiset.sum uses dot notation but multiset.map doesn't, even though in the source code dot notation is used everywhere. Or maybe the pretty printer doesn't use dot notation whenever it's not associated to the first argument?

[Yaël Dillies]

Is it pp nodot by any chance?

[Junyan Xu]

The pp_nodot attribute is not added to src#multiset.map at its definition or locally.

[Anatole Dedecker]

Junyan Xu said:

So set.image f doesn't admit a left adjoint unless f is a bijection, because it doesn't preserve intersections unless f is injective and doesn't preserve nullary intersection unless f is surjective, and similarly set.kern_image f doesn't admit a right adjoint because it's just (f '' sᶜ)ᶜ.

I've worked out the right adjoint to docs#filter.comap, which I call filter.kern_map, and it also admits a simple description: for m : α → β and f : filter α, (f.kern_map m).sets is exactly the image of f.sets under set.kern_image m. Compare this to (f.map m).sets, which is exactly the preimage of f.sets under set.preimage m. The appearance of docs#set.kern_image is because docs#filter.mem_comap' says exactly (is defeq to) s ∈ g.comap m ↔ s.kern_image m ∈ g.

import order.filter.basic

variables {α β : Type*} (m : α → β)

namespace set

lemma kern_image_eq_compl (s : set α) : s.kern_image m = (m '' sᶜ)ᶜ :=
begin
  ext1,
  simp only [kern_image, mem_set_of_eq, mem_compl_eq, mem_image, not_exists, not_and],
  exact forall_congr (λ _, not_imp_not.symm),
end

variables {s : set α} {t : set β}

lemma image_downward_closed (h : t ⊆ m '' s) : m '' (s ∩ m ⁻¹' t) = t :=
by rwa [image_inter_preimage, inter_eq_right_iff_subset]

lemma kern_image_upward_closed (h : s.kern_image m ⊆ t) : (s ∪ m ⁻¹' t).kern_image m = t :=
begin
  rw [kern_image_eq_compl, compl_subset_comm] at h,
  rw [kern_image_eq_compl, compl_union, ← preimage_compl, image_downward_closed m h, compl_compl],
end

end set

namespace filter

open set

lemma mem_comap'' (s : set α) (g : filter β) : s ∈ g.comap m ↔ s.kern_image m ∈ g := mem_comap'

def kern_map (f : filter α) : filter β :=
{ sets := (kern_image m) '' f.sets,
  univ_sets := ⟨univ, f.univ_sets, by simp [kern_image_eq_compl]⟩,
  sets_of_superset := begin
    rintro _ t ⟨s, hm, rfl⟩ hi,
    use [s ∪ m ⁻¹' t, f.sets_of_superset hm (subset_union_left s _)],
    exact kern_image_upward_closed m hi,
  end,
  inter_sets := begin
    rintro _ _ ⟨s₁, h₁, rfl⟩ ⟨s₂, h₂, rfl⟩,
    use [s₁ ∩ s₂, f.inter_sets h₁ h₂],
    simp only [kern_image_eq_compl, compl_inter, image_union, compl_union],
  end }

lemma comap_kern_map (m : α → β) : galois_connection (comap m) (kern_map m) :=
λ g f, begin
  simp_rw [le_def, mem_comap''], split,
  { rintro h _ ⟨s, hs, rfl⟩, exact h s hs },
  { intros h s hs, exact h _ ⟨s, hs, rfl⟩ },
end

end filter


-- miscellaneous lemmas unnecessary for the Galois connection

namespace set

variables {s : set α} {t : set β}

lemma image_downward_closed' (h : t ⊆ m '' s) : t ∈ set.range (set.image m) :=
by { rw [← inter_eq_right_iff_subset, ← image_inter_preimage] at h, exact ⟨_, h⟩ }

lemma image_downward_closed'' (h : t ⊆ m '' s) : m '' (m ⁻¹' t) = t :=
begin
  rw [← inter_eq_right_iff_subset, ← image_inter_preimage] at h,
  apply subset_antisymm,
  { apply image_preimage_subset },
  { conv_lhs { rw ← h }, apply image_subset, apply inter_subset_right },
end

lemma kern_image_upward_closed' (h : s.kern_image m ⊆ t) : t ∈ set.range (set.kern_image m) :=
begin
  rw [kern_image_eq_compl, compl_subset_comm] at h,
  obtain ⟨s', h'⟩ := image_downward_closed' m h,
  use s'ᶜ, simp only [kern_image_eq_compl, compl_compl, h'],
end

lemma kern_image_upward_closed'' (h : s.kern_image m ⊆ t) : (m ⁻¹' t).kern_image m = t :=
begin
  rw [kern_image_eq_compl, compl_subset_comm] at h,
  rw [kern_image_eq_compl, ← preimage_compl, image_downward_closed'' m h, compl_compl],
end

lemma kern_image_mono {s₁ s₂ : set α} (h : s₁ ⊆ s₂) : s₁.kern_image m ⊆ s₂.kern_image m :=
begin
  simp only [kern_image_eq_compl, compl_subset_compl],
  apply image_subset m (compl_subset_compl.2 h),
end

end set

Has any of this been PR-ed? I know it sounds crazy, but I need this for defining the space of test functions on an open set $\Omega$ of a finite dimensional vector space $E$ in a convenient way!

Because I don't want to have "extensions by zero" all the time, I want $\mathcal{D}(\Omega)$ to be the type of smooth functions defined on all of $E$ and whose docs#tsupport is a compact subset of $\Omega$. The problem is to encode the last condition in a convenient way that doesn't involve duplicating the API of docs#has_compact_support for this relative case (for example, a naive combination of docs#has_compact_support and "support $\subseteq\Omega$" makes proving the sum of two test functions is a test function annoying).

So I want to apply the same trick as docs#has_compact_support_iff_eventually_eq but with a different filter, namely ⨅ (s : set S) (h : is_compact s), 𝓟 (coe '' s : set α)ᶜ (I am in a normed space so docs#cocompact = docs#coclosed_compact). I've long been wondering if this could be defined from docs#cocompact by pure filter-theoretic nonsense, and I just realized that this is exactly kern_map coe cocompact, which is way more satisfying!

[Junyan Xu]

No I haven't PR'd. Glad that the definition finds some actual use! I doubt I have time for the PR, and I think it's better that someone more familiar with the filter library PRs it, especially since you are probably adding more APIs to it. As shown in the proof above, the Galois connection is essentially known, as docs#filter.mem_comap'' in mathlib, and the main content of my work was to show (kern_image m) '' f.sets forms a filter. I also worked out some more relationships back then:
image.png

[Junyan Xu]

The diagonal inclusion/generation are essneitally known in mathlib, and the middle top two are used in induced/coinduced topology, but I can't think of what the bottom row is good for.