Defining degenerate quadratic forms

Stream: new members

[Eric Wieser]

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,
    rw quadratic_form.map_zero,
  },
  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]

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

[Reid Barton]

push_neg should help somehow

[Johan Commelin]

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

[Eric Wieser]

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

[Johan Commelin]

Maybe we should call them smooth?

[Johan Commelin]

smooth = nonsingular = nondegenerate

[Reid Barton]

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

[Eric Wieser]

I can remove that iff

[Eric Wieser]

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

[Reid Barton]

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

[Reid Barton]

compare set.nonempty

[Eric Wieser]

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

[Reid Barton]

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

[Eric Wieser]

With an underscore to match pos_def?

[Reid Barton]

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

[Eric Wieser]

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

[Reid Barton]

Yeah, math English is weird :upside_down:

[Eric Wieser]

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

[Adam Topaz]

Or is it non-nonwerid?

[Adam Topaz]

+1 for nondegenerate btw

[Adam Topaz]

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

[Reid Barton]

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

[Eric Wieser]

Alright, will do that

[Eric Wieser]

I guess I should keep the lemma but in reverse?

[Eric Wieser]

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

Thanks for the push_neg tip.

[Adam Topaz]

(docstring is wrong)

[Johan Commelin]

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

[Adam Topaz]

should nondegenerate be a class?

[Eric Wieser]

simp only [and_comm, exists_prop] does the trick

[Eric Wieser]

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

[Eric Wieser]

#5045

[Eric Wieser]

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

[Oliver Nash]

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]

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]

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

[Kevin Buzzard]

Yes it's untrue.

[Eric Wieser]

Whoops

[Eric Wieser]

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]

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]

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

[Johan Commelin]

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

[Eric Wieser]

Please go ahead

[Johan Commelin]

#5050

[Eric Wieser]

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

[Kevin Buzzard]

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]

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]

polar Q x y is what you say it is

[Eric Wieser]

Which is _not_ the associated bilinear form, but twice it

[Damiano Testa]

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]

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

[Damiano Testa]

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]

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

[Johan Commelin]

We have determinants and Cramer's rule

[Eric Wieser]

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

[Johan Commelin]

Aah, snap

[Damiano Testa]

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]

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

[Eric Wieser]

Are you perhaps describing decidable Q.nondegenerate?

[Damiano Testa]

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

[Eric Wieser]

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

[Eric Wieser]

And less like a definition of degeneracy

[Damiano Testa]

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]

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]

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]

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]

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]

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]

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

[Damiano Testa]

rather than empty, just trivial!

[Adam Topaz]

Oh right, power of 2 :)

[Damiano Testa]

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

[Adam Topaz]

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

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

[Johan Commelin]

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

[Reid Barton]

or maybe an integral domain?

[Adam Topaz]

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

[Adam Topaz]

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

[Reid Barton]

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

[Adam Topaz]

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

[Damiano Testa]

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]

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]

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]

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

[Damiano Testa]

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]

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]

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]

Adam Topaz said:

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]

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

[Adam Topaz]

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

[Johan Commelin]

(And PR the result to mathlib)

[Johan Commelin]

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]

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]

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

[Johan Commelin]

Not yet, see the base change PR #4773

[Adam Topaz]

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

open quadratic_form

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,
  add_mem' := sorry,
  smul_mem' := sorry }

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

[Adam Topaz]

@Damiano Testa does this look right to you?

[Adam Topaz]

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]

Looks like the following is equivalent:

import linear_algebra.quadratic_form
import linear_algebra

open quadratic_form

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,
  add_mem' := sorry,
  smul_mem' := sorry }

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

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

[Kevin Buzzard]

Apparently quadratic forms in characteristic 2 deserve their own theory!

[Adam Topaz]

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]

Adam Topaz said:

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]

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

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

[Adam Topaz]

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

[Damiano Testa]

Adam Topaz said:

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]

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

[Damiano Testa]

thank you for the formalization!