Stream: general

Kenny Lau (Nov 01 2018 at 00:27):

We know that a topological additive abelian group is a uniform additive group, and that a uniform additive group is a topological additive group

Kenny Lau (Nov 01 2018 at 00:27):

but which one of them should be an instance? @Kevin Buzzard @Mario Carneiro

Mario Carneiro (Nov 01 2018 at 00:30):

if they are equivalent, then they should be the same

Mario Carneiro (Nov 01 2018 at 00:30):

(I have a preference for the topological terminology)

Kenny Lau (Nov 01 2018 at 00:30):

a topological additive group is based on a topological space and an additive group; a uniform additive group is based on a uniform space and an additive group

Kenny Lau (Nov 01 2018 at 00:30):

they can't be the same, right

Mario Carneiro (Nov 01 2018 at 00:31):

A topological add group has a uniform structure

so it's both

Kenny Lau (Nov 01 2018 at 00:31):

but that would cause a loop in the inferrence

how?

Mario Carneiro (Nov 01 2018 at 00:31):

I'm saying delete uniform add group and replace it with top add group

aha

now?

Mario Carneiro (Nov 01 2018 at 00:33):

so it's just a rename

Kenny Lau (Nov 01 2018 at 00:33):

well, currently we have:

class uniform_add_group (α : Type u) [uniform_space α] [add_group α] : Prop :=
(uniform_continuous_sub : uniform_continuous (λp:α×α, p.1 - p.2))


Mario Carneiro (Nov 01 2018 at 00:33):

maybe you don't need uniform continuity

Mario Carneiro (Nov 01 2018 at 00:34):

oh, it's a predicate

Mario Carneiro (Nov 01 2018 at 00:34):

@Johannes Hölzl will object, but I want it to be a class

Kenny Lau (Nov 01 2018 at 00:36):

indeed it is Hoelzl who introduced uniform add groups, at least according to this

Mario Carneiro (Nov 01 2018 at 00:37):

oh, wait we do need uniform continuity

Mario Carneiro (Nov 01 2018 at 00:37):

Is the uniformity of a uniform add group uniquely defined?

Mario Carneiro (Nov 01 2018 at 00:39):

Topological groups actually have two induced uniformities, the left and right uniformity

Mario Carneiro (Nov 01 2018 at 00:39):

so topological add group and uniform add group aren't exactly the same

Mario Carneiro (Nov 01 2018 at 00:40):

a uniform add group comes with a chosen uniformity, a top add group doesn't

Kenny Lau (Nov 01 2018 at 00:52):

so what should I do?

Kevin Buzzard (Nov 01 2018 at 08:46):

This is an implementation issue and I have no idea.

Kevin Buzzard (Nov 01 2018 at 08:46):

I will comment though that with something like the Haar measure on a locally compact Hausdorff topological group, there are two: a left Haar measure and a right Haar measure, but mathematicians often just talk about "the Haar measure" and they have just randomly chosen one of them.

Johan Commelin (Nov 01 2018 at 09:12):

But these are additive groups, which should always be abelian, and then the uniformities coincide.

Kevin Buzzard (Nov 01 2018 at 09:18):

No -- Haar measure doesn't need abelian. It's Pontrjagin duality which needs abelian

Johan Commelin (Nov 01 2018 at 09:47):

Sure, I know that. Infinite Galois groups have Haar measures...
So I think my point is: in the non-commutative case we don't want an instance from topological_group to uniform_group because in that case we want the user to explicitly say "Use the left uniformity" (or "use the left Haar measure", etc...). But in the commutative case, the left and right uniformity agree (just as with Haar measures), so it would make sense if the system could automatically pick one. But then we get diamond issues, and maybe it is just not worth it.

Kevin Buzzard (Nov 01 2018 at 14:57):

Oh I see! Sorry :-) What I'm suggesting is that we always use the left one.

Patrick Massot (Nov 01 2018 at 18:30):

I was also confused by uniform_add_group in the beginning, and wanted to get rid of it and keep topological add groups. But then I had this completion diamond issue, and Johannes fixed it by using more uniform_add_group...

Kenny Lau (Nov 01 2018 at 18:54):

@Patrick Massot @Kevin Buzzard the problem is that I'm cleaning up the perfectoid project in which you have an instance of topological add comm group -> uniform add group

Kenny Lau (Nov 01 2018 at 18:54):

which messes up everything

Johan Commelin (Nov 01 2018 at 19:04):

How much breaks if you remove that instance?

Patrick Massot (Nov 01 2018 at 19:39):

Everything about topological rings in the perfectoid project has been merged into mathlib, you can get rid of everything

Kenny Lau (Nov 01 2018 at 19:41):

I don't think it's everything

Kenny Lau (Nov 01 2018 at 19:42):

here's what is left of for_mathlib/uniform_space.lean:

import analysis.topology.completion
import analysis.topology.uniform_space

namespace uniform_space
variables {α : Type*} [uniform_space α] {β : Type*} [uniform_space β] {γ : Type*} [uniform_space γ]
open Cauchy set

def pure_cauchy₂ : α × β → Cauchy α × Cauchy β := λ x, (pure_cauchy x.1, pure_cauchy x.2)

lemma pure_cauchy_dense₂ : ∀x : Cauchy α × Cauchy β, x ∈ closure (range (@pure_cauchy₂ α _ β _)) :=
begin
intro x,
dsimp[pure_cauchy₂],
rw [←prod_range_range_eq, closure_prod_eq],
simp[prod.ext_iff, pure_cauchy_dense],
end

namespace pure_cauchy

lemma prod.de : dense_embedding (λ p : α × β, (pure_cauchy p.1, pure_cauchy p.2)) :=
dense_embedding.prod dense_embedding_pure_cauchy dense_embedding_pure_cauchy
end pure_cauchy

end uniform_space


Johan Commelin (Nov 01 2018 at 19:45):

Are those lemmas used elsewhere in the perfectoid project?

I don't know

Patrick Massot (Nov 01 2018 at 20:43):

You can remove this.

Last updated: May 10 2021 at 00:31 UTC