Zulip Chat Archive

Stream: general

Topic: uniform_add_group vs topological_add_group


view this post on Zulip 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

view this post on Zulip Kenny Lau (Nov 01 2018 at 00:27):

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

view this post on Zulip Mario Carneiro (Nov 01 2018 at 00:30):

if they are equivalent, then they should be the same

view this post on Zulip Mario Carneiro (Nov 01 2018 at 00:30):

(I have a preference for the topological terminology)

view this post on Zulip 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

view this post on Zulip Kenny Lau (Nov 01 2018 at 00:30):

they can't be the same, right

view this post on Zulip Mario Carneiro (Nov 01 2018 at 00:31):

A topological add group has a uniform structure

view this post on Zulip Mario Carneiro (Nov 01 2018 at 00:31):

so it's both

view this post on Zulip Kenny Lau (Nov 01 2018 at 00:31):

but that would cause a loop in the inferrence

view this post on Zulip Mario Carneiro (Nov 01 2018 at 00:31):

how?

view this post on Zulip Mario Carneiro (Nov 01 2018 at 00:31):

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

view this post on Zulip Kenny Lau (Nov 01 2018 at 00:32):

aha

view this post on Zulip Kenny Lau (Nov 01 2018 at 00:32):

now?

view this post on Zulip Mario Carneiro (Nov 01 2018 at 00:32):

Actually I guess this is already how uniform_add_group is defined

view this post on Zulip Mario Carneiro (Nov 01 2018 at 00:33):

so it's just a rename

view this post on Zulip 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))

view this post on Zulip Mario Carneiro (Nov 01 2018 at 00:33):

maybe you don't need uniform continuity

view this post on Zulip Mario Carneiro (Nov 01 2018 at 00:34):

oh, it's a predicate

view this post on Zulip Mario Carneiro (Nov 01 2018 at 00:34):

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

view this post on Zulip Kenny Lau (Nov 01 2018 at 00:36):

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

view this post on Zulip Mario Carneiro (Nov 01 2018 at 00:37):

oh, wait we do need uniform continuity

view this post on Zulip Mario Carneiro (Nov 01 2018 at 00:37):

Is the uniformity of a uniform add group uniquely defined?

view this post on Zulip Mario Carneiro (Nov 01 2018 at 00:39):

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

view this post on Zulip Mario Carneiro (Nov 01 2018 at 00:39):

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

view this post on Zulip Mario Carneiro (Nov 01 2018 at 00:40):

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

view this post on Zulip Kenny Lau (Nov 01 2018 at 00:52):

so what should I do?

view this post on Zulip Kenny Lau (Nov 01 2018 at 08:44):

@Kevin Buzzard what do you think about this?

view this post on Zulip Kevin Buzzard (Nov 01 2018 at 08:46):

This is an implementation issue and I have no idea.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Nov 01 2018 at 09:12):

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

view this post on Zulip Kevin Buzzard (Nov 01 2018 at 09:18):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 01 2018 at 14:57):

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

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Kenny Lau (Nov 01 2018 at 18:54):

which messes up everything

view this post on Zulip Johan Commelin (Nov 01 2018 at 19:04):

How much breaks if you remove that instance?

view this post on Zulip 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

view this post on Zulip Kenny Lau (Nov 01 2018 at 19:41):

I don't think it's everything

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 01 2018 at 19:45):

Are those lemmas used elsewhere in the perfectoid project?

view this post on Zulip Kenny Lau (Nov 01 2018 at 19:45):

I don't know

view this post on Zulip Patrick Massot (Nov 01 2018 at 20:43):

You can remove this.


Last updated: May 10 2021 at 00:31 UTC