uniform_add_group vs topological_add_group

Stream: general

[Kenny Lau]

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]

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

[Mario Carneiro]

if they are equivalent, then they should be the same

[Mario Carneiro]

(I have a preference for the topological terminology)

[Kenny Lau]

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]

they can't be the same, right

[Mario Carneiro]

A topological add group has a uniform structure

[Mario Carneiro]

so it's both

[Kenny Lau]

but that would cause a loop in the inferrence

[Mario Carneiro]

how?

[Mario Carneiro]

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

[Kenny Lau]

aha

[Kenny Lau]

now?

[Mario Carneiro]

Actually I guess this is already how uniform_add_group is defined

[Mario Carneiro]

so it's just a rename

[Kenny Lau]

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]

maybe you don't need uniform continuity

[Mario Carneiro]

oh, it's a predicate

[Mario Carneiro]

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

[Kenny Lau]

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

[Mario Carneiro]

oh, wait we do need uniform continuity

[Mario Carneiro]

Is the uniformity of a uniform add group uniquely defined?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kenny Lau]

so what should I do?

[Kenny Lau]

@Kevin Buzzard what do you think about this?

[Kevin Buzzard]

This is an implementation issue and I have no idea.

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Johan Commelin]

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]

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

[Patrick Massot]

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]

@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]

which messes up everything

[Johan Commelin]

How much breaks if you remove that instance?

[Patrick Massot]

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

[Kenny Lau]

I don't think it's everything

[Kenny Lau]

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]

Are those lemmas used elsewhere in the perfectoid project?

[Kenny Lau]

I don't know

[Patrick Massot]

You can remove this.