failed to synthesize `CommRing (R ⊗[ℤ] Localization M)`

Stream: Is there code for X?

[Kenny Lau]

ok, here's the Y of the problem:

import Mathlib

universe u

open TensorProduct

instance foo (R S : Type u) [CommRing R] [CommRing S] (M : Submonoid S) :
    CommRing (R ⊗[ℤ] Localization M) :=
  inferInstance
/-
failed to synthesize
  CommRing (R ⊗[ℤ] Localization M)
-/

[Notification Bot]

A message was moved here from #Is there code for X? > unique Z-module structure on any AddCommGroup by Kenny Lau.

[Kenny Lau]

in the code I see reference to https://github.com/leanprover-community/mathlib4/issues/10906 , maybe that is relevant?

[Kenny Lau]

right, i should add that the relevant instance is docs#Algebra.TensorProduct.instCommRing

[Kevin Buzzard]

(misleading post deleted because I made a crucial typo)

[Kenny Lau]

Localization S should be Localization M

[Kenny Lau]

image.png

[Kenny Lau]

I changed it to by convert Algebra.TensorProduct.instCommRing and got universe problems

[Kenny Lau]

so I changed it to by convert Algebra.TensorProduct.instCommRing.{0, u, u} and got two new subgoals

[Kenny Lau]

I closed the second goal with infer_instance and so I'm left with the first goal:

⊢ AddCommGroup.toIntModule (Localization M) = Algebra.toModule

[Kenny Lau]

so i'm now suspecting that something went wrong with Localization specifically

[Aaron Liu]

I've had trouble with localizations before, see #mathlib4 > Instance diamond in `OreLocalization`

[Kenny Lau]

I see, so 4 months ago Kevin Buzzard made a WIP PR that would have fixed this...

[Kenny Lau]

oh, except that Andrew said there that it wouldn't have solved the problem

[Kenny Lau]

hmm

[Kenny Lau]

I mean, I don't want to reinvent the wheel, does someone have retained memory from 4 months ago?

[Kenny Lau]

ok so I've reinvented the wheel and I've traced the definitions to:

#print OreLocalization.instAlgebra
#print OreLocalization.instModuleOfIsScalarTower
#print OreLocalization.instDistribMulActionOfIsScalarTower
#print OreLocalization.instMulActionOfIsScalarTower
#print OreLocalization.instSMulOfIsScalarTower
#check OreLocalization.hsmul
/-- Scalar multiplication in a monoid localization. -/
@[to_additive (attr := irreducible) "Vector addition in an additive monoid localization."]
protected def hsmul (c : R) :
    X[S⁻¹] → X[S⁻¹] :=
  liftExpand (fun m s ↦ oreNum (c • 1) s • m /ₒ oreDenom (c • 1) s) (fun r t s ht ↦ by
    dsimp only
    rw [← mul_one (oreDenom (c • 1) s), ← oreDiv_smul_oreDiv, ← mul_one (oreDenom (c • 1) _),
      ← oreDiv_smul_oreDiv, ← OreLocalization.expand])

[Kenny Lau]

so now I can see why there are defeq problems for R := ℤ

[Andrew Yang]

Yeah. There are no good solution now. One choice is to attribute [-instance] AddCommGroup.toIntModule, and another is to not talk about ℤ.

[Eric Wieser]

Andrew and I were indirectly looking at this earlier today

[Kevin Buzzard]

#21344 is inactive, I didn't want to close it because it should be some kind of issue but I'm not working on it and Andrew's comment made me realise I didn't know what I was doing. I've changed the label from awaiting-author to please-adopt.

[Kevin Buzzard]

I'm surprised we don't have

instance (A : Type*) [AddCommGroup A ] : Subsingleton (Module ℤ A) := by
  sorry

Did I just miss it?

[Kevin Buzzard]

#Is there code for X? > two module instance over ℤ @ 💬

[Kevin Buzzard]

import Mathlib

universe u

instance (M : Type*) [AddCommMonoid M] : Subsingleton (Module ℤ M) where
  allEq inst1 inst2 := by
    let _ := Module.addCommMonoidToAddCommGroup ℤ (M := M)
    ext z m
    rw [int_smul_eq_zsmul inst1,int_smul_eq_zsmul]

open TensorProduct

variable  (R S : Type u) [CommRing R] [CommRing S] (M : Submonoid S)

noncomputable instance :
    CommRing (R ⊗[ℤ] (Localization M)) := by
  convert Algebra.TensorProduct.instCommRing.{0,u,u}
  · apply Subsingleton.elim
  · infer_instance

[Aaron Liu]

well it works

[Kenny Lau]

yes, it works there but it fails in later applications because they're still not defeq

[Kevin Buzzard]

I should add that I didn't fill in the sorrys in #21344 because I couldn't figure them out quickly and wanted people's opinions about whether the approach was good in general.

I merged master into the PR and it does seem to solve your problem:

import Mathlib.RingTheory.TensorProduct.Basic
import Mathlib.RingTheory.Localization.Basic

universe u

open TensorProduct

variable (R S : Type u) [CommRing R] [CommRing S] (M : Submonoid S) in

#synth CommRing (R ⊗[ℤ] Localization M) -- works

[Kenny Lau]

I wonder if that approach would create problems down the line since there are technically now two instances of Z-module on Localization M

[Kenny Lau]

like perhaps someone would prove some theorem about the R-module structure on Localization M, and then specialise that theorem to R=Z, and now the problem would be moved to that point

[Kevin Buzzard]

Yeah presumably that's what Andrew is saying on the PR. I don't have the bandwidth to understand the problem properly but maybe someone like Eric or Andrew or you can come up with some amazing solution which involves some massive refactor or something