Tensor Products

Stream: new members

[Zhangir Azerbayev]

Hi everyone. I'm trying to do some basic stuff with tensor products.

import tactic
import data.real.basic
import linear_algebra.basic
import linear_algebra.finite_dimensional
import linear_algebra.tensor_product

universe u
open tensor_product

variables (K V : Type u) [field K] [add_comm_group V] [module K V]
[finite_dimensional K V]
variables v w : V

#check V ⊗ₜ[K] V
#check  v ⊗ₜ[K] w

The error message I'm getting is

failed to synthesize type class instance for
K V : Type u,
...
⊢ add_comm_group (Type u)

Does anyone know what add_comm_group (Type u) means?

[Mario Carneiro]

It's trying to infer an instance of add_comm_group for Type, which doesn't have one because the universe is not a group

[Mario Carneiro]

This sometimes happens when you write things like nat + int

[Mario Carneiro]

The issue appears to be that ⊗ₜ is tensor_group.tmul, which is the multiplication of vectors inside the tensor product. It is not the tensor product type itself

[Mario Carneiro]

The notation for the type itself is V ⊗[K] V although it is in a locale that you have to open first

open_locale tensor_product
#check (v ⊗ₜ[K] w : V ⊗[K] V)

[Zhangir Azerbayev]

I see, thank you @Mario Carneiro . What is the difference between a namespace and a locale?

[Mario Carneiro]

open_locale and localized are mathlib notions (not part of lean core) for simulating namespaced notation