U' ⊗ V ≃ Hom(U, V)

Stream: Is there code for X?

[Anatole Dedecker]

Do we have something like this ?

import linear_algebra.dual

open_locale tensor_product big_operators

variables {R U V : Type*} [field R] [add_comm_group U] [add_comm_group V] [module R U] [module R V]
  [finite_dimensional R U]

def tensor_equiv_hom : (module.dual R U) ⊗[R] V ≃ₗ[R] (U →ₗ[R] V) := sorry

[Oliver Nash]

I think this is en route in #10372

[Patrick Massot]

Anatole, if you ask this in relation to the sphere eversion project, you should know we already have enough using docs#continuous_linear_map.to_span_singleton that can be used as in https://github.com/leanprover-community/sphere-eversion/blob/ef9c5e678f2f7270a40592b581855e30f7ae973f/src/to_mathlib/measure_theory/parametric_interval_integral.lean#L405-L418

[Anatole Dedecker]

No no, it was because I proved this isomorphism on my own to try working with tensor product, so I was wondering if I should make a PR out of it

[Anatole Dedecker]

Although in the case I have in mind I think docs#continuous_linear_map.smul_right would be better since it doesn't "restrict" the domain to K