Bundled uniform continuous map

Stream: Is there code for X?

[Aaron Liu]

Are there bundled uniform continuous maps in mathlib? I see docs#UniformEquiv for the uniform continuous equivs with uniform continuous inverse, and I know I can use the morphisms in the category of uniform spaces, but I want a version that doesn't use category theory.

[Jireh Loreaux]

No, we don't have bundled uniform continuous maps.

[Kevin Buzzard]

People like Thomas Skrivan would be pleased about this because the unbundled maps are far easier for fun_prop to work with. Why do we need them?

Are uniform maps between uniform spaces naturally a uniform space? This is famously not true for topological spaces and continuous maps

[Aaron Liu]

They are naturally a uniform space in two different ways lol

[Aaron Liu]

They both give you a monoidal closed structure on the category of uniform spaces but one of them is symmetric and the other is not

[Aaron Liu]

If you pick pointwise convergence the corresponding tensor product to make it monoidal closed is symmetric, and if you pick uniform convergence then the corresponding tensor product is not symmetric

[Aaron Liu]

Anyways the reason I want a type of bundled uniform continuous maps is because it makes it convenient for stating adjunctions

[Kevin Buzzard]

But didn't someone just say that we had the category of uniform spaces?

[Aaron Liu]

Also a lot of definitions are "if IsUniformContinuous f then construction else junk"

[Aaron Liu]

Kevin Buzzard said:

But didn't someone just say that we had the category of uniform spaces?

I think there's a circular import problem

[Aaron Liu]

For example here are a few adjunctions I don't know how to state because we don't have a bundled uniformly continuous map

• completion left adjoint to forget (complete hausdorff uniform space -> uniform space)
• separation quotient left adjoint to forget (hausdorff uniform space -> uniform space)
• fine uniformity left adjoint to forget (uniform space -> topological space)
• stone cech left adjoint to forget (compact hausdorff uniform space -> topological space)
• discrete uniformity left adjoint to forget (uniform space -> types)
• indiscrete uniformity right adjoint to forget (uniform space -> types)

I still don't understand the problem with fun_prop and bundled maps. I know it doesn't work but why does it not work? What's the fundamental problem here that's unfixable?

[Notification Bot]

This topic was moved here from #Is there code for X? > Bundles uniform continuous map by Aaron Liu.