Nondegenerate bilinear / quadratic forms

Stream: mathlib4

[David Loeffler]

Premable: One of my students (Nick Trutmann, at ETH Zürich) recently formalized a proof of the "uniqueness" part of Sylvester's law of inertia (i.e. quadratic forms over the reals have a well-defined signature), which is a long-standing TODO item for Mathlib; and I was just looking at how exactly it should be formulated in order to best fit into the library.

Question: What is the "preferred" formulation of "nondegeneracy of a bilinear / quadratic form" in Mathlib?

At the moment there is no definition for quadratic forms, and a welter of confusingly-slightly-different definitions for bilinear forms. We have

• docs#LinearMap.SeparatingLeft and docs#LinearMap.SeparatingRight: for bilinear maps X × Y → K, the assertion that there is no x with B x y = 0 for all y, resp. no y with B x y = 0 for all x (conditions which are equivalent if dim X = dim Y < ∞ or if a symmetry condition is present, which are the most important cases, but not in general).
• docs#LinearMap.Nondegenerate: condition of being both left-separating and right-separating.
• docs#LinearMap.BilinForm.Nondegenerate: copy of LinearMap.SeparatingLeft but assuming X = Y.
• docs#Matrix.Nondegenerate: matrix version of LinearMap.SeparatingLeft, again assuming X = Y.

This is rather confusing, particularly the fact that LinearMap.BilinForm.Nondegenerate is not equivalent to LinearMap.Nondegenerate! This also leads to SeparatingLeft being used in places where Nondegenerate would seem more natural, e.g. the current formulation of the existence part of Sylvester in docs#QuadraticForm.equivalent_one_neg_one_weighted_sum_squared has the nondegeneracy condition formulated as LinearMap.SeparatingLeft (QuadraticMap.associated Q), which is just ugly.

I suggest we unify LinearMap.BilinForm.Nondegenerate and LinearMap.Nondegenerate; but should we standardize on defining nondegenerate = left-separating, or nondegenerate = left and right-separating?

[David Loeffler]

(FWIW, my preference is to standardize the definition as "nondegenerate = left-separating", with lemmas saying this is equivalent to right-separating under finite-dimensionality or symmetry hypotheses; and anyone who wants the right-separating condition in situations where the two aren't equivalent can work directly with LinearMap.SeparatingRight. )
EDIT: This is probably not a good idea because it means the entire API for SeparatingLeft ends up being duplicated for Nondegenerate. Maybe we should standardize on the "both left and right separating" version; but I'm keen we should standardize on something.

[Johan Commelin]

To me the "left+right" version sounds most natural.
So I propose to deprecate docs#LinearMap.BilinForm.Nondegenerate

And then it would make sense to update docs#Matrix.Nondegenerate to match that.

[Michael Stoll]

I'd also think that "nondegenerate" should be a symmetric condition; I would find it surprising if it were one-sided...

[Johan Commelin]

But not demanding X = Y, right?

[David Loeffler]

Johan Commelin said:

So I propose to deprecate docs#LinearMap.BilinForm.Nondegenerate

Deprecations are actually a bit of a problem here: the problem is that since we are deprecating it in favour of a declaration with the same name but in a higher namespace, dot-notating on a bilinear form picks up the deprecated alias in preference to the un-deprecated def.

I can't think of a good way of solving this, other than simply not having a deprecation.

[Kevin Buzzard]

In situations that our deprecation machinery can't handle, I would imagine that a comment in the code would be appropriate, so downstream users have a chance of quickly finding out what the issue is when their code breaks.

[Eric Wieser]

We could also just change it to an abbrev

[Artie Khovanov]

Doesn't Sylvester's law of inertia hold over any ordered field?
image.png
source: Real Algebra by Knebusch and Scheiderer

[David Loeffler]

Doesn't Sylvester's law of inertia hold over any ordered field?

That depends how you want to formulate it. If you formulate it as

"for any quadratic form there is a basis where the matrix is diagonal, and the number of positive, negative, zero entries are isomorphism invariants of the form"

then any linearly ordered field is OK. If you want to state it as

"for any quadratic form there is a basis where the matrix is diagonal with all diagonal entries {0, 1, -1}, and the number of +1, -1, and 0 entries are isomorphism invariants of the form"

(which is, I think, how Sylvester originally stated it), then you need to be working over R, or at least over a linearly ordered field in which all positive elements are squares. Clearly we should have both versions.

[Artie Khovanov]

Yeah that's exactly the right setting for the second one. I guess my point is we don't need the analytic structure, completeness, whatever.

[David Loeffler]

FWIW, I agree with you, but the necessary machinery isn't there in mathlib to state it this way. (I think there are quite a few results, e.g. existence of square roots of positive-def matrices, which we currently do only over $\mathbb{R}$ because we don't have the definitions required to state them in their natural generality.)

[Artie Khovanov]

I have an open PR defining real-closed fields: #33697
This isn't quite the right generality but it's already a big improvement.

[Artie Khovanov]

Well, I suppose it's not a proper generalisation until I've proved that $\mathbb{R}$ is real closed, which isn't hard but isn't in that PR.

[David Loeffler]

This is great! I had vaguely remembered someone was working on this but I
didn't realise it was you. :-)

I am not sure this is quite the right generality for Sylvester – I think
for Sylvester the correct setting is a "Euclidean field", i.e. a
linearly-ordered field where every positive element is a square, which is
more general than being real-closed. But it is definitely good to have
real-closed fields in Mathlib in any case.

[Artie Khovanov]

Yes, I agree. I didn't know that was the name for them. My point is that the proof over real-closed fields would immediately generalise to Euclidean fields, while a proof over the reals might well not.

[David Loeffler]

Johan Commelin said:

To me the "left+right" version sounds most natural.
So I propose to deprecate docs#LinearMap.BilinForm.Nondegenerate

And then it would make sense to update docs#Matrix.Nondegenerate to match that.

I have made a PR at #34110 which makes the following changes:

• make docs#LinearMap.BilinForm.Nondegenerate into an abbrev for docs#LinearMap.Nondegenerate, as suggested by Eric;
• update docs#Matrix.Nondegenerate to match docs#LinearMap.Nondegenerate, and introduce two new predicates docs#Matrix.SeparatingLeft and docs#Matrix.SeparatingRight;
• fix downstream code appropriately.

The one slight pain point is that several downstream code files prove nondegeneracy using nondegenerate_iff_ker_eq_bot, and with the new (stronger) definition of Nondegenerate this is only true with some extra side conditions. Fortunately these are satisfied in the applications I found

There are two boring pre-requisite PR's (sorting out naming conflicts & duplication) at #34057 and #34082.

[Johan Commelin]

Let me help out the emoji bot.

[Johan Commelin]

The main PR: #34110

[Johan Commelin]

Prereq 1: #34057

[Johan Commelin]

Prereq 2: #34082

[Antoine Chambert-Loir]

My answer will come late, but there are four natural notions for bilinear forms, according to whether the left/right associated linear map is injective or an isomorphism.

[David Loeffler]

@Antoine Chambert-Loir I agree these four notions are very natural; but is it common to use the term "nondegenerate" for the condition at the associated linear map to the dual is an isomorphism? I'd call that "perfect" rather than "nondegenerate".

[Eric Wieser]

Does this mean that left and right separating should be defined in terms of injectivity rather than how they behave at zero?

[Eric Wieser]

(in order to be correctly defined for semi modules)

[Antoine Chambert-Loir]

I guess so.

[Antoine Chambert-Loir]

Some people use nondegenerate for injectivity and invertible for isomorphism.