## Stream: new members

### Topic: Defining degenerate quadratic forms

#### Eric Wieser (Nov 19 2020 at 19:08):

I have a definition which needs a proof that a docs#quadratic_form is non-degenerate. While I can write that as ∀ m, Q m = 0 → m = 0, it would be nice if I could write it as ¬Q.degenerate (since we already have docs#quadratic_form.pos_def).

I tried to define degenerate, but the proof I needed to get back to the form that's actually useful is ugly

import linear_algebra.quadratic_form

section degenerate
variables {R₂ : Type*} {M₂ : Type*} [add_comm_group M₂] [ring R₂] [module R₂ M₂]

/-- A degenerate quadratic form is zero on some nonzero vectors. -/
def degenerate (Q₂ : quadratic_form R₂ M₂) : Prop := ∃ x ≠ 0, Q₂ x = 0

lemma non_degenerate_iff (Q₂ : quadratic_form R₂ M₂) : ¬degenerate Q₂ ↔ ∀ x, Q₂ x = 0 ↔ x = 0 :=
by {
unfold degenerate,
split,
{ intros h x,
split,
{ have := forall_not_of_not_exists h x,
simp at this,
have := mt this,
simp at this,
exact this, },  - - what a mess!
rintro rfl,
},
rintros ha ⟨x, hx, hqx⟩,
exact hx ((ha x).mp hqx)
}

end degenerate


Would it make more sense to define non_degenerate? It would make it much easier to use, but then ¬non_degenerate is pretty ugly if that ever shows up.

Can anyone suggest how to golf the mess above?

#### Johan Commelin (Nov 19 2020 at 19:10):

My intuition says that it will be useful to define nondegenerate directly, yes.

#### Reid Barton (Nov 19 2020 at 19:10):

push_neg should help somehow

#### Johan Commelin (Nov 19 2020 at 19:10):

It's a very common assumption. More common then assuming that something is degenerate.

#### Eric Wieser (Nov 19 2020 at 19:11):

Indeed - it just seems unfortunate to me to use not in a name when we already have a symbol for it

#### Johan Commelin (Nov 19 2020 at 19:12):

Maybe we should call them smooth?

#### Johan Commelin (Nov 19 2020 at 19:12):

smooth = nonsingular = nondegenerate

#### Reid Barton (Nov 19 2020 at 19:12):

oh I see, part of the problem is you have an iff on the nondegenerate side

#### Eric Wieser (Nov 19 2020 at 19:12):

I can remove that iff

#### Eric Wieser (Nov 19 2020 at 19:12):

Since the reverse direction is obvious and holds for all Q anyway (docs#quadratic_form.map_zero)

#### Reid Barton (Nov 19 2020 at 19:15):

I still think it's best to define nondegenerate with that name

#### Reid Barton (Nov 19 2020 at 19:15):

compare set.nonempty

#### Eric Wieser (Nov 19 2020 at 19:16):

Well, presumably docs#set.empty is taken by ∅

#### Reid Barton (Nov 19 2020 at 19:16):

It's just a historical accident that things like nondegenerate and nonempty have the non- prefix while things like injective don't

#### Eric Wieser (Nov 19 2020 at 19:16):

With an underscore to match pos_def?

#### Reid Barton (Nov 19 2020 at 19:17):

No, nondegenerate is one word, positive definite is two words

#### Eric Wieser (Nov 19 2020 at 19:17):

Oh, I assumed it was non-degenerate vs positive-definite

#### Reid Barton (Nov 19 2020 at 19:18):

Yeah, math English is weird :upside_down:

#### Eric Wieser (Nov 19 2020 at 19:18):

Wait, isn't my claim correct? The two random webpages I had open confirmed my spelling

#### Adam Topaz (Nov 19 2020 at 19:18):

Or is it non-nonwerid?

#### Adam Topaz (Nov 19 2020 at 19:19):

+1 for nondegenerate btw

#### Adam Topaz (Nov 19 2020 at 19:19):

Never in my life have I ever assumed explicitly that a quadratic form was degenerate!

#### Reid Barton (Nov 19 2020 at 19:19):

I think positive definite could have a hyphen but it would be weird in nondegenerate

#### Eric Wieser (Nov 19 2020 at 19:19):

Alright, will do that

#### Eric Wieser (Nov 19 2020 at 19:19):

I guess I should keep the lemma but in reverse?

#### Eric Wieser (Nov 19 2020 at 19:22):

/-- A non-degenerate quadratic form is zero only on zero vectors. -/
def nondegenerate (Q₂ : quadratic_form R₂ M₂) : Prop := ∀ x, Q₂ x = 0 → x = 0

lemma not_nondegenerate_iff (Q₂ : quadratic_form R₂ M₂) : ¬nondegenerate Q₂ ↔ ∃ x ≠ 0, Q₂ x = 0 :=
begin
unfold nondegenerate,
push_neg,
split,
{ rintros ⟨x, hqx, hx⟩, exact ⟨x, hx, hqx⟩, },
{ rintros ⟨x, hx, hqx⟩, exact ⟨x, hqx, hx⟩, },
end


#### Eric Wieser (Nov 19 2020 at 19:22):

Thanks for the push_neg tip.

#### Adam Topaz (Nov 19 2020 at 19:23):

(docstring is wrong)

#### Johan Commelin (Nov 19 2020 at 19:25):

Do you even need the split? Or will something like simp only [and_comm] close it after push_neg?

#### Adam Topaz (Nov 19 2020 at 19:26):

should nondegenerate be a class?

#### Eric Wieser (Nov 19 2020 at 19:27):

simp only [and_comm, exists_prop] does the trick

#### Eric Wieser (Nov 19 2020 at 19:29):

Since pos_def isn't, I'd say nondegenerate shouldn't be either

#5045

#### Eric Wieser (Nov 19 2020 at 19:35):

Proving that nondegenerate Q ↔ Q.discr ≠ 0 (given sufficient constraints for discr to exist) is an exercise left to the reviewer

#### Oliver Nash (Nov 20 2020 at 11:27):

Is this definitely the standard terminology?

Ignoring characteristic 2 for simplicity, I would refer to a quadratic form as non-degenerate when its associated bilinear form is non-degenerate.

E.g., I would say Q(x, y) = x² - y² is non-degenerate (in two dimensions) even though Q(1, 1) = 0.

#### Damiano Testa (Nov 20 2020 at 11:30):

I agree with @Oliver Nash. I would say that nondegenerate is the condition that the appropriate determinant does not vanish, while not having a non-trivial zero I would call anisotropic.

#### Eric Wieser (Nov 20 2020 at 11:37):

If I'm reading that correctly, is my claim nondegenerate Q ↔ Q.discr ≠ 0 untrue in the current definition?

Yes it's untrue.

Whoops

#### Eric Wieser (Nov 20 2020 at 11:44):

That's unfortunate, because my lemma that needed Q.nondegenerate is probably harder to prove than I thought also untrue for the case I had in mind

#### Kevin Buzzard (Nov 20 2020 at 11:50):

As Damiano says, the condition that $Q$ is nowhere-vanishing (except at zero) is called anisotropic and is far more subtle than being nondegenerate (for example it is not preserved if you change the base field: $x^2+y^2$ is anisotropic over $\mathbb{R}$ but not over $\mathbb{C}$).

#### Johan Commelin (Nov 20 2020 at 11:52):

My apologies for hitting the merge button too quickly :face_palm:

#### Johan Commelin (Nov 20 2020 at 11:56):

@Eric Wieser Are you working on a PR that updates the terminology? If not, then I will do it.

#5050

#### Eric Wieser (Nov 20 2020 at 12:06):

Is the definition I should have used ∀ x, (∀ y, polar Q x y = 0) → x = 0?

#### Kevin Buzzard (Nov 20 2020 at 12:18):

Is polar Q the associated bilinear form? There are subtleties in characteristic 2 which I am not really on top of, but away from char 2 if polar Q x y = Q (x + y) - Q x - Q y then what you posted is the definition of nondegenerate. In char 2, x^2 would be degenerate here because polar Q would be identically zero.

#### Kevin Buzzard (Nov 20 2020 at 12:21):

My (poor) understanding of char 2 is that there are two words for bilinear forms (perhaps alternating and antisymmetric?) which are the same in general but have distinct meanings in char 2 (one implies the other), and perhaps it's the case that people don't really study quadratic forms at all in char 2?

#### Eric Wieser (Nov 20 2020 at 12:46):

polar Q x y is what you say it is

#### Eric Wieser (Nov 20 2020 at 12:46):

Which is _not_ the associated bilinear form, but twice it

#### Damiano Testa (Nov 20 2020 at 13:42):

A statement that works regardless of the characteristic is that the quadratic form is nondegenerate iff the corresponding quadric is smooth. You can compute the singular locus using the jacobian criterion. In turn, this means that the determinant of the hessian matrix must be nonzero at all points where the quadratic form vanishes. In characteristic different from 2, it suffices to check non-vanishing of the determinant, thanks to Euler's identity. In characteristic 2, the extra condition is needed. However, it is all that needs to be checked. This can be further computed explicitly: let me know if there is any reason for wanting to do this explicitly!

#### Eric Wieser (Nov 20 2020 at 13:44):

That definition sounds like a lot more work than the one I give above...

#### Damiano Testa (Nov 20 2020 at 13:45):

it is simply requiring a polynomial not to vanish. I am not sure how hard it would be to implement this. If determinants are available, you can compute the formula using cramer's rule

#### Johan Commelin (Nov 20 2020 at 13:45):

@Damiano Testa What would you propose as Lean definition of quadratic_form.nondegenerate?

#### Johan Commelin (Nov 20 2020 at 13:45):

We have determinants and Cramer's rule

#### Eric Wieser (Nov 20 2020 at 13:46):

Not in characteristic 2 we don't, the conversion to matrix doesn't exist there

Aah, snap

#### Damiano Testa (Nov 20 2020 at 13:47):

Ok, so here is what is true mathematically: if the dimension of the kernel of the hessian is at least 2, the quadratic form is degenerate always. If the dimension of the kernel is at most one, then use cramer's rule to find a generator of the kernel, evaluate the quadratic form on this vector and check that you get a non-zero result

#### Damiano Testa (Nov 20 2020 at 13:47):

by hessian, i really mean the matrix of second derivatives. explicitly, with 0 along the diagonal...

#### Eric Wieser (Nov 20 2020 at 13:48):

Are you perhaps describing decidable Q.nondegenerate?

#### Damiano Testa (Nov 20 2020 at 13:49):

very likely what i described is decidable, or should at least assume classical!

#### Eric Wieser (Nov 20 2020 at 13:49):

What you have sounds like an algorithm for determining if Q is degenerate

#### Eric Wieser (Nov 20 2020 at 13:49):

And less like a definition of degeneracy

#### Damiano Testa (Nov 20 2020 at 13:50):

my definition is that the vanishing set in P^n is smooth. in turn, i can compute this via the method described

so, i guess that my definition would be via smoothness, but this seems less accessible in lean than computing determinants

#### Adam Topaz (Nov 20 2020 at 14:54):

Oops! I should have looked at the definitions more carefully yesterday :(

If you want a coordinate-free way to define nondegeneracy for a quadratic form, you can say that it's regular over every field extension of the base (it's enough to check it for an algebraic closure, but it's presumably easier to write down the definition with every field extension), where "regular" can be defined with a simple linear-algebraic condition in terms of the quadratic form and the associated polar form. But it seems that quadratic forms in mathlib are defined over arbitrary rings, not just fields, and I don't know what the correct definition is in general (without going into more complicated algebraic geometry).

#### Damiano Testa (Nov 20 2020 at 14:57):

Working over a field, you only need to check it over purely inseparable extensions of degree a power of 2: when the characteristic is different from 2, the singular locus has a point over the algebraic closure iff it has a point over the ground field.

#### Adam Topaz (Nov 20 2020 at 14:59):

Sure, I agree. But it feels unnatural to define something by saying "if the characteristic is 2, do this, and if not, then do that."

#### Adam Topaz (Nov 20 2020 at 15:00):

I think it makes more sense to give a uniform definition at the start, and prove a theorem later saying that if the characteristic is not 2, then you can use a simpler condition, and if it's 2, use another condition

#### Damiano Testa (Nov 20 2020 at 15:00):

Of course! Although the statement "check it over purely inseparable extensions of degree a power of 2" was my hack for not separating cases!

#### Adam Topaz (Nov 20 2020 at 15:00):

Ah I see :) The type of purely inseparable extensions of degree 2 can be empty :rofl:

#### Damiano Testa (Nov 20 2020 at 15:01):

rather than empty, just trivial!

#### Adam Topaz (Nov 20 2020 at 15:01):

Oh right, power of 2 :)

#### Damiano Testa (Nov 20 2020 at 15:01):

(sorry, the ones of degree 2 can be empty: the ones of degree a power of two always contains one element)

#### Adam Topaz (Nov 20 2020 at 15:03):

@Damiano Testa Do you know of a simple definition over an arbitrary ring? The only one I can think of is to work with the family of quadrics over spec of the base ring.

#### Adam Topaz (Nov 20 2020 at 15:03):

(And to be honest I've never actually seen such a definition in the literature)

#### Johan Commelin (Nov 20 2020 at 15:05):

Of course another option is that we can assume that the base ring is a field when defining quadratic_form.nondegenerate.

#### Reid Barton (Nov 20 2020 at 15:08):

or maybe an integral domain?

#### Adam Topaz (Nov 20 2020 at 15:08):

I don't think it works over an arbitrary domain, you can have bad reduction at some primes

#### Adam Topaz (Nov 20 2020 at 15:09):

Well... it depends on how you define it.

#### Reid Barton (Nov 20 2020 at 15:09):

OK, I don't really know what I'm talking about, but it seems awkward to exclude the case of $\mathbb{Z}$

#### Adam Topaz (Nov 20 2020 at 15:12):

Yeah, I agree it would be nice to have a definition that works (At least) over $\mathbf{Z}$

#### Damiano Testa (Nov 20 2020 at 15:14):

I think that as soon as you start wondering about quadratic forms over arbitrary rings, a little of language from algebraic geometry makes life much simpler. I would say that the "correct" generalization is to use smoothness of the morphism to the base ring/scheme. However, it is hard to find a quadratic form smooth over Z: the requirement becomes that the discriminant should be "almost 1" (you have some extra freedom coming from 2, of all places). For instance, xy=0 is smooth in two variables over Z and you get "for free" that xy-z^2=0 is also smooth over Z. You can construct further examples using E_8 in 8 or 9 dimensions, but integral, unimodular lattices are hard to come by.

#### Damiano Testa (Nov 20 2020 at 15:16):

it might be easier to say that a form over an integral domain is nondegenerate if it is so over the field of fractions and then think about revising this definition later on, once you really need to deduce properties of reductions modulo primes of the base ring

#### Adam Topaz (Nov 20 2020 at 15:17):

Damiano Testa said:

it might be easier to say that a form over an integral domain is nondegenerate if it is so over the field of fractions and then think about revising this definition later one, once you really need to deduce properties of reductions modulo primes of the base ring

This should be more appropriately called "generically nondegenerate"

#### Damiano Testa (Nov 20 2020 at 15:17):

I agree, but it might be helpful to save the "generically" until you also have a "specially" in the picture!

#### Damiano Testa (Nov 20 2020 at 15:19):

for instance, even thinking about the hasse-minkowski theorem, it may not be too useful to have the "special" point of view. certainly not for the statement, but possibly not even for the proof...

#### Adam Topaz (Nov 20 2020 at 15:19):

Wait.... I think the following is true: A quadratic form over a ring $A$ is nondegenerate (in the correct sense) if its base-change with respect to every morphism $A \to K$, where $K$ is a field, is nondegenerate (or just regular)

#### Damiano Testa (Nov 20 2020 at 15:21):

i vote for "nondegenerate" to mean "generically nondegenerate over an integral domain". once people really want to use quadratic forms over more general rings and really deal with reduction types, then they might want to start using different names, like smooth, conic/quadric bundle, brauer-severi variety,...

#### Damiano Testa (Nov 20 2020 at 15:23):

Wait.... I think the following is true: A quadratic form over a ring $A$ is nondegenerate (in the correct sense) if its base-change with respect to every morphism $A \to K$, where $K$ is a field, is nondegenerate (or just regular)

I believe that this can be proved using that smoothness is local on the base. you can get away with regularity, since you allow field extensions, and geometrically regular means smooth.

#### Johan Commelin (Nov 20 2020 at 15:28):

It would be good if someone could capture this fruitful dialogue in a lean file :grinning:

#### Adam Topaz (Nov 20 2020 at 15:28):

All this just tells me that we really need more algebraic geometry in mathlib

#### Johan Commelin (Nov 20 2020 at 15:28):

(And PR the result to mathlib)

#### Johan Commelin (Nov 20 2020 at 15:29):

But we can't really start doing more AG if we don't have the definition of a flat module... that's what has been stopping me

#### Damiano Testa (Nov 20 2020 at 15:29):

A more hands on approach to this issue is to compute the "universal determinant":

det (hessian matrix)

as a polynomial with integer coefficients. Note that there are lots of 2's along the diagonal. Remove the largest power of 2 that divides the polynomial above and define a form to be non-degenerate if this polynomial does not vanish when evaluated on the coefficients of the quadratic form. does this seem like a reasonable point of view?

#### Adam Topaz (Nov 20 2020 at 15:37):

Does mathlib even have base-change of vectorspaces w.r.t. field extensions?

#### Johan Commelin (Nov 20 2020 at 15:43):

Not yet, see the base change PR #4773

#### Adam Topaz (Nov 20 2020 at 16:05):

Well, modulo the missing stuff about base-change (and some pseudocode), here is what I propose as a definition:

import linear_algebra.quadratic_form
import linear_algebra

variables {K : Type*} [field K] {M : Type*} [add_comm_group M] [vector_space K M] (Q : quadratic_form K M)

def radical : submodule K M :=
{ carrier := {m | Q m = 0 ∧ (∀ n : M, (polar Q) m n = 0)},
zero_mem' := sorry,
smul_mem' := sorry }

-- nondegenerate Q := ∀ (L : field extensions of K), radical (base_change L Q) = ⊥


#### Adam Topaz (Nov 20 2020 at 16:06):

@Damiano Testa does this look right to you?

#### Adam Topaz (Nov 20 2020 at 16:09):

But when actually making this definition, we will need to quantify over all field extensions, and in particular over some types, so some universe annotations will be necessary as well..

#### Adam Topaz (Nov 20 2020 at 16:14):

Looks like the following is equivalent:

import linear_algebra.quadratic_form
import linear_algebra

variables {K : Type*} [field K] {M : Type*} [add_comm_group M] [vector_space K M] (Q : quadratic_form K M)

def radical : submodule K M :=
{ carrier := {m | Q m = 0 ∧ (∀ n : M, (polar Q) m n = 0)},
zero_mem' := sorry,
smul_mem' := sorry }

def polar_radical : submodule K M :=
{ carrier := {m | ∀ n, polar Q m n = 0},
zero_mem' := sorry,
smul_mem' := sorry }

def nondegenerate := (radical Q = ⊥) ∧ (vector_space.dim (polar_radical Q) ≤ 1)


#### Kevin Buzzard (Nov 20 2020 at 16:28):

Apparently quadratic forms in characteristic 2 deserve their own theory!

#### Adam Topaz (Nov 20 2020 at 16:30):

The equivalence with the second definition I mentioned above comes from a theorem in the book by Elman, Karpenko and Merkurjev. They do a lot with quadratic forms in arbitrary characteristic, whereas most texts tacitly assume characteristic not 2.

#### Damiano Testa (Nov 20 2020 at 16:35):

Damiano Testa does this look right to you?

If I understand this correctly, this means that you are requiring m to be a root of the quadratic form and in the kernel of the hessian matrix. I would call this a correct definition of nondegenerate , once you extend to all extensions (or, alternatively, all purely inseparable extensions of degree a power of 2).

#### Damiano Testa (Nov 20 2020 at 16:36):

(being in the kernel of the hessian matrix implies the vanishing of Q over fields of characteristic different from 2, by Euler's identity.)

#### Adam Topaz (Nov 20 2020 at 16:36):

I think with the second definition it's not required to extend the base.

#### Adam Topaz (Nov 20 2020 at 16:37):

See lemma 7.16 on page 43 here:
https://sites.ualberta.ca/~karpenko/publ/Kniga.pdf

#### Damiano Testa (Nov 20 2020 at 16:39):

See lemma 7.16 on page 43 here:
https://sites.ualberta.ca/~karpenko/publ/Kniga.pdf

I agree that this is indeed equivalent! This should be the argument with cramer's rule.

#### Adam Topaz (Nov 20 2020 at 16:41):

Alright, I should go back to writing notes for my class now :)

#### Damiano Testa (Nov 20 2020 at 16:45):

thank you for the formalization!

Last updated: May 12 2021 at 23:13 UTC