Diamond in `PiTensorProduct`?

Stream: mathlib4

[Moritz Doll]

I just came across this while working on a refactor and this certainly seems bad.

import Mathlib.LinearAlgebra.PiTensorProduct

variable {ι : Type*}
variable {R : Type*} [CommSemiring R]
variable {s : ι → Type*} [∀ i, AddCommMonoid (s i)] [∀ i, Module R (s i)]

open scoped TensorProduct

#check PiTensorProduct.hasSMul' (R₁ := ℕ) (R := R) (ι := ι) (s := s)
#check AddMonoid.toNatSMul (M := (⨂[R] i, s i))

variable (n : ℕ) (f : (⨂[R] i, s i))

example : AddMonoid.toNatSMul.smul n f = PiTensorProduct.hasSMul'.smul n f := by
  rfl -- fails

I would be surprised if this is the only instance where toNatSMul causes issues.

[Floris van Doorn]

Yes, that's not good.

Since AddMonoid.toNatSMul just uses a projection of AddCommMonoid, we can manually modify docs#PiTensorProduct.instAddCommMonoid (or an even more basic definition) so that it uses something that is defeq to PiTensorProduct.hasSMul', right?

[Moritz Doll]

Looking at it a bit more, I tend towards thinking that hasSMul' is a bit weird. The SMul instance from AddCommMonoid seems pretty reasonable. In fact I would have assumed that hasSMul' should do a similar thing and use Function.Surjective.distribMulAction and friends to transport the structures through the quotient. However, the quotient does not have anything about SMul. I would hope that something like

def hasSMul {M : Type*} [AddMonoid M] [SMul R M] (c : AddCon M)
    (h : ∀ (r : R) x y, c x y → c (r • x) (r • y)) :
    SMul R c.Quotient where
  smul r := Quotient.map' (fun x ↦ r • x) (h r)

works.

[Yury G. Kudryashov]

So, both pow/nsmul on docs#Con.Quotient and this instSMul' should be changed. I'm not sure if changing both will give us defeq in the right reducibility though.

[Moritz Doll]

This works, so I don't understand why we want to change nsmul.

variable (R) in
def hasSMul {M : Type*} [AddMonoid M] [SMul R M] (c : AddCon M)
    (h : ∀ (r : R) x y, c x y → c (r • x) (r • y)) :
    SMul R c.Quotient where
  smul r := Quotient.map' (r • ·) (h r)

variable (c : AddCon M) (r : ℕ) (x : c.Quotient)

#check AddMonoid.toNatSMul.smul r x
#check (hasSMul ℕ c (fun r _ _ ↦ c.nsmul r)).smul r x

example : AddMonoid.toNatSMul.smul r x = (hasSMul ℕ c (fun r _ _ ↦ c.nsmul r)).smul r x := by rfl

[Moritz Doll]

The only problem is that there is no instance for general scalar multiplication on FreeAddMonoid, but that shouldn't be too hard either

[Moritz Doll]

Ah, the scalar multiplication on FreeAddMonoid is in fact the problem: the addition is just concatenation and component-wise scalar multiplication is not equal to that, but in the case of PiTensorProduct the equivalence relation forces the two to be equal.

[Yury G. Kudryashov]

Thanks for investigating! I think that we should introduce instSMul before instAddCommMonoid, then use Function.Surjective.addCommMonoid instead of the generic instance.

[Moritz Doll]

It seems less straightforward, because the definition of the SMul instance uses the additive structure, but there is probably some way around it