Hi Mingli,
welcome to the Metamath community!
You started with an interesting topic, and I hope I can assist you with
your "project".
Here is a definition that would be valid (checked nby the metamath
verifier) and hopefully fullfils your expectations:
${
$d a q v $.
$( The definition of a "quadratic form". (Contributed by ...,
5-Feb-2022.) $)
df-qfrm $a |- QFrm = { q e. ( ( Base ` ( Scalar ` V ) ) ^m ( Base ` V )
) |
A. v e. ( Base ` V ) A. a e. ( Base ` ( Scalar ` V ) )
( q ` ( a ( .s ` V ) v ) ) = ( ( a ( .r ` ( Scalar ` V ) )
a ) ( .s ` V ) ( q ` v ) ) } $.
$}
I also proved some basic theorems for this definition:
${
isqfrm.b $e |- B = ( Base ` V ) $.
isqfrm.m $e |- .x. = ( .s ` V ) $.
isqfrm.s $e |- S = ( Scalar ` V ) $.
isqfrm.k $e |- K = ( Base ` S ) $.
isqfrm.t $e |- .X. = ( .r ` S ) $.
$( The predicate "is a quadratic form". (Contributed by ...,
5-Feb-2022.) $)
isqfrm $p |- ( Q e. QFrm <-> ( Q e. ( K ^m B ) /\ A. v e. B A. a e. K
( Q ` ( a .x. v ) ) = ( ( a .X. a ) .x. ( Q ` v ) ) ) )
$=
? $.
$( A quadratic form is a function from a class ` B ` (usually the base
set
of a vector space) to the base set ` K ` of its scalars ` S `
(usually a
field). (Contributed by ..., 5-Feb-2022.) $)
qfrmf $p |- ( Q e. QFrm -> Q : B --> K ) $=
?$.
$( The property of a quadratic form as a function from a class ` V `
(usually a vector space) to its scalars ` S ` (usually a field).
(Contributed by ..., 5-Feb-2022.) $)
qfrmprop $p |- ( ( Q e. QFrm /\ X e. B /\ A e. K )
-> ( Q ` ( A .x. X ) ) = ( ( A .X. A ) .x. ( Q ` X ) )
) $=
? $.
$}
Maybe you want to prove them by yourself as an exercise...
Here some remarks you should consider:
* The definition does not require V to be a vector space. It can also be a
left module or anything else having scalars. If it is important that V is a
vector space for a specific theorem, it must be provided as antecedent,
e.g., ( ( V e. LVec /\ Q e. QFrm ) -> ...)
* In set.mm, we distingush between groups, rings, fields, etc. (as tuples
of a base set and several operations, represented by "extensible
structures") and the set of their elements (the base set). Example: if Q =
( B , + , * ) is the field of the rational numbers, then B is the set of
the rational numbers. QFrm should be a function mapping the elements of a
structure V (e.g., the vectors of a vector space) to the elements of the
scalar structure, therefore we use
the notation `( Base ``V )` resp. `( Base `` S )` for the domain and the
codomain of QFrm.
* In a definition, we usually have to use all required construct explicitly
(that's why it looks so complicated), whereas in theorems we can use class
variables to abbreviate complex constructs, e.g., K = ( Base ` S )= ( Base
` ( Scalar ` V ) ) as the base set of the scalar (field) S of (the vector
space) V. Theorem ~isqfrm is a direct translation of the definition, using
such class variables. As you can see, this is much better to comprehend. In
practice, the definition itself would mostly be used in such basic theorems
only, and the basic theorems would be used in the following.
If you have further questions, don't hesitate to ask then in this forum.
Maybe others can share their experiences and opinions here, too.
By the way, in Wikipedia I read "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 and the function q(u+v)-q(u)-q(v) is
bilinear." Is the first condition really sufficient for your purposes, or
do you need the bilinearity, too?
Regarding your second question: maybe someone else has an answer for it.
Alexander
On Saturday, February 5, 2022 at 7:23:06 PM UTC+1 [email protected] 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, 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/9b0edf65-c729-4207-b775-936be2a4aa78n%40googlegroups.com.
