Outer product of two vectors

Stream: Is there code for X?

[Niels Voss]

Given v : E and w : F where E and F are finite-dimensional inner product spaces, how do you construct the outer product wvᴴ : E →ₗ[𝕜] F, where ᴴ denotes the conjugate transpose? I guess you can do dualTensorHom 𝕜 E F (InnerProductSpace.toDualMap 𝕜 E v ⊗ₜ[𝕜] w), but is there a better way?

[Kevin Buzzard]

It's the composite of two linear maps E->k and k->F, the first of which only depends on v and the second of which only depends on w. No doubt we have the first, I don't know about the second, but if we have both of these then probably the easiest way to make it is as the composite. Note that you only need E to have a bilinear form and you don't need anything to be finite-dimensional.

[Aaron Liu]

like this?

import Mathlib

variable {𝕜 : Type*} [RCLike 𝕜] {E F : Type*} [SeminormedAddCommGroup E] [AddCommGroup F]
    [InnerProductSpace 𝕜 E] [Module 𝕜 F]

def outerProduct (w : F) (v : E) : E →ₗ[𝕜] F :=
  .comp (LinearMap.toSpanSingleton 𝕜 F w) (innerₛₗ 𝕜 v)

[Aaron Liu]

I could probably bundle this further as being conjugate-linear in v and linear in w

[Niels Voss]

Is this something we want as a definition in mathlib?

[Aaron Liu]

since it's so short I think probably not?

[Niels Voss]

I guess it also depends on how many useful theorems can be stated about the outer product, and whether this would help or hurt discoverability

[Aaron Liu]

I feel like this would be more naturally stated with v : E →ₗ[𝕜] 𝕜 instead of v : E

[Aaron Liu]

the inner product isn't really doing anything besides attach the space to its dual

[Niels Voss]

This makes sense

[Jireh Loreaux]

Yes, although we probably want a version both for docs#Module.Dual and also docs#StrongDual. Then for Hilbert spaces we can have an abbrev.

[Niels Voss]

Do we want a version that converts a vector to its dual or should we follow Aaron's suggestion?

[Jireh Loreaux]

I'm saying the same thing as Aaron. You shouldn't take two vectors, but rather a functional and a vector.

[Niels Voss]

and should this go into mathlib?

[Jireh Loreaux]

I would like to see it, yes. This is a standard thing that comes up. For instance, I think @Monica Omar used this to show that the center of the continuous linear maps are just the scalar ones.

[Monica Omar]

there's this PR #27668 by @Iván Renison, but it's been a few months since it's been updated

[Iván Renison]

Yes, I didn't continue because I was not convinced about what I was doing with the suggestions

[Iván Renison]

Especially the name, I have always called it outer product, so naming it rankOne seems quite strange for me

[Iván Renison]

But I should I continue ir. I will try to in the next days