Tensor product on linear maps

Stream: Is there code for X?

[Iván Renison]

Hi, do we have something like this?

def LinearMap_tmul (T N : E →ₗ[𝕜] E) : E ⊗[𝕜] E →ₗ[𝕜] E ⊗[𝕜] E

I now that with T ⊗ₜ[𝕜] N I get a (E →ₗ[𝕜] E) ⊗[𝕜] (E →ₗ[𝕜] E), witch is kind of equivalent to E ⊗[𝕜] E →ₗ[𝕜] E ⊗[𝕜] E, but it not the same type (it can't be used as a function) and I have not found a way of converting from one to the other

[Kevin Buzzard]

What do you mean by "kind of equivalent"?

[Kevin Buzzard]

By the way tmul means "tensoring elements together" so that's definitely not the right name for what you're looking for -- theorems with tmul in will talk about $x\otimes y$ not $V\otimes W$.

[Iván Renison]

Kevin Buzzard said:

What do you mean by "kind of equivalent"?

I'm not sure
What I now is that when having explicit matrices and vectores (informal speaking) they are isomorphism (if not the same)

[Kevin Buzzard]

But not canonically, right? There's no natural way to get from one to the other without picking a basis I don't think.

[Jz Pan]

docs#TensorProduct.map ?

[Kevin Buzzard]

Here's how to answer your question:

@loogle LinearMap, TensorProduct

[loogle]

:search: TensorProduct.Neg.aux, LinearMap.lTensor, and 847 more

[Kevin Buzzard]

oh yikes that's too many

[Kevin Buzzard]

oh but it's only the 6th one down, and Jz has already told you the answer :-)

[Jz Pan]

Iván Renison said:

(E →ₗ[𝕜] E) ⊗[𝕜] (E →ₗ[𝕜] E), witch is kind of equivalent to E ⊗[𝕜] E →ₗ[𝕜] E ⊗[𝕜] E

Really? I don't know how to get two E →ₗ[𝕜] E back from an element of E ⊗[𝕜] E →ₗ[𝕜] E ⊗[𝕜] E.

[Iván Renison]

Jz Pan said:

docs#TensorProduct.map ?

Thanks

[Kevin Buzzard]

If everything is finite-dimensional then V tensor W and Hom(V,W) have the same dimension so if you pick bases they'll be noncanonically isomorphic.

[Iván Renison]

You are right

[Iván Renison]

I was a little confused

[Kevin Buzzard]

This is how matrices and vectors can be misleading.

[Kevin Buzzard]

It's a shame that

@loogle (?A ⊗[?k] ?B) →ₗ[?k] (?C ⊗[?k] ?D)

doesn't work

[loogle]

:exclamation: <input>:1:4: expected token

[Kevin Buzzard]

set_option pp.notation false in
#check E ⊗[𝕜] E →ₗ[𝕜] E ⊗[𝕜] E

gives

LinearMap (RingHom.id 𝕜) (TensorProduct 𝕜 E E) (TensorProduct 𝕜 E E) : Type

[Yaël Dillies]

docs#TensorProduct.map ?

[Kevin Buzzard]

yes we got there a while ago :-)

[Yaël Dillies]

Sorry, I sent this message 12min ago

[Kevin Buzzard]

The game now is to make loogle find it painlessly

[Kevin Buzzard]

@loogle |- LinearMap (RingHom.id ?k) (TensorProduct ?k ?A ?B) (TensorProduct ?k ?C ?D)

[loogle]

:search: TensorProduct.Neg.aux, LinearMap.lTensor, and 3 more

[Kevin Buzzard]

That's a bit more reasonable

[Jz Pan]

Frankly, in mathematics don't know how to construct (E ⊗[𝕜] E →ₗ[𝕜] E ⊗[𝕜] E) →ₗ[𝕜] ((E →ₗ[𝕜] E) ⊗[𝕜] (E →ₗ[𝕜] E))

[Kevin Buzzard]

If E is finite-dimensional and you pick an ordered basis of E and then choose a method of getting ordered bases of V tensor W and Hom(V,W) from ordered bases of V and W and then you identify every n-dimensional vector space equipped with an ordered basis with k^n then it's just the identity map.

[Kevin Buzzard]

If you think about it this way then you can see they are kind of equivalent.

[Kevin Buzzard]

This is exactly how not to do linear algebra.

[Jz Pan]

OK the bundled version is docs#TensorProduct.homTensorHomMap

[Jz Pan]

If it is bijective then it is indeed an isomorphism. Although we don't know how to write down its inverse.

[Jz Pan]

Kevin Buzzard said:

If everything is finite-dimensional then V tensor W and Hom(V,W) have the same dimension so if you pick bases they'll be noncanonically isomorphic.

But this argument indeed shows that the canonical forward map is bijective. So it is isomorphic. The inverse map must also be "canonical"...

[Kevin Buzzard]

We are identifying a finite-dimensional vector space with its dual here, nothing is canonical.

[Kevin Buzzard]

The canonical thing is that in the finite-dimensional case $Hom(V,W^*)=(V\otimes W)^*$ (this is just curry/uncurry) and if everything is equal to its dual because the transpose of a row vector is a column vector then you can just remove the stars.

[Eric Wieser]

Kevin Buzzard said:

It's a shame that

...

doesn't work

@loogle open scoped TensorProduct in (?A ⊗[?k] ?B) →ₗ[?k] (?C ⊗[?k] ?D)

[loogle]

:search: TensorProduct.Neg.aux, LinearMap.lTensor, and 293 more

[Eric Wieser]

Kevin Buzzard said:

But not canonically, right? There's no natural way to get from one to the other without picking a basis I don't think.

@loogle open scoped TensorProduct in (_ →ₗ[?𝕜] _) ⊗[?𝕜] (_ →ₗ[?𝕜] _), open scoped TensorProduct in (_ ⊗[?𝕜] _) →ₗ[?𝕜] (_ ⊗[?𝕜] _)

[loogle]

:search: TensorProduct.homTensorHomMap, TensorProduct.homTensorHomMap_apply, and 4 more

[Eric Wieser]

So docs#homTensorHomEquiv is the basis-agnostic equivalence (it doesn't depend on the choice, but does still need one)