Zulip Chat Archive

Stream: PR reviews

Topic: Bounded maps #12046

Johan Commelin (Mar 10 2022 at 07:00):

I don't know anything about bornologies. Reviews welcome!

Scott Morrison (Mar 10 2022 at 08:14):

I'm not sure I'd even heard of them before this PR!

Moritz Doll (Mar 10 2022 at 10:35):

I think that it looks good, but I am not too familiar with how to define morphisms properly in mathlib. Maybe there should be a Prop saying that a map is bounded iff it maps bounded sets to bounded sets (that should follow directly from the definition).

Moritz Doll (Mar 10 2022 at 10:54):

and the todo comment is maybe a bit too optimistic: for example there are two different ways to obtain a good bornology from a pseudometric space that is a module over a normed field: #12078 and #12449. In each case one has that bounded maps are continuous. and of course a bornology does not have to be compatible with the topology (a bornological space does not need to have a topology at all)

Jireh Loreaux (Mar 10 2022 at 14:02):

@Yaël Dillies didn't you define locally bounded maps?

Jireh Loreaux (Mar 10 2022 at 14:12):

Oh nevermind, this is the same PR. :face_palm:

Jireh Loreaux (Mar 10 2022 at 14:36):

FYI: a bornological_space does have to have a topology (in fact, it must be a LCTVS), and moreover, the topology and the bornology have to be compatible. However, a bornology on a type does not imply a topology on that type, and even if one exists, they don't have to be compatible. This is somewhat confusing terminology, but it seems to be standard.

Moritz Doll (Mar 10 2022 at 14:57):

you are of course correct, I meant 'equipped with a bornology' and forgot that bornological space were a (different) thing.

Yaël Dillies (Mar 15 2022 at 20:36):

Should be ready for review again. Sorry for the delay.

Moritz Doll (Mar 16 2022 at 08:00):

I don't feel qualified to properly review PRs, but I think it should be merged.

Kyle Miller (Mar 16 2022 at 08:24):

I like how we discovered that bornologies can be defined purely in terms of their "filter at infinity" and that locally bounded functions have a simple filter definition -- mathlib has out-filtered Bourbaki once again

Yaël Dillies (Mar 16 2022 at 08:56):

Yet another artifact of formalization!

Arthur Paulino (Mar 16 2022 at 09:29):

Does it deserve a blog post? I think we don't see it everyday

Last updated: Dec 20 2023 at 11:08 UTC