3 ms·

For anyone not familiar with the concept, a one-form is something that takes vectors as inputs and produces numbers as outputs. See https://en.wikipedia.org/wik

For anyone not familiar with the concept, a one-form is something that takes vectors as inputs and produces numbers as outputs. See https://en.wikipedia.org/wiki/One-form https://en.wikipedia.org/wiki/One-form

smlckz 6y ago
Can I think of one-forms as partially applied (curried) dot product? (Forgive me for the usage of pseudo-Haskell notation below.) Let V F be a vector space over F. The (curried) inner product is dot :: V F -> V F -> F Now I take each vector in a vector v :: V F and apply it to ''dot'' partially to get a covector/one-form v* :: V F -> F. If I take all vectors in V F and apply each of them partially, I should get the covector space V* F :: V F -> F over the field F. Now, if this makes sense, tell me how to construct V** F from this and show that it's isomorphic to V F.
- layoutIfNeeded 6y ago
  Yes. In other words: if vectors are column vectors, then covectors are row vectors, and vice versa. In this case, taking the dual is transposing your vectors, and the transpose of a transpose gives you back the original vectors. But mathematicians try to build the most general, most abstract framework, which doesn't rely on the specifics of a concrete example (i.e. the dot product of finite-dimensional real vectors).
- ianhorn 6y ago
  dot v :: V F -> F (dot v) is a member of the dual space. To double it up with dual dual, and to do it with the same partial application construction, we need to introduce an inner product on the dual space. ddot :: (V F -> F) -> (V F -> F) -> F ddot (dot v) :: (V F -> F) -> F To identify these things, we need a bijection and we need vector space properties to match up (inner product, addition, and scaling). Starting with an inner product: dddot (ddot (dot v)) (ddot (dot w)) = dot v w Then the bijection: phi :: V F -> (V F -> F) -> F phi_inv :: ((V F -> F) -> F) -> V F phi v = ddot (dot v) phi_inv (ddot (dot v)) = v Then we'd also have to show that phi (v+w) = (phi v) +* (phi w) and the same for dual space addition and scaling phi (a v) = a phi v, etc, but it's starting to get less fun, so that's left as an exercise for the reader/next commenter. I think they fall out of my dddot definition. A gotcha here is that my dual space isn't the entire type (V F -> F), just the subset that's in the image of dot (linear transformations). That's why we can do the pattern matching in my definition of phi_inv. That's the typey way to do it and it was fun to think through. What's easier is to just think of the currying as the transpose operation and multiplication. Then appeal to transpose transpose = identity. It's handwavier, but still has the same elements if you flesh it out, I think. All that said, it's not the easiest mental model. My mental model is that vectors and one forms are for measuring against each other. You have a vector v and a form x. You apply x to measure how much v is in that direction. Like, your vector might be some coordinateless physical thing, and your one form is "meters per second in the north direction" and you can apply your form to the vector to get a good old fashioned number for its north component in meters per second.
- edflsafoiewq 6y ago
  Yes for finite-dimensional spaces. For infinite-dimensional spaces you can think of 1-forms as generalizations of a partially-applied dot product (eg. the Dirac delta function). You are asking if every covector f can be written as dot(v,—) for some v. This is true for finite-dimensional spaces (take v = f(e1)e1 + ... + f(en)en, where e1,...,en is a orthogonal basis for dot). Since v is unique, this gives an isomorphism between V and V٭ and applying the same argument to V٭ and V٭٭, those are isomorphic, so V and V٭٭ are also isomorphic. But the isomorphism depends on the choice of dot. However the map V -> V٭٭ does not depend on the choice of dot. The type is V -> (V->F) -> F so this is just (reversed) function application. You can easily show this is injective. Furthermore when V is finite-dimensional, we know from above that dim(V)=dim(V٭)=dim(V٭٭), so we know in this case it is also an iso.
- BenFrantzDale 6y ago
  Yes. And in Python I’ve used this: you can just say f = x.dot and then call f(y), which of course is the same as x.dot(y).

smlckz 6y ago

Can I think of one-forms as partially applied (curried) dot product? (Forgive me for the usage of pseudo-Haskell notation below.) Let V F be a vector space over F. The (curried) inner product is dot :: V F -> V F -> F Now I take each vector in a vector v :: V F and apply it to ''dot'' partially to get a covector/one-form v* :: V F -> F. If I take all vectors in V F and apply each of them partially, I should get the covector space V* F :: V F -> F over the field F. Now, if this makes sense, tell me how to construct V** F from this and show that it's isomorphic to V F.

layoutIfNeeded 6y ago
Yes. In other words: if vectors are column vectors, then covectors are row vectors, and vice versa. In this case, taking the dual is transposing your vectors, and the transpose of a transpose gives you back the original vectors. But mathematicians try to build the most general, most abstract framework, which doesn't rely on the specifics of a concrete example (i.e. the dot product of finite-dimensional real vectors).
ianhorn 6y ago
dot v :: V F -> F (dot v) is a member of the dual space. To double it up with dual dual, and to do it with the same partial application construction, we need to introduce an inner product on the dual space. ddot :: (V F -> F) -> (V F -> F) -> F ddot (dot v) :: (V F -> F) -> F To identify these things, we need a bijection and we need vector space properties to match up (inner product, addition, and scaling). Starting with an inner product: dddot (ddot (dot v)) (ddot (dot w)) = dot v w Then the bijection: phi :: V F -> (V F -> F) -> F phi_inv :: ((V F -> F) -> F) -> V F phi v = ddot (dot v) phi_inv (ddot (dot v)) = v Then we'd also have to show that phi (v+w) = (phi v) +* (phi w) and the same for dual space addition and scaling phi (a v) = a phi v, etc, but it's starting to get less fun, so that's left as an exercise for the reader/next commenter. I think they fall out of my dddot definition. A gotcha here is that my dual space isn't the entire type (V F -> F), just the subset that's in the image of dot (linear transformations). That's why we can do the pattern matching in my definition of phi_inv. That's the typey way to do it and it was fun to think through. What's easier is to just think of the currying as the transpose operation and multiplication. Then appeal to transpose transpose = identity. It's handwavier, but still has the same elements if you flesh it out, I think. All that said, it's not the easiest mental model. My mental model is that vectors and one forms are for measuring against each other. You have a vector v and a form x. You apply x to measure how much v is in that direction. Like, your vector might be some coordinateless physical thing, and your one form is "meters per second in the north direction" and you can apply your form to the vector to get a good old fashioned number for its north component in meters per second.
edflsafoiewq 6y ago
Yes for finite-dimensional spaces. For infinite-dimensional spaces you can think of 1-forms as generalizations of a partially-applied dot product (eg. the Dirac delta function). You are asking if every covector f can be written as dot(v,—) for some v. This is true for finite-dimensional spaces (take v = f(e1)e1 + ... + f(en)en, where e1,...,en is a orthogonal basis for dot). Since v is unique, this gives an isomorphism between V and V٭ and applying the same argument to V٭ and V٭٭, those are isomorphic, so V and V٭٭ are also isomorphic. But the isomorphism depends on the choice of dot. However the map V -> V٭٭ does not depend on the choice of dot. The type is V -> (V->F) -> F so this is just (reversed) function application. You can easily show this is injective. Furthermore when V is finite-dimensional, we know from above that dim(V)=dim(V٭)=dim(V٭٭), so we know in this case it is also an iso.
BenFrantzDale 6y ago
Yes. And in Python I’ve used this: you can just say f = x.dot and then call f(y), which of course is the same as x.dot(y).