Hi Mingli,
Let me try to add up to / complete the other answers, starting from your
own definition.
You write:
```metamath
df-qfrm $a |- QFrm = { V --> ( Scalar ` V ) | V e. LVec /\
q e. V --> ( Scalar ` V ) /\ v e. V /\ a e. ( Scalar ` V ) /\
q ` ( a .x. v ) = ( a * a ) .x. v }
$.
```
So your `QFrm` is in the form ` { A --> B | ph } `. Unfortunately, this
syntax has not been defined in set.mm. A definition for a "class of
something" has to take one of the following forms:
```metamath
cab $a class { x | ph } $.
crab $a class { x e. A | ph } $.
copab $a class { <. x , y >. | ph } $.
coprab $a class { <. <. x , y >. , z >. | ph } $.
```
The first two forms define "the set of `x` in `A` fulfilling `ph`", the
third defines a relation (like '<'), the last also defines a relation,
but with three elements.
Here, you want to define a set of mappings, so the second form is what
we need. Something like ` QFrm = { q e. M | ph(q) } `, where `q e. M`
would express "q is a mapping", and `ph(q)` would express "q is quadratic".
For "q e. M" to express "q is a mapping", we have ~df-map, and the
operation `^m`: the set of all functions that map from ` B ` to ` A ` is
written ` ( A ^m B ) `.
Here we want mappings from the base of a field V to the scalars of that
field, so we have to write ` ( Base ` ( Scalar ` V ) ) ^m ( Base ` V )
`. Alexander has explained why we need to use the ` Base ` here.
Now, a quadratic form always relates to a specific vector space. Above,
we have not defined what ` V ` is, and so our definition is not a closed
form.
There are two ways around this: either we define ` QFrm ` as the set of
all quadratic forms, regardless of the underlying vector space, or we
first fix a specific vector space, and then define the class of
quadratic forms over that specific vector space. I think the latter is
usually better, and what you try to achieve. So here what we want is a
function, mapping one vector space ` w ` to the class of quadratic forms
over ` w `, ` ( QFrm ` w ) `. Later on, we will be able to state "` Q `
is a quadratic form over V" by writing `Q e. ( QFrm ` V )`.
We can use the "maps to" notation here: ` ( w e. Field |-> F(w) ) `
stands for "the function which maps the field `w` to `F(w)`.
Putting it together, this gives:
```metamath
df-qfrm $a |- QFrm = ( w e. Field |-> { q e. ( Base ` ( Scalar ` w ) )
^m ( Base ` w ) | ph } ) $.
```
Of course I've still omitted `ph` here, which corresponds to your:
```metamath
v e. V /\ a e. ( Scalar ` V ) /\ q ` ( a .x. v ) = ( a * a ) .x. v
```
We have not introduced `v` and `a` yet though. Those are respectively
/any/ vector and /any/ scalar, so we shall use "for all": ` A. a e. (
Base ` ( Scalar ` w ) ) A. v e. ( Base ` w ) ps `
Finally, ` .x. ` is just another class variable, like ` A `. In the
theorems which make use of it, like ~ drngmcl, there is a hypothesis to
give it a value. In your definition, we cannot use such a trick, so we
have to use everything verbatim. The scalar multiplication operation of
` w ` is ` ( .s ` w ) `, so instead of ` ( a .x. v ) ` one has to write
` ( a ( .s ` w ) v ) `. This gives:
```metamath
( q ` ( a ( .s ` w ) v ) ) = ( ( a ( .r ` ( Scalar ` w ) ) a ) ( .s ` w
) ( q ` v ) )
```
It also looks like we need to express the fact that ` q(u+v) - q(u) -
q(v) ` is bilinear. It is a mapping function of two variables `u` and
`v`, so we can express it using ~ cmpt2:
```metamath
cmpt2 $a class ( x e. A , y e. B |-> C ) $.
```
Let's assume we have a similar definition for Bilinear Forms, `BFrm`. A
statement "` Q ` is a bilinear form over ` w `" is expressed ` Q e. (
BFrm ` w ) `. This gives:
```metamath
( u e. ( Base ` w ) , v e. ( Base ` w ) |-> ( q ` ( u ( +g ` w ) v ) (
-g ` ( Scalar ` w ) ) ( ( q ` u ) ( +g ` ( Scalar ` w ) ) ( q ` v ) ) )
) e. ( BFrm ` w )
```
Let's put everything together once again:
```metamath
${
$d a q v w $.
$( The definition of a "quadratic form". (Contributed by ...,
5-Feb-2022.) $)
df-qfrm $a |- QFrm = ( w e. Field |-> { q e. ( ( Base ` ( Scalar `
w ) ) ^m ( Base ` w ) ) | (
A. v e. ( Base ` w ) A. a e. ( Base ` ( Scalar ` w ) )
( q ` ( a ( .s ` w ) v ) ) = ( ( a ( .r ` ( Scalar ` w ) ) a ) ( .s ` w
) ( q ` v ) )
/\ ( u e. ( Base ` w ) , v e. ( Base ` w ) |-> ( q ` (
u ( +g ` w ) v ) ( -g ` ( Scalar ` w ) ) ( ( q ` u ) ( +g ` ( Scalar ` w
) ) ( q ` v ) ) ) ) e. ( BFrm ` w )
) } ) $.
$}
```
That shall be exactly Mario's answer, with the addition of the "bilinear
form" part. That's quite complex, but the next theorems are going to be
simpler... and Metamath forces us with some formalism (which is good!).
Actually, there is one little difference with Mario's definition. I've
written ` ( w e. Field |-> ... ) `, but we usually prefer ` ( w e. _V
|-> ... ) `. By using the universal class ` _V `, we do not force ` w `
to be a field, this allows us to be as general as possible, and define
"what a quadratic form would be if ` w ` was a vector space".
In practice, as explained by Alexander, as soon as we will need any
specific field or vector space property (say, distributivity), this will
have to appear as a hypothesis, like ` ( W e. Field -> ... ) ` or ` ( W
e. LVec -> ... `.
Of course, `BFrm`, the function mapping a field to the set of its
bilinear forms, will need to be defined first: this is left as an
exercise! ;-)
BR,
_
Thierry
On 06/02/2022 02:22, Mingli Yuan wrote:
Hi, folks,
I am a newbie and I have a question about expressing a quadratic form
over a vector space.
Just follow cases in set.mm <http://set.mm>, I give below definition
of a quadratic form
```metamath
$(
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Quadratic Form
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
A quadratic form over a field K is
a map q: V -> K from a finite-dimensional K-vector space to K
such that q(av) = a^2 q(v) for all a \in K, v \in V.
$)
$c QFrm $.
$( Extend class notation with class of all quadratic forms. $)
cqfrm $a class QFrm $.
df-qfrm $a |- QFrm = { V --> ( Scalar ` V ) | V e. LVec /\
q e. V --> ( Scalar ` V ) /\ v e. V /\ a e. ( Scalar ` V ) /\
q ` ( a .x. v ) = ( a * a ) .x. v }
$.
```
But I found it is difficult to express special quadratic forms over R^3
In Haskell or similar languages which support algebraic data types, we
can define
```haskell
data Tree a = Tip | Node (Tree a) a (Tree a)
```
Here a is a type parameter.
So my questions are:
(1) Is the definition of Quadratic Form correct?
(2) How can we express something like a type with parameter and the
initialization of a type with parameter.
Thanks a lot.
Mingli
--
You received this message because you are subscribed to the Google
Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send
an email to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAGDRuAg4F%3Deb2qSTLBsXwX7yz05W7b6PBR%2BX%2B2Q-zCBB7E6RbA%40mail.gmail.com
<https://groups.google.com/d/msgid/metamath/CAGDRuAg4F%3Deb2qSTLBsXwX7yz05W7b6PBR%2BX%2B2Q-zCBB7E6RbA%40mail.gmail.com?utm_medium=email&utm_source=footer>.
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/2e441a57-9df9-0de1-d0a6-606200185b62%40gmx.net.
