Type error tensor product

Stream: new members

[María Inés de Frutos Fernández]

I don't understand what's going on in the following code:

import data.real.basic
import ring_theory.tensor_product

noncomputable theory
open_locale tensor_product

variables (K : Type) [ring K] [algebra ℚ K]

instance : ring (K ⊗[ℚ] ℝ) := algebra.tensor_product.tensor_product.ring --or infer_instance
instance : ring (ℚ ⊗[ℚ] ℝ) := algebra.tensor_product.tensor_product.ring --fails

The first instance works fine, but the second one gives me the error

  algebra.tensor_product.tensor_product.ring
has type
  ring (?m_3 ⊗ ?m_4) : Type (max ? ?)
but is expected to have type
  ring (ℚ ⊗ ℝ) : Type

However both (K ⊗[ℚ] ℝ) and (ℚ ⊗[ℚ] ℝ) have type Type. So why does the second one fail? I guess it has something to do withℚ playing two different roles, but I don't see why that causes a problem.

[Adam Topaz]

Is lean able to infer a Q algebra structure on Q? (I hope it can...)

[Reid Barton]

If I write

instance : ring (ℚ ⊗[ℚ] ℝ) := begin
  convert @algebra.tensor_product.tensor_product.ring ℚ _ ℚ _ _ ℝ _ _,
end

then I am left with

⊢ semiring.to_module = algebra.to_module

[María Inés de Frutos Fernández]

Adam Topaz said:

Is lean able to infer a Q algebra structure on Q? (I hope it can...)

Yes, it can.

[Reid Barton]

so it seems like there is some disagreement about the module ℚ ℚ structure, however, from looking at the definitions I don't understand why: looks like both should be given by x \bub y = x * y

[Eric Rodriguez]

ext, congr gets the goal r = ⇑(rat.cast_hom ℚ) r, which doesn't seem to be true by refl :(

[Adam Topaz]

Ah I bet the algebra structure is obtained from some general instance for characteristic zero fields, and the module structure comes from the obvious module structure of a ring on itself

[Reid Barton]

oh yes you're right, local attribute [instance, priority 10000] algebra.id fixes it

[Reid Barton]

and otherwise it's finding docs#rat.algebra_rat

[Reid Barton]

Shouldn't that instance have some lower priority?

[María Inés de Frutos Fernández]

Thanks a lot!

[Reid Barton]

FWIW, these has type ?m, expected X errors usually mean that Lean already tried the obvious ?m = X but it failed for some reason generally having to do with type classes

[Adam Topaz]

Reid Barton said:

FWIW, these has type ?m, expected X errors usually mean that Lean already tried the obvious ?m = X but it failed for some reason generally having to do with type classes

The same error can sometimes pop up because of universe issues, but you can diagnose those by using set_option pp.universes true.

[Eric Wieser]

Reid Barton said:

Shouldn't that instance have some lower priority?

That doesn't really make the problem go away, it just makes it appear less often

[Eric Wieser]

There has been discussion in the past about how to fix the qsmul diamond in the same way we fixed nsmul and zsmul, but it never got implemented

[Reid Barton]

Problems appearing less often is good though, right? Like, we already have a linter for catch-all instances don't we?

[Reid Barton]

I assume it doesn't fire on this instance because it has multiple parameters and one of them is not a variable?

[Eric Wieser]

That linter is there to catch performance issues, not surprising instances

[Eric Wieser]

You still run into the same typeclass diamond if you have a lemma about a general [division_ring R] [char_zero R] that uses the "obvious" ℚ-action, then specialize it to R=ℚ.

[Eric Wieser]

The two solutions are either:

• Add [module ℚ R] to all such lemmas (like we do with decidable) so that we never state anything about a specific instance.
• Make the diamond defeq by adding data to division_ring (like we do with add_monoid.nsmul)

[Reid Barton]

• Delete the instance

[Reid Barton]

Eric Wieser said:

That linter is there to catch performance issues, not surprising instances

Hmm, that itself comes as a surprise to me.

[Eric Wieser]

Yes, deleting or hiding in a locale would be part of the first bullet most likely

[Eric Wieser]

The priority linter is there to force a breadth-first search, and stop lean trying to solve semiring R by looking for field R before having exhausted all the direct instances