feat: completion of a uniform multiplicative group

[trivial1711]

Multiplicativize Topology.Algebra.GroupCompletion. That is, rewrite it in the multiplicative setting and recover the original results using @[to_additive].

• Because @[to_additive] doesn't work with noncomputable section (https://github.com/leanprover/lean4/pull/2610), some instances with @[to_additive] need to be explicitly marked with noncomputable instance.
• One might be tempted to multiplicativize this definition from Topology.Algebra.GroupCompletion:

instance [UniformSpace α] [Add α] : Add (Completion α) :=
  ⟨Completion.map₂ (· + ·)⟩

to this:

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

However, as Eric Wieser pointed out, doing so would create a bad diamond with the definition

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

in Topology.Algebra.UniformRing.

How should this diamond be resolved? Well, the definition of multiplication that uses curry <| (denseInducing_coe.prod denseInducing_coe).extend ((↑) ∘ uncurry (· * ·)) is the "correct" one. For example, it yields the correct result if α is ℚ, unlike the definition that uses Completion.map₂ (· * ·). (This is because Completion.map₂ yields junk values if used on a function which is not uniformly continuous. Note, however, that if multiplication on α is uniformly continuous, then Completion.map₂ (· * ·) and curry <| (denseInducing_coe.prod denseInducing_coe).extend ((↑) ∘ uncurry (· * ·)) are propositionally equal.) So, following Eric's suggestion, we remove the definition that uses Completion.map₂ (· * ·), and generalize the other definition to any uniform space with a multiplication operation:

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

This requires slightly modifying some of the proofs in Topology.Algebra.GroupCompletion. For example, suppose that α is a uniform group. Since we can no longer use Completion.continuous_map₂, it becomes more efficient to prove that the multiplication, inversion, and division operations on Completion α are uniformly continuous before we prove that Completion α is a group.

• Previously, Topology.Algebra.GroupCompletion had an instance:

instance [UniformSpace α] [Sub α] : Sub (Completion α) := ...

Naively multiplicativizing this would yield

@[to_additive]
instance [UniformSpace α] [Inv α] : Inv (Completion α) := ...

Unfortunately, this would conflict with Topology.Algebra.UniformField, which already instantiates Inv (Completion α) when α is a uniform field. Instead, we use two different instance declarations. (If α is an additive group, then this instantiates Neg (Completion α) twice, and the instances are syntactically equal.)

@[to_additive]
noncomputable instance [UniformSpace α] [Group α] : Inv (Completion α) := ...

instance [UniformSpace α] [Neg α] : Neg (Completion α) := ...

This avoids the bad diamond (because a uniform field can never be a Group) while remaining backward compatible. Note that the @[to_additive] is necessary here, because it maintains the link between the additive setting and multiplicative setting. We use a similar method to instantiate Div (Completion α).

• Some definitions in this file involve a module structure on α. We leave these as is and do not attempt to multiplicativize them at all.
• The instance of DistribMulAction must be multiplicativized to an instance of MulDistribMulAction manually.

Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Completion.20of.20a.20uniform.20multiplicative.20group

Co-authored-by: Eric Wieser

---