76 views

Skip to first unread message

Feb 5, 2022, 1:23:06 PMFeb 5

to meta...@googlegroups.com

Hi, folks,

```metamath

$(

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

$(

=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

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 }

$.

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)

```

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

Feb 5, 2022, 4:14:05 PMFeb 5

to Metamath

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 ) ) } $.

$}

$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 ) ) ) $=

? $.

$}

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

Feb 5, 2022, 6:10:15 PMFeb 5

to Metamath

Hi Mingli,

(2) How can we express something like a type with parameter and the initialization of a type with parameter.

I'm not an expert, so don't take my word for it. But let me guess. Haskell is based on simple type theory while set.mm is ZFC, i.e. set theory. They are different beasts. You can embed type theory, of course, but that would not be set.mm anymore, IMHO.

But maybe some real expert will say that I'm telling nonsensicality and this should be easy to do :)

Feb 5, 2022, 10:26:01 PMFeb 5

to meta...@googlegroups.com

Thanks, Alex and vvs

Quadratic form is widely used, but looks like it is still missing in metamath.

I guess I need the bilinear condition but I'm not sure about it. In fact, following paper[1], I am trying to solve Pascal's Hexagon theorem.

If not wrong, I did not see too many obstacles for the formalization of the simple proof.

The next step is to introduce homogeneous coordinates which connect conic sections in 2d with quadratic form in 3d.

And then by some algebraic property of cross product in 3d space to prove the theorem.

(we still do not have cross product in 3d?)

Maybe difficult for a newbie to solve, at least it is a good chance for exercises.

So far the learning curve is a little bit steep because a lot of conventions are not documented?

But the community is very nice, which reminds me of Norm.

[1]: A very simple proof of Pascal’s hexagon theorem and some applications by Nedeljko Stefanovic and Milos Milosevic

--

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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4bef40e5-3ab7-402d-850c-e08aaeb0edcan%40googlegroups.com.

Feb 6, 2022, 1:39:19 AMFeb 6

to metamath

On Sat, Feb 5, 2022 at 6:10 PM vvs <vvs...@gmail.com> wrote:

Hi Mingli,(2) How can we express something like a type with parameter and the initialization of a type with parameter.I'm not an expert, so don't take my word for it. But let me guess. Haskell is based on simple type theory while set.mm is ZFC, i.e. set theory. They are different beasts. You can embed type theory, of course, but that would not be set.mm anymore, IMHO.But maybe some real expert will say that I'm telling nonsensicality and this should be easy to do :)

That's nonsense, this should be easy to do. :) The equivalent of a type with a parameter in set.mm is a function from sets to sets. You use function application to represent the application of the type function to some particular type.

This has already appeared in this thread: in AV's code you have ( QFrm ` V ) as the type of all quadratic forms over V. Or rather it should read that: there appears to be an error in the code, and the code as written would have tripped the definition checker. Here's a revised version (still not checked though):

This has already appeared in this thread: in AV's code you have ( QFrm ` V ) as the type of all quadratic forms over V. Or rather it should read that: there appears to be an error in the code, and the code as written would have tripped the definition checker. Here's a revised version (still not checked though):

${

$d a q v $.

$( The definition of a "quadratic form". (Contributed by ...,

5-Feb-2022.) $)

df-qfrm $a |- QFrm = ( w e. _V |-> { 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 ) ) } ) $.

$}

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 ) ) } ) $.

$}

${

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.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 ` V ) <-> ( 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 ` V ) -> 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 ` V ) /\ X e. B /\ A e. K )

-> ( Q ` ( A .x. X ) ) = ( ( A .X. A ) .x. ( Q ` X ) ) ) $=

? $.

? $.

$}

Sometimes, when it is important for the input to be a proper class, type level functions can also be written as term constructors from class to class instead. For example, the equivalent of Haskell's [a] type, the type of lists (let's ignore the infinite ones), is "Word A" in set.mm. An element of Word A is a finite list of elements drawn from A.

Sometimes, when it is important for the input to be a proper class, type level functions can also be written as term constructors from class to class instead. For example, the equivalent of Haskell's [a] type, the type of lists (let's ignore the infinite ones), is "Word A" in set.mm. An element of Word A is a finite list of elements drawn from A.

There is no particularly convenient way to define inductive datatypes in metamath as in Haskell, but it is possible to define a type of trees or other such things via a fixpoint construction. We should probably have a simpler mechanism for this.

Feb 6, 2022, 3:19:44 AMFeb 6

to Metamath

On Sunday, February 6, 2022 at 7:39:19 AM UTC+1 di....@gmail.com wrote:

...

This has already appeared in this thread: in AV's code you have ( QFrm ` V ) as the type of all quadratic forms over V. Or rather it should read that: there appears to be an error in the code, and the code as written would have tripped the definition checker. Here's a revised version (still not checked though):

Sorry for my mistake, and many thanks to Mario who detected it. It was a little late last night, and I only used metamath.exe to check the definition and the theorems, and not mmj2 which would have detected the mistake by its soundness checks. Of course, the class/vector space V should not be used directly in the definition, but should be made variable by defining QFrm as funktion mapping a set/vector space V to the set of the quadratic forms over this set/vector space.

I'll revise my definition and theorems according to Mario's suggestion (at least the distinct variable conditions must be adjusted, and some subtleties with V being a proper class must be considered) in the near future.

Feb 6, 2022, 3:40:56 AMFeb 6

to meta...@googlegroups.com, Mingli Yuan

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

--

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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAGDRuAg4F%3Deb2qSTLBsXwX7yz05W7b6PBR%2BX%2B2Q-zCBB7E6RbA%40mail.gmail.com.

Feb 6, 2022, 7:11:07 AMFeb 6

to Metamath

Here is, as promised, the corrected theorem and related basic theorems, checked by metamath.exe as well as mmj2. Theorem
qfrm was added, which charaterizes the set of quadratic forms over a set/vector space V. See the remarks in its comment about the necessity of V to be a set. Of course, the bilinearity has to be added, as described by Thierry.

${

$d a q v w $.

$( The definition of a "quadratic form". (Contributed by ...,

5-Feb-2022.) $)

$d a q v w $.

$( The definition of a "quadratic form". (Contributed by ...,

5-Feb-2022.) $)

df-qfrm $a |- QFrm = ( w e. _V

|-> { q e. ( ( Base ` ( Scalar ` w ) ) ^m ( Base ` w ) ) |

A. v e. ( Base ` w ) A. a e. ( Base ` ( Scalar ` w ) )

( q ` ( a ( .s ` w ) v ) )

( q ` ( a ( .s ` w ) v ) )

= ( ( a ( .r ` ( Scalar ` w ) ) a ) ( .s ` w ) ( q ` v ) ) } ) $.

$}

${

$d B q w $. $d K q w $. $d U w $. $d V a q v w $. $d .x. w $.

$d .X. w $.

$}

${

$d B q w $. $d K q w $. $d U w $. $d V a q v w $. $d .x. w $.

$d .X. w $.

qfrm.b $e |- B = ( Base ` V ) $.

qfrm.m $e |- .x. = ( .s ` V ) $.

qfrm.s $e |- S = ( Scalar ` V ) $.

qfrm.k $e |- K = ( Base ` S ) $.

qfrm.t $e |- .X. = ( .r ` S ) $.

$( The set of quadratic forms over a set ` V `. The assumption that ` V `

must be a set (` V e. U `) is necessary, because if ` V ` was a proper

class (` V e/ _V `) , then ` ( QFrm `` V ) = (/) ` (see ~ fvprc ), but

the right hand side of the equation would be ` { (/) } =/= (/) `

(see ~ mapdm0 and ~ ral0 ). Usually, ` V ` will be a vector space

(` U = LVec `, i.e. ` V e. LVec `). (Contributed by ...,

5-Feb-2022.) $)

qfrm $p |- ( V e. U -> ( QFrm ` V ) = { q e. ( K ^m B ) |

must be a set (` V e. U `) is necessary, because if ` V ` was a proper

class (` V e/ _V `) , then ` ( QFrm `` V ) = (/) ` (see ~ fvprc ), but

the right hand side of the equation would be ` { (/) } =/= (/) `

(see ~ mapdm0 and ~ ral0 ). Usually, ` V ` will be a vector space

(` U = LVec `, i.e. ` V e. LVec `). (Contributed by ...,

5-Feb-2022.) $)

qfrm $p |- ( V e. U -> ( QFrm ` V ) = { q e. ( K ^m B ) |

A. v e. B A. a e. K

( q ` ( a .x. v ) ) = ( ( a .X. a ) .x. ( q ` v ) ) } ) $=

? $.

$d Q a q v $. $d .x. q $. $d .X. q $.

$( The predicate "is a quadratic form". (Contributed by ...,

5-Feb-2022.) $)

isqfrm $p |- ( V e. U -> ( Q e. ( QFrm ` V ) <-> ( Q e. ( K ^m B )

? $.

$d Q a q v $. $d .x. q $. $d .X. q $.

$( The predicate "is a quadratic form". (Contributed by ...,

5-Feb-2022.) $)

isqfrm $p |- ( V e. U -> ( Q e. ( QFrm ` V ) <-> ( 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 ` V ) -> Q : B --> K ) $=

? $.

$d A a $. $d B v $. $d K a v $. $d Q a v $. $d X a v $.

$d .x. a v $. $d .X. a v $.

$d .x. a v $. $d .X. a v $.

$( 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.) $)

Feb 6, 2022, 8:44:35 AMFeb 6

to Metamath

That's nonsense, this should be easy to do. :) The equivalent of a type with a parameter in set.mm is a function from sets to sets. You use function application to represent the application of the type function to some particular type.

Very well, then.

Also, maybe I was looking in the wrong direction and this isn't relevant here, but function is still just an approximation and it is not a type, right? I mean, in case where you really want it to be different from set? Then it would be not enough to just define a function and you will need several theorems to prove that. And if you will use it too often then it might become annoying.

Feb 6, 2022, 10:37:58 AMFeb 6

to meta...@googlegroups.com, Mingli Yuan

Hi Mingli,

It's very good that you have a paper to follow, and very good that you set yourself as a target to prove another of the "100 theorems"! Good luck, and don't hesitate to shout for help whenever you feel blocked, I'm sure you'll find many willing to help!

The title of the paper is "A very simple proof", but not
everything is as simple as it claims ;-)

Very very quickly surveying what you might need:

It seems you're right that we do not have the 3D cross product in
Metamath yet. That's probably a very good addition! (and
absolutely necessary for that proof)

To express the Euclidean space in 3 dimensions, you can use ` (
EEhil ` 3 )` . It is defined as ` ( RR^ ( 1 ... 3 ) ) `, and
that's a structure which is also a vector space. Then, for
example, the set of quadratic forms over RR^3 will be ` ( QFrm ` (
EEhil ` 3 ) ) ` (once you've defined it!).

We already have quite some matrix algebra, defined by Stefan O'Rear and Alexander Van der Vekens.

Alexander has already introduced the concept of "linear dependency" as `linDepS` (see ~df-lindeps).

Norm has a whole chapter about projective geometry, but unfortunately I don't understand it, I can't tell whether it could be useful.

I hope this helps somehow!

BR,

_

Thierry

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAGDRuAhT3ZADrOrPF3%3D9nVv3SZCVj8ZVh5_Rv%3D%2BRZMErfqvHYQ%40mail.gmail.com.

Feb 6, 2022, 10:41:44 AMFeb 6

to metamath

There isn't really any essential way that a type is different from a set, except that a type abstracts some encoding details that sets instantiate in a particular way. That means that if you have a type you want to model then sets are a way to do it, maybe not the only way. Of course the function giving the type family is only the beginning of the story: in haskell an inductive data type comes with constructors and pattern matching, and that corresponds to functions and a recursion principle in metamath.

Feb 6, 2022, 11:11:30 AMFeb 6

to Metamath

There isn't really any essential way that a type is different from a set, except that a type abstracts some encoding details that sets instantiate in a particular way. That means that if you have a type you want to model then sets are a way to do it, maybe not the only way. Of course the function giving the type family is only the beginning of the story: in haskell an inductive data type comes with constructors and pattern matching, and that corresponds to functions and a recursion principle in metamath.

I'm thinking more about elements that may belong to many sets, while they can have only one type. Isn't that the main reason why type theory was invented in the first place? Yes, it's possible to use set theory with particular axioms like ZFC, but trying to model type theory inside it kinda defeats the purpose. Why not implement type theory in Metamath then?

Feb 6, 2022, 2:47:19 PMFeb 6

to metamath

On Sun, Feb 6, 2022 at 11:11 AM vvs <vvs...@gmail.com> wrote:

There isn't really any essential way that a type is different from a set, except that a type abstracts some encoding details that sets instantiate in a particular way. That means that if you have a type you want to model then sets are a way to do it, maybe not the only way. Of course the function giving the type family is only the beginning of the story: in haskell an inductive data type comes with constructors and pattern matching, and that corresponds to functions and a recursion principle in metamath.I'm thinking more about elements that may belong to many sets, while they can have only one type. Isn't that the main reason why type theory was invented in the first place? Yes, it's possible to use set theory with particular axioms like ZFC, but trying to model type theory inside it kinda defeats the purpose. Why not implement type theory in Metamath then?

Two things: (1) it's been done, see hol.mm or dtt.mm. (2) It's not necessary; type theory can be simulated in set.mm without straying very far from idiomatic style, and without a lot of overhead, so it amounts to a particular way of handling propositions in ZFC. I don't see why you are so eager to say "types are not quite sets" and therefore you may as well throw away the library and get another one if you want to use type-based reasoning. Type theory thinking can still be useful without the trappings of type theory itself, and in fact type theory simulated in set theory has some advantages over pure type theory in that you can bend the rules when it is advantageous to do so. In lean, there is a concept called "defeq", or definitional equality, and it is strictly stronger than regular equality: there are things that are propositionally equal but not defeq, like x + (y + z) and (x + y) + z. You can prove these two are equal, but if you have a type family indexed in natural numbers and an element in F ((x + y) + z) you can't just treat it as an element of F (x + (y + z)). In metamath you can; since the values are equal the sets are equal so any element of one is also an element of the other. Defeq is simply not a thing in metamath, and this is very freeing.

Feb 6, 2022, 3:23:57 PMFeb 6

to meta...@googlegroups.com

At least in my email cilent these got linked funny. The
references are to http://us.metamath.org/holuni/mmhol.html and
https://github.com/digama0/dtt.mm respectively, as far as I know.
Hope that helps people follow along in case anyone is unfamiliar.

Feb 6, 2022, 7:00:49 PMFeb 6

to Metamath

I don't see why you are so eager to say "types are not quite sets"

I am not, I think. I don't really care. I'm trying to avoid being biased but fall in that trap over and over again.

But I know that such people exist and I don't know why someone should insist that they are wrong just because somebody else have a different opinion. This is also a philosophical difference, not just a practical one. But even from a practical point of view everyone have their own definition of feasibility. We can walk backwards or even upside down, that's certainly possible, but not everyone will find this quite feasible. And when I'm not sure what solution is feasible in this particular case, I prefer to reason conservatively. But maybe I'm overreacting sometimes.

Type theory thinking can still be useful without the trappings of type theory itself, and in fact type theory simulated in set theory has some advantages over pure type theory in that you can bend the rules when it is advantageous to do so.

And not everyone will like it. Should we say that there is only one single truth?

In lean, there is a concept called "defeq", or definitional equality, and it is strictly stronger than regular equality: there are things that are propositionally equal but not defeq, like x + (y + z) and (x + y) + z. You can prove these two are equal, but if you have a type family indexed in natural numbers and an element in F ((x + y) + z) you can't just treat it as an element of F (x + (y + z)). In metamath you can; since the values are equal the sets are equal so any element of one is also an element of the other. Defeq is simply not a thing in metamath, and this is very freeing.

Ok. But this is starting to sound like a preaching :) And don't take me wrong. If you feel so strongly about this issue I won't continue to try to dissuade you. Probably this discussion already turned into bikeshedding and I should stop arguing and do something useful instead :) I'm sorry.

Feb 6, 2022, 8:59:21 PMFeb 6

to meta...@googlegroups.com

Thanks, Thierry, Mario and Alex, I will follow your advice, and take the exercise. :-)

The community is so friendly! I will ask if I am blocked.

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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/14ce5c0a-44e9-4ee8-b6be-ac2d67848ac8n%40googlegroups.com.

Feb 7, 2022, 7:23:38 PMFeb 7

to Metamath

Sorry, I'm a bit late to the party. As has been noted, you also need bilinearity of the associated
symmetric form. Without it, you are simply defining homogeneous
functions of degree two.

Also, quadratic forms should be defined in set.mm on (left) modules for wider applicability (even if some results might be funny over noncommutative rings).

As
for the first point, the associated symmetric form is probably
important enough that a definition would be useful. Here is a proposal
(I do not remember the names of the components of an extensible
structure, so I put mnemonic ones):

$(
Define the function associating with a function ` q ` from a magma to a
group its "associated binary form". For its value, see ... It is
symmetric as soon as the magma and the group are commutative (with no
condition on q), see ... It is bilinear when the magma and the group
are respectively a module and its ring of scalars and ` q ` is a
quadratic form (this is actually part of the definiton of a quadratic
form, see ~df-qform ). $)

df-assocbiform $a assoc_bi_form = ( m e. Magma , g e. Group |->

( q e. ( ( Base `g ) ^m ( Base ` m ) ) |->

( x , y e.
( Base ` m ) |-> ( ( q ` ( x ( Plus ` m ) y ) )

( Plus ` g )

( ( Opposite ` g ) ` ( ( q ` x ) ( Plus ` g ) ( q ` y ) ) ) ) ) ) ) $.

If homogeneous functions are to be defined, then maybe (restricting to the case domain=codomain):

df-homog $a Homog = ( x e. ScalSet |-> ( d e. NN0 |-> { f e. ( ( Base ` x ) ^m ( Base ` x ) ) |

A. a e. ( Base ` x ) A. s e. ( Base ` ( Scalar ` x ) ) ( f ` ( s (
scalmul ` x ) a ) ) = ( s^d ( scalmul ` x ) ( f ` a ) ) } ) ) $.

(s^d is probably defined somewhere in set.mm
but I do not know the syntax, and ScalSet is the class of "sets with a
magma of scalars", or "M-sets" if M is said magma, sometimes "sets with
operators", as in group actions).

Then, quadratic forms can be defined by:

df-qform $a QForm = ( m e. LMod |-> { q e. ( ( Homog ` m ) ` 2 ) |
( ( M
assoc_bi_form ( Scalar ` M ) ) ` q ) e. ( BilinForm ` m ) } ) $.

df-bilinform $a BilinForm = ( m e. LMod |-> { q e.
( ( Base ` ( Scalar `m ) ) ^m (
( Base ` m )
X. ( Base ` m )
) ) | [ the two partial functions are linear forms ] } ) $.

If notation becomes too heavy, one can use "local variables" in the form " [ z / ( Base ` x ) ] ... " as is done in a few other definitions in set.mm, if I recall correctly.

Benoît

Feb 11, 2022, 2:54:30 AMFeb 11

to meta...@googlegroups.com

Hi, Benoit and others, thanks for your reply. Let me keep a weekly pace to learn metamath step by step.

I still stick to Alex's assignment :-) - try to complete the proofs he left in the first reply.

I still stick to Alex's assignment :-) - try to complete the proofs he left in the first reply.

Yes and of course, I was blocked by questions. I record the learning process and give comments and questions as below.

It is a little bit long and preliminary, but maybe the next newcomers can learn faster and easier.

```metamath

$( A field is a commutative division ring. (Contributed by Mario Carneiro,17-Jun-2015.) $)

isfld $p |- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) ) $=

( cdr ccrg cfield df-field elin2 ) ABCDEF $.

$c Field $.

$( Extend class notation with class of all division rings. $)

cdr $a class DivRing $.

$( Class of fields. $)

cfield $a class Field $.

$( Define class of all division rings. A division ring is a ring in which

the set of units is exactly the nonzero elements of the ring.

(Contributed by NM, 18-Oct-2012.) $)

df-drng $a |- DivRing = { r e. Ring |

( Unit ` r ) = ( ( Base ` r ) \ { ( 0g ` r ) } ) } $.

$( A _field_ is a commutative division ring. (Contributed by Mario Carneiro,

17-Jun-2015.) $)

df-field $a |- Field = ( DivRing i^i CRing ) $.

```

${

elin2.x $e |- X = ( B i^i C ) $.

$( Membership in a class defined as an intersection. (Contributed by

Stefan O'Rear, 29-Mar-2015.) $)

elin2 $p |- ( A e. X <-> ( A e. B /\ A e. C ) ) $=

( wcel cin wa eleq2i elin bitri ) ADFABCGZFABFACFHDLAEIABCJK $.

$}

I had read the manual - *metamath* by Norm, and I understood the RPN notion and the stack.

Also I checked several examples, e.g.,

Also I checked several examples, e.g.,

```metamath

$( A field is a commutative division ring. (Contributed by Mario Carneiro,17-Jun-2015.) $)

isfld $p |- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) ) $=

( cdr ccrg cfield df-field elin2 ) ABCDEF $.

```

The proof here starts with cdr which is a class notion, and I understand here is one abstract layer based on the class notion.

And based on the abstract layer we can set up more advanced math. In my understanding, it also means if we grasp several rules

above the layer we can safely ignore the detail beneath the layer. Those are the assumptions I started to explore.

I copy the definitions of field and elin2 for reference

```metamath

$c DivRing $.$c Field $.

$( Extend class notation with class of all division rings. $)

cdr $a class DivRing $.

$( Class of fields. $)

cfield $a class Field $.

$( Define class of all division rings. A division ring is a ring in which

the set of units is exactly the nonzero elements of the ring.

(Contributed by NM, 18-Oct-2012.) $)

df-drng $a |- DivRing = { r e. Ring |

( Unit ` r ) = ( ( Base ` r ) \ { ( 0g ` r ) } ) } $.

$( A _field_ is a commutative division ring. (Contributed by Mario Carneiro,

17-Jun-2015.) $)

df-field $a |- Field = ( DivRing i^i CRing ) $.

```

${

elin2.x $e |- X = ( B i^i C ) $.

$( Membership in a class defined as an intersection. (Contributed by

Stefan O'Rear, 29-Mar-2015.) $)

elin2 $p |- ( A e. X <-> ( A e. B /\ A e. C ) ) $=

( wcel cin wa eleq2i elin bitri ) ADFABCGZFABFACFHDLAEIABCJK $.

$}

```

In order to understand how proof of isfld works, I use below command to show

```

MM > show proof isfld /renumber /lemmon

1 df-field $a |- Field = ( DivRing i^i CRing )

2 1 elin2 $p |- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) )

1 df-field $a |- Field = ( DivRing i^i CRing )

2 1 elin2 $p |- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) )

```

and

```

MM> show proof isfld

5 elin2.x=df-field $a |- Field = ( DivRing i^i CRing )

6 isfld=elin2 $p |- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) )

5 elin2.x=df-field $a |- Field = ( DivRing i^i CRing )

6 isfld=elin2 $p |- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) )

```

My questions here are:

1. In the manual by Norm, a simple example was given at page 137, it pushes several $f or $ e into the stack,

and when it meets assertions, it will match and substitute.

Considering proof

```metamath

( cdr ccrg cfield df-field elin2 ) ABCDEF $.

( cdr ccrg cfield df-field elin2 ) ABCDEF $.

```

So the question here is: cdr, ccrg, cfield, df-field are all $a, and only elin2 is a $p, where are the $f or $ e?

2. Fortunately, I check the manual and found a /all option and mention about syntax construction, so we have

```

MM> show proof isfld /all

1 cA=cR $f class R

2 cB=cdr $a class DivRing

3 cC=ccrg $a class CRing

4 cX=cfield $a class Field

5 elin2.x=df-field $a |- Field = ( DivRing i^i CRing )

6 isfld=elin2 $p |- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) )

1 cA=cR $f class R

2 cB=cdr $a class DivRing

3 cC=ccrg $a class CRing

4 cX=cfield $a class Field

5 elin2.x=df-field $a |- Field = ( DivRing i^i CRing )

6 isfld=elin2 $p |- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) )

```

But where does step 1 come from? and when the verifier reads cdr in step 2, what does it happen?

It seems I should understand how class notions take effect precisely?

3. If we could ignore the class notions here as an abstraction layer, maybe we can understand the proof as process below

```

1. cdr a label and class of DivRing, left it in scope

2. ccrg a label and class of CRing, left it in scope

3. cfield a label and class of Field, left it in scope

4. df-field construct class by defined constructions and assigned it to label Field, left it in scope

5. elin2.x matched by Field

6. elin2 takes effect by elin2 and QED.

```

I know this understanding is only roughly true but not precisely.

Thanks in advance.

Mingli

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/c9b002d5-1182-4ddc-b4cd-8e6502a2ad66n%40googlegroups.com.

Feb 11, 2022, 6:24:52 AMFeb 11

to Metamath

The proofs in set.mm are written in the "compressed" format (described in an appendix of the book). If you want to see the "normal" uncompressed format, which best permits to understand the proof stack, type

MM> show proof isfld /normal

Proof of "isfld":

---------Clip out the proof below this line to put it in the source file:

cR cdr ccrg cfield df-field elin2 $.

---------The proof of "isfld" (33 bytes) ends above this line.

Proof of "isfld":

---------Clip out the proof below this line to put it in the source file:

cR cdr ccrg cfield df-field elin2 $.

---------The proof of "isfld" (33 bytes) ends above this line.

I think with this, you'll understand how this works.

That being said, understanding the proof verification mechanism will not help you (or only very remotely) in understanding the math, and conversely. You can learn them separately.

Benoît

Feb 11, 2022, 6:55:24 AMFeb 11

to meta...@googlegroups.com, Mingli Yuan

Hi Mingli,

You're trying to understand how a proof is stored and verified.There's absolutely nothing wrong with that, but I just wanted to state that it's not mandatory that you understand those.

I think when I first started with Metamath, I focused on
understanding simple proofs on the website, or on MMJ2 (both are
similar), created my first proofs and let the tool (MMJ2) store
and verified the proof for me. I consider the compressed proof
format like a kind of "binary executable" which we don't
absolutely need to understand and read.

MMJ2 and the website both hide some steps of the proof
(syntactical steps) and allows you focus on the more important
ones (logical steps).

Like all proofs in set.mm, the proof you chose is provided in compressed format. That format favors space over readability, so as few information as possible is included.1. So the question here is: cdr, ccrg, cfield, df-field are all $a, and only elin2 is a $p, where are the $f or $ e?

The $f and $e hypotheses which are "in scope" are known, so they do not need not repeated in the statement list in parentheses. That format is described in appendix B. of the Metamath Book, which states:

If the statement being proved has m mandatory hypotheses,integers 1 through m correspond to the labels of these hypotheses in theorder shown by the show statement ... / full command, i.e., the RPNorder of the mandatory hypotheses.

Here is the output of that command:

67962 isfld $p |- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) ) $= ... $.

Its mandatory hypotheses in RPN order are:

cR $f class R $.

So there is a single mandatory hypothesis, which is `cR`,
referred to by a `A` in the compressed proof (here A encodes to
integer 1).

MM> show proof isfld /all

1 cA=cR $f class R

2 cB=cdr $a class DivRing

3 cC=ccrg $a class CRing

4 cX=cfield $a class Field

5 elin2.x=df-field $a |- Field = ( DivRing i^i CRing )

6 isfld=elin2 $p |- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) )

```

2. But where does step 1 come from? and when the verifier reads cdr in step 2, what does it happen?

It seems I should understand how class notions take effect precisely?

...and that's where the `cR` comes from, since `A` is the first
character of the compressed proof (ABCDEF).

What happens is that the statement with a single "class R" is stored on the proof stack.

Here is how I would describe the rest of the verification
process:

Next, `B` is read, which refers to `cdr`. This pushes "class DivRing" on the stack, which now contains "class R / class DivRing".

And so on until step 5, where the stack contains "class R / class DivRing / class CRing / class Field / |- Field = ( DivRing i^i CRing )".

Then, at step 6, `elin2` in invoked, which requires 4 variables :
A, X, B and C, and an hypothesis ~elin2.x of the form `|- X = ( B
i^i C ) `.

All 5 items are popped from the stack, in the order in which they are declared:

- A, which is substituted by R
- B, substituted by DivRing
- C, substituted by CRing
- X, substituted by Field
- |- X = ( B i^i C ), substituted by Field = ( DivRing i^i CRing
). The verifier checks that this substitution matches.

Finally, the statement of elin2 is pushed on the stack: |- ( A e. X <-> ( A e. B /\ A e. C ) )

Which, when substituted, results in |- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) ).

That is the final and only expression remaining on the proof
stack, and the verifier finally verifies that this matches with
the statement of ~isfld.

And that's it! Luckily this was a very short proof!

In practice, if you had used MMJ2 or checked the website proof of isfld, you can see that that proof only has 2 steps: 1-4 are hidden, and only 5-6 are shown.

That's because steps 1-4 only deal with "syntactically" building
the expressions which will later be used in substitutions, not
deriving new true statements.

BR,

_

Thierry

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAGDRuAjAUAtf9Mvz%3D7TRK3%3DtjAHPp1e0%2BWEmX61n4%2BUuqT%3DsFw%40mail.gmail.com.

Feb 11, 2022, 8:04:43 AMFeb 11

to Thierry Arnoux, meta...@googlegroups.com

Hi, Thierry and Benoit,

$( Add 'class' as a typecode. $)

$( $j syntax 'class'; $)

I had read the lines in set.mm

```

$c class $.$( Add 'class' as a typecode. $)

$( $j syntax 'class'; $)

```

So I guess the class notion is a kind of syntax sugar. I did not know mmj can simplify the development, that is why I want to understand how this mechanism works.

Right now, I know mmj and the webpage is more important for development.

Thanks

Mingli

Feb 12, 2022, 2:02:05 PMFeb 12

to Metamath

Mingli, you wrote:

> So far the learning curve is a little bit steep because a lot of conventions are not documented?

We are striving to keep documentation up-to-date and to document our conventions. For the moment, documentation is not very centralized: there is the website (e.g., http://us2.metamath.org/mpeuni/mmset.html), the github pages (like README.md and CONTRIBUTING.md), the help of the metamath program (obtained by typing MM> help [command]), the statement ~conventions in set.mm (http://us2.metamath.org/mpeuni/conventions.html#uniprg) for set.mm-specific conventions, searching within this google group.

Can you keep a log of what seems undocumented to you, and share it here once you've verified it is undocumented, so that we can add it ?

Thanks in advance.

Benoît

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu