Completion of a uniform multiplicative group

Stream: mathlib4

[Mitchell Lee]

In Topology.Algebra.GroupCompletion (https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Algebra/GroupCompletion.html) it is proved that the completion of a uniform additive group is itself a uniform additive group and that it satisfies various properties including functoriality. I would like to "multiplicativize" this file; that is, rewrite it in the multiplicative setting and recover the original results using @[to_additive]. Does anyone have any thoughts on whether I should do this? If so, are there any particular difficulties I should watch out for?

[Mitchell Lee]

Okay, I have found one reason why this might be difficult. In my first attempt to multiplicativize this file, I changed this:

instance [Neg α] : Neg (Completion α) :=
  ⟨Completion.map (fun a ↦ -a : α → α)⟩

to this:

@[to_additive]
instance [Inv α] : Inv (Completion α) :=
  ⟨Completion.map (fun a ↦ a⁻¹ : α → α)⟩

Unfortunately, this yields the error message "failed to compile definition, consider marking it as 'noncomputable' because it depends on 'UniformSpace.Completion.map', and it does not have executable code", which I do not really understand. Even if I mark it as noncomputable, though, there is another problem: if α is a field, this conflicts with the following definition of inverse on the completion of α, from Topology.Algebra.UniformField line 101.

instance instInvCompletion : Inv (hat K) :=
  ⟨fun x => if x = 0 then 0 else hatInv x⟩

One option is to only instantiate Inv (Completion α) if α is a group under multiplication:

@[to_additive]
noncomputable instance [Group α] : Inv (Completion α) :=
  ⟨Completion.map (fun a ↦ a⁻¹ : α → α)⟩

Mathlib does successfully build with this change, but I am worried that it might break something else at some point.

Here is my progress: https://github.com/leanprover-community/mathlib4/compare/trivial1711-multiplicative-completion

[Mitchell Lee]

Perhaps I should give up and accept that Mathlib doesn't put a group structure on the completion of a uniform multiplicative group. It probably isn't going to come up very often anyway.

[Kevin Buzzard]

I don't really see a reason why this shouldn't all work, and it should be a good exercise. Why do you need it, out of interest? The multiplicative theory will not be any more or less computable than the additive theory.

[Mitchell Lee]

Recently, I multiplicativized several files in Topology.Algebra.InfiniteSum, so they work with infinite products now too.

Now, I want to add a few lemmas to Topology.Algebra.InfiniteSum.Group that involve completion:

section UniformAddGroup

open UniformSpace.Completion

variable [AddCommGroup α] [UniformSpace α] [UniformAddGroup α]

/-- A function `f` has a sum in an uniform additive group `α` if and only if it has that sum in the
completion of `α`. -/
theorem hasSum_iff_hasSum_compl (f : β → α) (a : α):
    HasSum f a ↔ HasSum (toCompl ∘ f) a := sorry

/-- A function `f` is summable in a uniform additive group `α` if and only if it is summable in
`Completion α` and its sum in `Completion α` lies in the image of `toCompl : α →+ Completion α`. -/
theorem summable_iff_summable_compl_and_tsum_mem (f : β → α) :
    Summable f ↔ Summable (toCompl ∘ f) ∧ ∑' i, toCompl (f i) ∈ Set.range toCompl := sorry

/-- A function `f` is summable in a uniform additive group `α` if and only if the net of its partial
sums is Cauchy and its sum in `Completion α` lies in the image of `toCompl : α →+ Completion α`.
(The condition that the net of partial sums is Cauchy can be checked using
`cauchySeq_finset_iff_sum_vanishing` or `cauchySeq_finset_iff_tsum_vanishing`.) -/
theorem summable_iff_cauchySeq_finset_and_tsum_mem (f : β → α) :
    Summable f ↔ CauchySeq (fun s : Finset β ↦ ∑ b in s, f b) ∧
      ∑' i, toCompl (f i) ∈ Set.range toCompl := sorry

/-- If a function `f` is summable in a uniform additive group `α`, then its sum in `α` is the same
as its sum in `Completion α`. -/
theorem Summable.toCompl_tsum {f : β → α} (hf : Summable f) : ∑' i, f i = ∑' i, toCompl (f i) := sorry

end UniformAddGroup

I was able to prove all of these lemmas (see https://github.com/leanprover-community/mathlib4/compare/master...trivial1711-complete-sums), but now they are the only statements in the whole file that don't have a multiplicative analogue. And that annoys me. But unfortunately, I can't state the multiplicative analogue of these statements until Topology.Algebra.GroupCompletion is multiplicativized.

I admit, however, that my own mild annoyance might not be a very good reason to want mathlib to recognize the completion of a uniform multiplicative group as a group.

[Mitchell Lee]

Also, Topology.Algebra.GroupCompletion already starts with noncomputable section, so I think those instances were already noncomputable. But it seems that if you put @[to_additive]on the instances, you have to declare them noncomputable again, even though they're in a noncomputable section.

[Yaël Dillies]

cc @Floris van Doorn, this looks like a to_additive bug

[Yakov Pechersky]

Apart from completions of groups, I wonder if you'll need completions of groups with zero.

[Floris van Doorn]

This looks like lean4#2610.

[Floris van Doorn]

cc @Alex J. Best

[Matthew Ballard]

You might just want suppress_compilation at the top of the file if you don't care about code generation for your completed groups.

[Mitchell Lee]

Okay, I've made the completion of a uniform multiplicative group into a PR: #11837

[Eric Wieser]

There's some slight awkwardness here with the definition of multiplication; this PR introduces

instance [Mul α] : Mul (Completion α) :=
  ⟨Completion.map₂ (· * ·)⟩

but we already have

instance mul [Ring α] : Mul (Completion α) :=
  ⟨curry <| (denseInducing_coe.prod denseInducing_coe).extend ((↑) ∘ uncurry (· * ·))⟩

Are these definitions compatible?

[Mitchell Lee]

Thanks for catching that. I think this is actually a big problem. These are (propositionally) equal if multiplication is continuous, but if it isn't, then I am not sure.

[Mitchell Lee]

Never mind, these are not even propositionally equal. Completion.map₂ just returns some junk value if used on a function that isn't uniformly continuous. Such as multiplication on $\mathbb{R}$, for example. So the definition using Completion.map₂ just doesn't work for rings at all.

[Kevin Buzzard]

A ring is never a group -- can you restrict to groups?

[Mitchell Lee]

Yeah, that is the most obvious answer. Unfortunately, the zero ring is a group. I don't know if this would actually create a bad diamond, though, because it might not actually have a Group instance on it.

[Mitchell Lee]

Also, I don't know if this bad diamond would actually matter.

[Mitchell Lee]

I don't have a great understanding of the pitfalls of typeclass inference and how to avoid them.

[Eric Wieser]

Does the Ring definition of * make sense on groups? If the group version just has weird junk values, perhaps they can be changed to match the junk values used by rings.

[Mitchell Lee]

I think the ring definition makes sense for groups. Some of the proofs in Topology/Algebra/GroupCompletion would have to be reworked, but that seems worth it.

[Eric Wieser]

Presumably the result would be that many of the results would generalize to uniform completions of monoids?

[Mitchell Lee]

So we could just do this. I think.

@[to_additive]
instance mul [Mul α] : Mul (Completion α) :=
  ⟨curry <| (denseInducing_coe.prod denseInducing_coe).extend ((↑) ∘ uncurry (· * ·))⟩

[Mitchell Lee]

Maybe some of the results could be generalized to monoids in which the multiplication is uniformly continuous. This is not currently a typeclass in mathlib, though.

[Mitchell Lee]

(This is probably because every topological group has a canonical uniformity that makes it into a uniform group, but topological monoids do not.)

[Mitchell Lee]

(Okay, maybe this is wrong; sorry.)

[Mitchell Lee]

Mitchell Lee said:

So we could just do this. I think.

@[to_additive]
instance mul [Mul α] : Mul (Completion α) :=
  ⟨curry <| (denseInducing_coe.prod denseInducing_coe).extend ((↑) ∘ uncurry (· * ·))⟩

I just did it: https://github.com/leanprover-community/mathlib4/tree/trivial1711-multiplicative-completion. By "it", I mean this. Let α be a uniform space with an addition operation. I changed the definition of addition on Completion α to use DenseInducing.extend instead of Completion.map₂:

instance [Add α] : Add (Completion α) :=
  ⟨curry <| (denseInducing_coe.prod denseInducing_coe).extend ((↑) ∘ uncurry (· + ·))⟩

Everything in mathlib still works, after a few tweaks to some of the proofs in Mathlib/Topology/Algebra/GroupCompletion.lean. If addition onα is uniformly continuous, then the new definition is propositionally equal to the old one. If addition on α is not uniformly continuous, then the new definition yields sensible values whereas the old definition yields junk values.

With this new definition, everything can be multiplicativized. We end up with

@[to_additive]
instance [Mul α] : Mul (Completion α) :=
  ⟨curry <| (denseInducing_coe.prod denseInducing_coe).extend ((↑) ∘ uncurry (· * ·))⟩

which is the exact definition of multiplication on uniform rings currently in Mathlib/Topology/Algebra/UniformRing.lean. This gets rid of the bad diamond that Eric Wieser thankfully pointed out. And we can even delete the definition of multiplication on uniform rings in Mathlib/Topology/Algebra/UniformRing.lean because it's redundant.

I will try to make a pull request soon.

[Mitchell Lee]

Okay, here it is: #11837.

[Kevin Buzzard]

Thanks so much for unraveling all this!

[Eric Wieser]

Is map / map2 useful at all with the current definition? Should we redefine it to use extend?

[Mitchell Lee]

The definition of UniformSpace.Completion.map already uses denseInducing_coe.extend.

UniformSpace.Completion.map f is equal to denseInducing_coe.extend ((↑) ∘ f) if f is uniformly continuous. Otherwise, it is just some arbitrary constant function. This is by design; it has the advantage that it is always continuous, no matter what f is. However, it is probably not the best choice for defining operations on a uniform space.

[Mitchell Lee]

Hello, I have just run into a small problem. Recall the trick we use to define inversion and negation on uniform spaces. The idea is that we define negation on the completion of any uniform space that has a negation operation, but we define inversion on only the completion of a uniform space that has the structure of a multiplicative group. This avoids creating a bad diamond with the inversion operation on a uniform field. Here is a snippet that demonstrates this:

@[to_additive]
instance {α : Type*} [UniformSpace α] [Group α] : Inv (Completion α) := ...

-- more general instance which is definitionally equal to the more specific one defined above
instance {α : Type*} [UniformSpace α] [Neg α] : Neg (Completion α) := ...

The problem is this. Suppose you prove a theorem about the inversion operation on Completion α, and you use @[to_additive] on that theorem. Then, the additivized version will have the possibly unnecessary assumption [AdditiveGroup α]. I made a comment here that describes this problem in detail: #11837

Can anyone suggest how to work around this?