6 ms·

I'm talking about a practical task. Not an abstract existence result.

• xanderlewis 2y ago
  It’s not that abstract. You can literally write down the isomorphism: v —> [e_v: V* —> F, e_v(f) = f(v)].
  • g15jv2dp 2y ago
    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"?
    • ndriscoll 2y ago
      ```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.