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 ) } ) $.
It remains to define the class of bilinear forms on a module:
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
On Monday, February 7, 2022 at 2:59:21 AM UTC+1 [email protected] wrote:
> 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
>
>
> On Mon, Feb 7, 2022 at 8:00 AM vvs <[email protected]> wrote:
>
>> 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
>> <https://en.wikipedia.org/wiki/Type_theory#Differences_from_Set_Theory>
>> 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.
>>
>> --
>> 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/14ce5c0a-44e9-4ee8-b6be-ac2d67848ac8n%40googlegroups.com
>>
>> <https://groups.google.com/d/msgid/metamath/14ce5c0a-44e9-4ee8-b6be-ac2d67848ac8n%40googlegroups.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/c9b002d5-1182-4ddc-b4cd-8e6502a2ad66n%40googlegroups.com.
