Zulip Chat Archive

Stream: maths

Topic: nondegenerate bilinear form


Jason KY. (Mar 06 2021 at 17:59):

In PR #5814 I defined nondegenerate bilinear forms to be

def nondegenerate (B : bilin_form R M) : Prop :=
 m : M, ( n : M, B m n = 0)  m

As @Heather Macbeth pointed out this is not a symmetric definitionsince we can easily have defined it to be

def nondegenerate (B : bilin_form R M) : Prop :=
 m : M, ( n : M, B n m = 0)  m

Here (section 8.3) we have some definition of a symmetric version. Is this a better solution or should we keep it asymmetric as we have done for left cosets?

Heather Macbeth (Mar 06 2021 at 18:01):

Thank you for starting the discussion, Jason! Specifically, the lecture notes Jason linked are an example of someone choosing to define

def nondegenerate (B : bilin_form R M) : Prop :=
 m : M, (( n : M, B m n = 0)  m = 0)  (( n : M, B n m = 0)  m = 0)

Heather Macbeth (Mar 06 2021 at 18:03):

(In finite dimension these definitions are all equivalent.)

Kevin Buzzard (Mar 06 2021 at 18:20):

Is this concept useful in the infinite-dimensional setting? I have only ever seen it being used in the finite-dimensional case in which case it doesn't matter

Eric Wieser (Sep 30 2021 at 13:45):

Related to this discussion; I was able to relax some of the lemmas in #5814 to not require degeneracy, in #9465. @Jason KY., are there downstream generalizations you can think of to continue from this point?

Eric Wieser (Sep 30 2021 at 13:47):

eg perhaps docs#quadratic_form.equivalent_one_neg_one_weighted_sum_squared should permit zeros too

Eric Wieser (Sep 30 2021 at 13:48):

But then we'd need to replace units K with with_zero (units K) or similar, which probably is annoying

Jason KY. (Sep 30 2021 at 14:18):

Thanks for the PR! It looks very good. For the generalization, I did think about permitting zeros but you are right that we will need with_zero (units K) which is annoying. The proof will go as follows, we show that every symmetric quadratic form can be restricted onto the largest subspace on which it is nondegenerate and we can obtain a sum of squares for that restriction. Then by this lemma we have the complement of that subspace is orthogonal and so the quadratic form agrees with the sum of squares on the whole space.

Jason KY. (Sep 30 2021 at 14:19):

So I think the only "hard" part is to lift the restricted sum of squares to the whole space which introduces zeros but I don't believe it to be too tough.


Last updated: Dec 20 2023 at 11:08 UTC