Instance diamond in `OreLocalization`

Stream: mathlib4

[Aaron Liu]

While trying to make a term of type ℝ →+*o Surreal:

import Mathlib

example :
    -- comes from `OreLocalization.hsmul`, depends on `SMul ℤ ℤ`
    @instHSMul ℤ (Localization (Submonoid.powers (2 : ℤ))) OreLocalization.instSMulOfIsScalarTower =
    -- comes from `OreLocalization.zsmul`, depends on `AddGroup ℤ`
    @instHSMul ℤ (Localization.Away (2 : ℤ)) SubNegMonoid.toZSMul := by
  -- helpme
  sorry

[Eric Wieser]

I'm not sure if this is a reasonable statement; are the types of the LHS and RHS reducibly defeq?

[Eric Wieser]

(that is, can you do the same test again on the second arguments to instHSMul, and test if with_reducible rfl is happy?)

[Aaron Liu]

import Mathlib

example : (Localization (Submonoid.powers (2 : ℤ))) = (Localization.Away (2 : ℤ)) := by
  with_reducible rfl

[Aaron Liu]

It works

[Kevin Buzzard]

I don't think this has got anything to do with the difference between Localization.Away and Localization: both docs#OreLocalization.instSMulOfIsScalarTower and docs#OreLocalization.instAddGroupOreLocalization work for general localization by submonoids. There's a warning in the code that the former instance might cause diamonds in an obscure situation but ths seems far less obscure.

[Yaël Dillies]

This diamond is known, yes. @Andrew Yang and I hit it in #21021

[Kevin Buzzard]

Maybe one could try weakening the definition of docs#OreLocalization.zsmul, adding an assumption [SMul ℤ R] and defining it not as zsmulRec but as OreLocalization.hsmul. This would reduce the scope of AddCommGroup X[S⁻¹] a little (requiring that S is a submonoid of basically a ring rather than just a monoid) but do we care in practice?

#21344 let's see if it compiles at least.

[Kevin Buzzard]

Hmm, it compiles (locally) but doesn't seem fix the diamond so I must have misanalysed something :-/

[Yaël Dillies]

Sorry, was interrupted. Let me explain.

[Kevin Buzzard]

Oh OK on that branch this works:

import Mathlib

example :
    -- comes from `OreLocalization.hsmul`, depends on `SMul ℤ ℤ`
    @instHSMul ℤ (Localization (Submonoid.powers (2 : ℤ))) OreLocalization.instSMulOfIsScalarTower =
    -- comes from `OreLocalization.zsmul`, depends on `AddGroup ℤ`
    @instHSMul ℤ (Localization.Away (2 : ℤ)) SubNegMonoid.toZSMul := by
  unfold instHSMul SMul.smul SubNegMonoid.toZSMul SubNegMonoid.zsmul
  unfold OreLocalization.instSMulOfIsScalarTower
  unfold AddGroup.toSubNegMonoid OreLocalization.instAddGroupOreLocalization
  dsimp only
  unfold OreLocalization.zsmul
  rfl

so it's now a reducibility issue (but I've now run out of time to think about this, unfortunately)

[Andrew Yang]

There is docs#OreLocalization.zsmul_eq_zsmul to show that they are at least equal.

[Andrew Yang]

And I’m not sure if we don’t need localization of modules of monoids.

[Kevin Buzzard]

We might need it in the future but apparently we don't need it yet in the non-commutative case.

[Kevin Buzzard]

Ok so #21344 now has

import Mathlib.RingTheory.OreLocalization.Ring
import Mathlib.GroupTheory.MonoidLocalization.Basic

example :
    -- comes from `OreLocalization.hsmul`, depends on `SMul ℤ ℤ`
    @instHSMul ℤ (Localization (Submonoid.powers (2 : ℤ))) OreLocalization.instSMulOfIsScalarTower =
    -- comes from `OreLocalization.zsmul`, depends on `AddGroup ℤ`
    @instHSMul ℤ (Localization (Submonoid.powers (2 : ℤ))) SubNegMonoid.toZSMul := by
  with_reducible_and_instances rfl

so the diamond is gone (and I assume will remain gone after import Mathlib) but in order to deal with Andrew's concern I've also added back the SMul instance without assuming a Z-action on R (so it works for monoids) but with low priority, so it will be found only if R isn't a ring, which should hopefully be enough to deal with all the issues here.

There are some sorrys which I've left as an exercise :-)

[Andrew Yang]

I don't think this low-priority trick works, because lemmas about groups will still find the Group instance which contains the bad zsmul instance.

[Andrew Yang]

Maybe it will work if [SMul ℤ X[S⁻¹]] is an assumption to AddGroup X[S⁻¹], but I'm not sure if TC synthesis will like it.