Zulip Chat Archive

Stream: new members

Topic: Defining degenerate quadratic forms


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

view this post on Zulip Johan Commelin (Nov 19 2020 at 19:10):

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

view this post on Zulip Reid Barton (Nov 19 2020 at 19:10):

push_neg should help somehow

view this post on Zulip Johan Commelin (Nov 19 2020 at 19:10):

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

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

view this post on Zulip Johan Commelin (Nov 19 2020 at 19:12):

Maybe we should call them smooth?

view this post on Zulip Johan Commelin (Nov 19 2020 at 19:12):

smooth = nonsingular = nondegenerate

view this post on Zulip Reid Barton (Nov 19 2020 at 19:12):

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

view this post on Zulip Eric Wieser (Nov 19 2020 at 19:12):

I can remove that iff

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

view this post on Zulip Reid Barton (Nov 19 2020 at 19:15):

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

view this post on Zulip Reid Barton (Nov 19 2020 at 19:15):

compare set.nonempty

view this post on Zulip Eric Wieser (Nov 19 2020 at 19:16):

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

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

view this post on Zulip Eric Wieser (Nov 19 2020 at 19:16):

With an underscore to match pos_def?

view this post on Zulip Reid Barton (Nov 19 2020 at 19:17):

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

view this post on Zulip Eric Wieser (Nov 19 2020 at 19:17):

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

view this post on Zulip Reid Barton (Nov 19 2020 at 19:18):

Yeah, math English is weird :upside_down:

view this post on Zulip Eric Wieser (Nov 19 2020 at 19:18):

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

view this post on Zulip Adam Topaz (Nov 19 2020 at 19:18):

Or is it non-nonwerid?

view this post on Zulip Adam Topaz (Nov 19 2020 at 19:19):

+1 for nondegenerate btw

view this post on Zulip Adam Topaz (Nov 19 2020 at 19:19):

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

view this post on Zulip Reid Barton (Nov 19 2020 at 19:19):

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

view this post on Zulip Eric Wieser (Nov 19 2020 at 19:19):

Alright, will do that

view this post on Zulip Eric Wieser (Nov 19 2020 at 19:19):

I guess I should keep the lemma but in reverse?

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

view this post on Zulip Eric Wieser (Nov 19 2020 at 19:22):

Thanks for the push_neg tip.

view this post on Zulip Adam Topaz (Nov 19 2020 at 19:23):

(docstring is wrong)

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

view this post on Zulip Adam Topaz (Nov 19 2020 at 19:26):

should nondegenerate be a class?

view this post on Zulip Eric Wieser (Nov 19 2020 at 19:27):

simp only [and_comm, exists_prop] does the trick

view this post on Zulip Eric Wieser (Nov 19 2020 at 19:29):

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

view this post on Zulip Eric Wieser (Nov 19 2020 at 19:34):

#5045

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

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

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

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

view this post on Zulip Kevin Buzzard (Nov 20 2020 at 11:37):

Yes it's untrue.

view this post on Zulip Eric Wieser (Nov 20 2020 at 11:37):

Whoops

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

view this post on Zulip Kevin Buzzard (Nov 20 2020 at 11:50):

As Damiano says, the condition that QQ 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: x2+y2x^2+y^2 is anisotropic over R\mathbb{R} but not over C\mathbb{C}).

view this post on Zulip Johan Commelin (Nov 20 2020 at 11:52):

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

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

view this post on Zulip Eric Wieser (Nov 20 2020 at 11:57):

Please go ahead

view this post on Zulip Johan Commelin (Nov 20 2020 at 12:02):

#5050

view this post on Zulip Eric Wieser (Nov 20 2020 at 12:06):

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

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

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

view this post on Zulip Eric Wieser (Nov 20 2020 at 12:46):

polar Q x y is what you say it is

view this post on Zulip Eric Wieser (Nov 20 2020 at 12:46):

Which is _not_ the associated bilinear form, but twice it

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

view this post on Zulip Eric Wieser (Nov 20 2020 at 13:44):

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

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

view this post on Zulip Johan Commelin (Nov 20 2020 at 13:45):

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

view this post on Zulip Johan Commelin (Nov 20 2020 at 13:45):

We have determinants and Cramer's rule

view this post on Zulip Eric Wieser (Nov 20 2020 at 13:46):

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

view this post on Zulip Johan Commelin (Nov 20 2020 at 13:46):

Aah, snap

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

view this post on Zulip Damiano Testa (Nov 20 2020 at 13:47):

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

view this post on Zulip Eric Wieser (Nov 20 2020 at 13:48):

Are you perhaps describing decidable Q.nondegenerate?

view this post on Zulip Damiano Testa (Nov 20 2020 at 13:49):

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

view this post on Zulip Eric Wieser (Nov 20 2020 at 13:49):

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

view this post on Zulip Eric Wieser (Nov 20 2020 at 13:49):

And less like a definition of degeneracy

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

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

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

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

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

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

view this post on Zulip Adam Topaz (Nov 20 2020 at 15:00):

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

view this post on Zulip Damiano Testa (Nov 20 2020 at 15:01):

rather than empty, just trivial!

view this post on Zulip Adam Topaz (Nov 20 2020 at 15:01):

Oh right, power of 2 :)

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

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

view this post on Zulip Adam Topaz (Nov 20 2020 at 15:03):

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

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

view this post on Zulip Reid Barton (Nov 20 2020 at 15:08):

or maybe an integral domain?

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

view this post on Zulip Adam Topaz (Nov 20 2020 at 15:09):

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

view this post on Zulip 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 Z\mathbb{Z}

view this post on Zulip Adam Topaz (Nov 20 2020 at 15:12):

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

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

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

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

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

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

view this post on Zulip Adam Topaz (Nov 20 2020 at 15:19):

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

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

view this post on Zulip Damiano Testa (Nov 20 2020 at 15:23):

Adam Topaz said:

Wait.... I think the following is true: A quadratic form over a ring AA is nondegenerate (in the correct sense) if its base-change with respect to every morphism AKA \to K, where KK 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.

view this post on Zulip Johan Commelin (Nov 20 2020 at 15:28):

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

view this post on Zulip Adam Topaz (Nov 20 2020 at 15:28):

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

view this post on Zulip Johan Commelin (Nov 20 2020 at 15:28):

(And PR the result to mathlib)

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

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

view this post on Zulip Adam Topaz (Nov 20 2020 at 15:37):

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

view this post on Zulip Johan Commelin (Nov 20 2020 at 15:43):

Not yet, see the base change PR #4773

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

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) = ⊥

view this post on Zulip Adam Topaz (Nov 20 2020 at 16:06):

@Damiano Testa does this look right to you?

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

view this post on Zulip Adam Topaz (Nov 20 2020 at 16:14):

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)

view this post on Zulip Kevin Buzzard (Nov 20 2020 at 16:28):

Apparently quadratic forms in characteristic 2 deserve their own theory!

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

view this post on Zulip Damiano Testa (Nov 20 2020 at 16:35):

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

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

view this post on Zulip Adam Topaz (Nov 20 2020 at 16:36):

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

view this post on Zulip Adam Topaz (Nov 20 2020 at 16:37):

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

view this post on Zulip Damiano Testa (Nov 20 2020 at 16:39):

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.

view this post on Zulip Adam Topaz (Nov 20 2020 at 16:41):

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

view this post on Zulip Damiano Testa (Nov 20 2020 at 16:45):

thank you for the formalization!


Last updated: May 12 2021 at 23:13 UTC