adic completion is commutative

Stream: mathlib4

[Kevin Buzzard]

I'm trying to bump FLT and this is timing out for me:

import Mathlib

open IsDedekindDomain HeightOneSpectrum

variable (B L : Type*)
    [CommRing B] [IsDedekindDomain B]
    [Field L] [Algebra B L] [IsFractionRing B L]
    (w : HeightOneSpectrum B)

-- w-adic completion of L is a field
#synth Field (adicCompletion L w)

/-
(deterministic) timeout at `isDefEq`, maximum number of heartbeats (200000) has been reached
-/
-- example (a b : adicCompletion L w) : a * b = b * a := mul_comm a b

#synth CommMagma (adicCompletion L w) -- times out

I'm out and about with a laptop and bad internet so I can't check whether this is failing on mathlib master and if so whether it was still failing in v4.15...

[Matthew Ballard]

Yes, this seems quite bad on master. The boundary seems CommMonoid and CommSemigroup

[Eric Wieser]

Fails on the web editor (almost master) and on the stable web editor (4.15.0)

[Matthew Ballard]

Removing the heartbeat limits, I cannot get it to return

[Michael Stoll]

This seems to be the problematic step:

#synth CommRing (adicCompletion L w) -- OK
#synth NonUnitalCommRing (adicCompletion L w) -- times out

[Michael Stoll]

The trace for NonUnitalCommRing ends with

  [] 💥️ apply @NumberField.instNormedFieldValuedAdicCompletion to NormedField (adicCompletion L w) ▼
  [tryResolve] 💥️ NormedField (adicCompletion L w) ≟ NormedField (adicCompletion L ?m.4778)

[Kevin Buzzard]

I wonder whether that huge PR which separates topology from algebra type classes fixes it? I'm quite busy this week because of LT25 :-/

[Matthew Ballard]

If you want a spot fix, you can de-instance locally or otherwise the one @Michael Stoll references above.

[Matthew Ballard]

#13020 made docs#IsDedekindDomain.HeightOneSpectrum.adicCompletion an abbrev. It didn't change any of the instances below, eg Field, which can now be inferInstance. Was there a reason for this?

[Matthew Ballard]

#20796 seems to fix things.

[Ruben Van de Velde]

Can you test against the FLT bump branch?

[Matthew Ballard]

Not until later, maybe tomorrow at the worst

[Matthew Ballard]

In theory you just need to sprinkle dsimp only [adicCompletion] for anything that breaks. If you want a low-thought-expenditure "fix"

[Kevin Buzzard]

Many thanks Matt! I really don't have much time this week because of trying to do my job and running LT24 and moving my daughter back to college so there is definitely no hurry here. It will be top priority for me on Monday.

[Ruben Van de Velde]

Thanks! I've got BaseChange.lean compiling in FLT, will push in a bit

[Ruben Van de Velde]

FLT#313

[Eric Wieser]

Kevin Buzzard said:

that huge PR which separates topology from algebra type classes fixes it?

Do you mean analysis (NormedAddCommGroup etc) from algebra typeclasses? I think topology and algebra are already separate

[Matthew Ballard]

While the patch is principled, Lean shouldn't be crashing out on this synthesis problem.