nondegenerate bilinear form

Stream: maths

[Jason KY.]

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]

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]

(In finite dimension these definitions are all equivalent.)

[Kevin Buzzard]

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]

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]

eg perhaps docs#quadratic_form.equivalent_one_neg_one_weighted_sum_squared should permit zeros too

[Eric Wieser]

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

[Jason KY.]

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.]

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.