Hacker News new | ask | show | jobs
by g15jv2dp 668 days ago
GP is giving you an element of V**. You want to turn it into a vector. To do that, please make the inverse isomorphism explicit without using a basis. I'll wait...
2 comments

Why? All I need to prove is that I have a canonical linear map going in one direction, and that this map is a bijection. (Since I already constructed such a bijection, I could just answer "for any z in V**, take the unique element v in V such that for all w in V*, w(v) = z(w)".) Do you disagree that I provided such a map? You are correct that V** is not isomorphic to V when V is infinite-dimensional, but your statement that "when dim V is finite, you need to choose a basis of V to find an isomorphism with the bidual" is incorrect. This is elementary textbook stuff (e.g. first chapter of Wald's GR book), so I won't argue further.
I responded to a sibling comment with an explanation: https://news.ycombinator.com/item?id=41234913 But good on you for the condescension even though you didn't understand my point ;)
You said even when dim V is finite you need a basis to find an isomorphism with V**. But that’s not true. You’re right if you mean V*, but not the bidual.
I'm talking about a practical task. Not an abstract existence result.
It’s not that abstract. You can literally write down the isomorphism: v —> [e_v: V* —> F, e_v(f) = f(v)].
Are you even trying to understand my point? Yes, in that direction, explicitly constructing an element of the bidual of V from an element of V is easy. To explicitly find an element of V from the element of the bidual, you need to choose a basis. Just try it, come on! Write down the inverse isomorphism. Let \alpha be an element of V**. Then v \in V such that f(v) = \alpha (where f is the isomorphism you wrote down) is given by...?

I will help you: if (e_i) is a basis of V and (e_i^*) is its dual basis, then v = \sum_i \alpha(e_i^*) e_i. Can you find such a formula without mentioning the word "basis"?

```case class Bidual[V](v: V) { def apply(f: Dual[V]) = f(v) }

def unwrap[V](ff: Bidual[V]): V = ff.v```

There's both directions of the isomorphism explicitly defined in a programming language. No choice of basis needed to define the maps, only to prove that the constructor for Bidual really gives you all linear functionals on the dual.