Zulip Chat Archive

Stream: new members

Topic: Tensor Products


view this post on Zulip Zhangir Azerbayev (Jul 05 2020 at 23:17):

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?

view this post on Zulip Mario Carneiro (Jul 05 2020 at 23:19):

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

view this post on Zulip Mario Carneiro (Jul 05 2020 at 23:20):

This sometimes happens when you write things like nat + int

view this post on Zulip Mario Carneiro (Jul 05 2020 at 23:21):

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

view this post on Zulip Mario Carneiro (Jul 05 2020 at 23:23):

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)

view this post on Zulip Zhangir Azerbayev (Jul 05 2020 at 23:28):

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

view this post on Zulip Mario Carneiro (Jul 05 2020 at 23:29):

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


Last updated: May 08 2021 at 18:17 UTC