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

---

[eric-wieser]

• We multiplicativize coe_zero to coe_one' rather than coe_one, because coe_one is already used for a statement about complete rings. Similarly, we have coe_inv' and coe_mul'.

The coe_one and coe_one' lemmas have the same statement; you can delete the duplicate One instance and one lemma.

The Mul one looks problematic, as the definitions are not the same-by-definition. Can you investigate whether they are genuinely different?

[trivial1711]

I'll take a look.

[trivial1711]

I am closing this because it needs significantly more work in order to avoid the bad diamond that eric-wieser describes

[trivial1711]

Recall the following trick that this pull request uses 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. We do this to avoid creating a bad diamond with the inversion operation on a uniform field.

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

instance {α : Type*} [UniformSpace α] [Neg α] : Neg (Completion α) := ...

Now, suppose that we want to prove coe_inv' (resp. coe_neg), which states that the coercion α → Completion α commutes with inversion (resp. negation). In the current version of this pull request, coe_inv' (resp. coe_neg) only applies to uniform multiplicative (resp. additive) groups. However, we do not use the fact that multiplication (resp. addition) on α is uniformly continuous to prove it. We only use the fact that inversion (resp. negation) is continuous. So, what we really want is to have more general statements that look like this:

theorem coe_inv' {α : Type*} [UniformSpace α] [Group α] [ContinuousInv α] : ...

theorem coe_neg {α : Type*} [UniformSpace α] [Neg α] [ContinuousNeg α] : ...

Note that coe_inv' needs the assumption [Group α], because otherwise inversion is not defined on Completion α at all. However, coe_neg does not need the analogous assumption [AdditiveGroup α].

The question is: If coe_inv' and coe_neg are written in this more general form, how can we link them using @[to_additive]? Here is one option, but it obviously leaves something to be desired.

@[to_additive coe_neg_do_not_use_this_use_the_more_general_version]
theorem coe_inv' {α : Type*} [UniformSpace α] [Group α] [ContinuousInv α] : ...

theorem coe_neg {α : Type*} [UniformSpace α] [Neg α] [ContinuousNeg α] : ...

[github-actions[bot]]

PR summary fc6438dbbf

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ MonoidHom.completion + MonoidHom.completion_coe + MonoidHom.completion_mul + MonoidHom.completion_one + MonoidHom.continuous_completion + MonoidHom.continuous_extension + MonoidHom.extension + MonoidHom.extension_coe + Multipliable.toComplMulHom_tprod + Multipliable.toCompl_tprod + coe_div + coe_inv_of_field + coe_inv_of_group + continuous_toComplMulHom + denseInducing_toCompl + group + hasProd_iff_hasProd_compl + instCommGroup + instDistribMulAction + instDivCompletionOfGroup + instInvCompletionOfGroup + instMulDistribMulAction + instNegCompletion + instSMul + instSubCompletion + instance : ContinuousDiv (Completion α) := ⟨uniformContinuous_completion_div.continuous⟩ + instance : ContinuousInv (Completion α) := ⟨uniformContinuous_completion_inv.continuous⟩ + instance : ContinuousMul (Completion α) := ⟨uniformContinuous_completion_mul.continuous⟩ + instance : DivInvMonoid (Completion α) + instance : Monoid (Completion α) + instance [Mul α] : Mul (Completion α) + instance [One α] : One (Completion α) := ⟨(1 : α)⟩ + instance [Pow X M] : Pow (Completion X) M + isDenseInducing_toComplMulHom + multipliable_iff_cauchySeq_finset_and_tprod_mem + multipliable_iff_multipliable_compl_and_tprod_mem + pow_def + toComplMulHom + uniformGroup - AddMonoidHom.completion - AddMonoidHom.completion_add - AddMonoidHom.completion_coe - AddMonoidHom.completion_zero - AddMonoidHom.continuous_completion - AddMonoidHom.continuous_extension - AddMonoidHom.extension - AddMonoidHom.extension_coe - Summable.toCompl_tsum - UniformSpace.Completion.coe_zero - addGroup - coe_add - coe_neg - coe_sub - hasSum_iff_hasSum_compl - instAddCommGroup - instance : AddMonoid (Completion α) - instance : SMul M (Completion X) - instance : SubNegMonoid (Completion α) - instance [Add α] : Add (Completion α) - instance [Neg α] : Neg (Completion α) - instance [Sub α] : Sub (Completion α) - instance [Zero α] : Zero (Completion α) - instance {M} [Monoid M] [DistribMulAction M α] [UniformContinuousConstSMul M α] : - mul - one - summable_iff_cauchySeq_finset_and_tsum_mem - summable_iff_summable_compl_and_tsum_mem - uniformAddGroup

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (1.00, 0.01)

Current number	Change	Type
106	1	bare open (scoped) Classical

Current commit fc6438dbbf Reference commit 9b434d1b7f

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[trivial1711]

I am setting this as WIP for now. My plan is to make a new pull request that renames toCompl : α →+ Completion α to coeAddHom and change this pull request to depend on that one.

[eric-wieser]

I was going to suggest exactly that!