Zulip Chat Archive

Stream: maths

Topic: nondegenerate bilinear form


view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Heather Macbeth (Mar 06 2021 at 18:03):

(In finite dimension these definitions are all equivalent.)

view this post on Zulip 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


Last updated: May 14 2021 at 18:28 UTC