co-bounded filter

Stream: Is there code for X?

[Jireh Loreaux]

I'm not sure what the appropriate name for this would be, but in a normed space do we have a definition of the filter of co-bounded sets (those whose complement is bounded)? Or is this just filter.comap norm at_top?

[Kevin Buzzard]

All this co stuff makes me wonder whether we should just formalise ideals (in the sense of "the complements of all these sets give you a filter") and then have the finite ideal, the bounded ideal, the null measure ideal...

[Kevin Buzzard]

We have closed sets in topology after all

[Yury G. Kudryashov]

AFAIK, we don't. You should define it in a pseudo_metric_space as { sets := {s | bounded sᶜ}, ... }

[Yury G. Kudryashov]

Currently we have

• docs#filter.cofinite
• docs#filter.cocompact
• docs#filter.coclosed_compact
• docs#filter.coprod, docs#filter.Coprod

[Kevin Buzzard]

Is this concrete definition better than Jireh's mathematically extremely satisfying comap definition?

[Kevin Buzzard]

Ie is it somehow better to make the concrete definition and then prove it's the comap?

[Yury G. Kudryashov]

The main advantage of my definition is that it works in any metric space.

[Yury G. Kudryashov]

You can use comap (dist x) at_top but it needs a base point.

[Kevin Buzzard]

I see. So make the def in full generality and then prove that in some special cases it's the comap. Sounds like a fine PR @Jireh Loreaux !

[Yury G. Kudryashov]

Clearly, we need @[simp] lemmas that simplify comap norm at_top, comap (dist x) at_top, and comap (λ x, dist x y) at_top to cobounded. BTW, we have a few lemmas about these comap filters in metric_space.basic that should be reformulated in terms of cobounded.

[Yury G. Kudryashov]

AFAIR, we prove cobounded ≤ cocompact and cobounded = cocompact in a proper space.

[Jireh Loreaux]

where should I put it? topology/metric_space/basic? or a new file?

[Jireh Loreaux]

yes, we have those results: docs#comap_dist_right_at_top_le_cocompact and it's left and eq versions.

[Yury G. Kudryashov]

I think that metric_space.basic is already long enough. Could you please put it into a new file and move the existing lemmas to this file?

[Yury G. Kudryashov]

Of course, instead of the old lemmas we should have cobounded_le_cocompact and comap_dist_left/right_eq_cobounded/comap_norm_eq_cobounded (or comap_dist_left/right_at_top/comap_norm_at_top)

[Adam Topaz]

There is a notion of a bornology, which is a way to formalize the notion of "boundedness". Should we think about defining bornological spaces?
https://en.wikipedia.org/wiki/Bornological_space
Presumably this is the right context for such a co-bounded filter?

[Patrick Massot]

It's not obscure at all, it's in Bourbaki!

[Adam Topaz]

I'm speaking as an arithmetic geometer, sorry ;) Fixed

[Patrick Massot]

I certainly never used that in my life, but it's still there :grinning:

[Yaël Dillies]

Wow, I love this Wikipedia page. "bornivorous"

[Yaël Dillies]

It's genuinely quite related to what Moritz and I have been doing over at file#analysis/seminorm

[Yaël Dillies]

Sounds precisely like the kind of generalization mathlib enjoys. Who is volunteering?

[Jireh Loreaux]

Yeah, they had fun with the names there. I guess I'm volunteering, but I'm not promising it soon. It doesn't seem like there is any rush anyway.

[Jireh Loreaux]

Unless it actually is important for your seminorm stuff, in which case I can make it a priority.

[Jireh Loreaux]

For the structure projections, I was considering is_borne (or is_borné) instead of is_bounded to potentially avoid confusion with other things in mathlib. Thoughts?

[Yaël Dillies]

Oh btw I have quite an idea of what should be there. bornological_space should be based on topological_space, bornological_module should follow normed_space.

[Yaël Dillies]

The projection should supersede docs#metric.bounded and you'll need docs#metric_space to extend bornological_space to avoid the diamond with prod, but both can (and indeed should) wait for another PR.

[Yaël Dillies]

In general, the API should closely follow topological_space.

[Yaël Dillies]

I'm taking care of bornivore. It is really orthogonal to the rest.

[Adam Topaz]

One might hope that the existing instances of is_bounded are all cases where the ambient object can be given a natural bornology, so perhaps is_bounded should be the way to go?

[Yaël Dillies]

What are you referring to, Adam? is_bounded isn't a thing. docs#metric.bounded?

[Adam Topaz]

I'm responding to @Jireh Loreaux 's last comment

[Yaël Dillies]

But there's no instance of is_bounded :thinking:

[Jireh Loreaux]

Yes, I'm literally copying from topological_space and making the necessary modifications.

[Jireh Loreaux]

Perhaps there is no is_bounded, but for some reason I thought there was.

[Yaël Dillies]

AFAIA, there's docs#set.bounded, docs#metric.bounded and docs#is_bounded_linear_map

[Kyle Miller]

(The definition of a bornology looks like an order ideal that contains the ideal of finite sets, but the Wikipedia page doesn't seem to mention anything about ideals -- am I missing something?)

[Adam Topaz]

Regardless of whether it exists, we have various conditions stipulating some sort of boundedness in different contexts. Metric spaces is one such example. The point I was making is that with the notion of bornologocal spaces, I am hoping that those various notions of boundedness actually define a bornology, so that we can indeed have a unified is_bounded prop which will encompass all of those ad hoc notions that we currently have.

[Yaël Dillies]

Yes, the covering condition, Kyle.

[Yaël Dillies]

And my answer is that this won't happen, Adam. The one thing I see it will generalize is metric.bounded.

[Kyle Miller]

Yaël Dillies said:

Yes, the covering condition, Kyle.

If an ideal contains the ideal of finite sets, then the covering condition is satisfied (and conversely).

[Adam Topaz]

I haven't looked through the library, but if this really the case, then that's even more of a reason to just use is_bounded as opposed to is_borne...

[Yaël Dillies]

I agree it's a nice topological_space-like name, is_borneis nice too, and more endemic.

[Adam Topaz]

Note bounded linear maps are linear maps which are also morphisms of bornological spaces (I think?)

[Yaël Dillies]

Oh, I think you're right.

[Jireh Loreaux]

So, unlike topological spaces, where ∅ is automatically an element, the axioms for bornological spaces don't guarantee that the bornology is nonempty unless the type is itself nontrivial. Should I just add the condition is_bounded ∅ as an axiom (my preference) so we never have to pass around needless nontrivial assumptions?

[Adam Topaz]

I think that's a reasonable assumption, but I don't have enough experience with these objects to say for sure.

[Adam Topaz]

I suppose we want the poset of bornologies to have \top, which should be the the set of finite subsets, right?

[Adam Topaz]

And for this to work for the empty type, we need the empty set to be bounded.

[Jireh Loreaux]

I mean, it is literally only an issue when the type is empty. Yes, I think this reasoning regarding top makes sense.

[Adam Topaz]

Actually it seems that the order on bornologies should be reversed from what we have in mathlib for the order on topological space structures.

[Adam Topaz]

Because a morphism is supposed to map a bounded set to a bounded set.

[Adam Topaz]

So this might be bot :)

[Jireh Loreaux]

ah, okay

[Kyle Miller]

For what it's worth, this is equivalent to the definition of a bornology that includes the empty set:

structure bornology (α : Type*) :=
(infty : filter α) -- the "filter at infinity"
(le_cofinite : infty ≤ cofinite)

and this is the definition of a bounded function with respect to bornologies b and b' on α and α':

def is_bounded (f : α → α') : Prop :=
b'.infty.comap f ≤ b.infty

proof of equivalence to other definition

import order.filter.cofinite

open filter

structure bornology (α : Type*) :=
(infty : filter α)
(le_cofinite : infty ≤ cofinite)

variables {α : Type*} (b : bornology α)
variables {α' : Type*} (b' : bornology α')

def is_bounded (f : α → α') : Prop :=
b'.infty.comap f ≤ b.infty

def bornology.ideal : set (set α) :=
{B : set α | Bᶜ ∈ b.infty}

lemma bornology.covers : ⋃₀ b.ideal = set.univ :=
begin
  ext x,
  simp,
  use {x},
  simp [bornology.ideal],
  have := b.le_cofinite,
  rw le_def at this,
  apply this,
  exact (set.finite_singleton x).compl_mem_cofinite,
end

lemma bornology.inclusion {B : set α} (hB : B ∈ b.ideal) {A : set α} (hA : A ⊆ B) : A ∈ b.ideal :=
mem_of_superset hB (set.compl_subset_compl.mpr hA)

lemma bornology.unions {B B' : set α} (hB : B ∈ b.ideal) (hB' : B' ∈ b.ideal) :
  B ∪ B' ∈ b.ideal :=
begin
  simp only [bornology.ideal, set.compl_union, set.mem_set_of_eq] at *,
  exact inter_mem hB hB',
end

lemma is_bounded_iff (f : α → α') :
  is_bounded b b' f ↔ ∀ (B : set α), B ∈ b.ideal → f '' B ∈ b'.ideal :=
begin
  simp [is_bounded, le_def, bornology.ideal],
  split,
  { rintro h B hB,
    obtain ⟨B', hB', h⟩ := h _ hB,
    have : B' ⊆ (f '' B)ᶜ,
    { intros x hx,
      simp,
      rintros x' hx' rfl,
      have : x' ∈ f⁻¹' B',
      exact hx,
      exact h this hx', },
    exact mem_of_superset hB' this, },
  { rintro h B hB,
    specialize h Bᶜ (by simpa using hB),
    refine ⟨_, h, _⟩,
    intro x,
    simp,
    intro h,
    specialize h x,
    exact set.not_not_mem.mp (imp_not_comm.mp h rfl), },
end

def bornology.of {α : Type*} (ideal : set (set α))
  (empty_mem : ∅ ∈ ideal)
  (covers : ⋃₀ ideal = set.univ)
  (incl : ∀ (B ∈ ideal) (A ⊆ B), A ∈ ideal)
  (union : ∀ (B B' ∈ ideal), B ∪ B' ∈ ideal) : bornology α :=
{ infty :=
  { sets := {B : set α | Bᶜ ∈ ideal},
    univ_sets := by simp [empty_mem],
    sets_of_superset := begin
      intros A A' hA h,
      rw ←set.compl_subset_compl at h,
      rw set.mem_set_of_eq at ⊢ hA,
      exact incl _ hA _ h,
    end,
    inter_sets := begin
      intros A A' hA hA',
      rw set.mem_set_of_eq at ⊢ hA hA',
      rw set.compl_inter,
      exact union _ hA _ hA',
    end },
  le_cofinite := begin
    rw le_def,
    intro A,
    simp,
    generalize : Aᶜ = A',
    intro h,
    refine h.dinduction_on _ (λ x s hx hs h, _),
    { exact empty_mem, },
    { rw set.insert_eq,
      apply union _ _ _ h,
      have := set.mem_univ x,
      rw [← covers, set.mem_sUnion] at this,
      obtain ⟨B, hB, h⟩ := this,
      apply incl _ hB,
      simp [h], },
  end }

section
variables (ideal : set (set α))
  (empty_mem : ∅ ∈ ideal)
  (covers : ⋃₀ ideal = set.univ)
  (incl : ∀ (B ∈ ideal) (A ⊆ B), A ∈ ideal)
  (union : ∀ (B B' ∈ ideal), B ∪ B' ∈ ideal)

lemma bornology.ideal_of_eq : (bornology.of ideal empty_mem covers incl union).ideal = ideal :=
begin
  ext B,
  simp [bornology.of, bornology.ideal],
end

end

[Adam Topaz]

Nice!

[Adam Topaz]

Shouldn't infty be called co-bounded, per the title of this thread? ;)

[Yury G. Kudryashov]

So, should we have

class bornology_space (α : Type*) :=
(cobounded : filter α)
(le_cofinite : cobounded ≤ cofinite)

with an instance for a pseudo_metric_space?

[Yury G. Kudryashov]

And bounded (or whatever is the new name) defined as sᶜ ∈ cobounded.

[Jireh Loreaux]

That was my new plan. Then the morphisms are just f that satisfy comap f cobounded ≤ cobounded. I can then provide the necessary API for bounded sets, and the API for cobounded sets comes mostly for free from the API for filters.

[Yury G. Kudryashov]

What are the other instances?

[Yury G. Kudryashov]

I mean, are we going to have more than one instance for bornology_space?

[Jireh Loreaux]

We will eventually, certainly locally convex spaces, or even any topological vector space.

[Yaël Dillies]

If you could let me define bounded maps, that'd be nice, so that we can follow the hom refactor right from the start.

[Yaël Dillies]

We could then instantiate bounded_map_class for continuous linear maps.

[Jireh Loreaux]

oops, sorry, I just saw your comment. See #12036. If you want I can remove the bounded_hom bits, but if possible I would prefer if you told me how to follow the hom refactor so I can learn about it more.

[Jireh Loreaux]

Even just pointing me to an example or the relevant documentation might be enough.

[Yaël Dillies]

Sorry, don't have time anymore now, so I suggest you have a look at file#order/hom/lattice or file#order/hom/bounded

[Yaël Dillies]

But also if you leave that to me, I'll be done in 20min. Up to you.

[Jireh Loreaux]

Alright, I'll just pull out the homs and leave it to you and I'll just pay attention to how you did it.

[Yaël Dillies]

Do you want them in the same PR or a different one? I'd be happy to defer.

[Jireh Loreaux]

Doesn't matter to me. You are welcome to stick them in that one if you want to push to that branch. Or defer, your choice.