C1 fields?

Stream: maths

[George McNinch]

Is the notion of a $(C_1)$ field in Mathlib? I looked but didn't spot it (though I've overlooked other things!!)

I believe the defn should read something like:

def IsC1 (k : Type) [Field k] : Prop :=
  ∀ (n : ℕ),
  ∀ f : MvPolynomial (Fin n) k,
  ∀ {d : ℕ},
  MvPolynomial.IsHomogeneous f d → d < n →
  ∃ v  : Fin n → k, f.eval v = 0 ∧ v ≠ 0

(see e.g. [Serre, "Galois Cohomology", II.3.2]) though of course I'm interested in phrasing suggestions... (assuming it isn't already available!) E.g. is it better to use Fintypes instead of Fin n for the MvPolynomials?

[Yaël Dillies]

George McNinch said:

is it better to use Fintypes instead of Fin n for the MvPolynomials?

It's (probably) better to use Fin n in the definition, and subsequently prove that this implies the arbitrary fintype version

[Yaël Dillies]

Btw I am pretty sure we do not have C1 fields, looks like a good contribution to mathlib :wink:

[George McNinch]

It's (probably) better to use Fin n in the definition, and subsequently prove that this implies the arbitrary fintype version

Aha - that definitely makes sense; thanks!

[Scott Carnahan]

Perhaps defining Cr for general r would be potentially helpful.

[Junyan Xu]

A possible reference is chapter 27 of Lorenz's Algebra II: https://link.springer.com/chapter/10.1007/978-0-387-72488-1_8
image.png

[George McNinch]

Junyan Xu said:

A possible reference is chapter 27 of Lorenz's Algebra II

Right; thanks.

I think the largest question is "what should be included". Here is a surely-too-long list of results about C1 that would be nice to have formalized.

First, results about "which fields are C1":

• algebraically closed fields are C1 (!)
• finite extension of C1 fields are C1
• finite fields are C1 ("Chevalley-Warning")
• the field of rational functions k(T) is C1 when k is alg. closed ("Tsen's Theorem")
• If $K_{nr}$ is "the" maximal unramified extension of a field $K$ which is complete under a discrete valuation with perfect residue field, then $K_{nr}$ is C1 (a result of Lang).

I know monograph/text-book references for the first 4. The only references I know for the fifth are Lang's original paper, and a Bourbaki seminar report (Jaffard 1954). I haven't actually read the proof. So probably this fifth point is just aspirational for now.
I'm also not sure whether this fifth point is one of those results where one can get away with "Henselian" rather than requiring "complete".

Second, applications of C1 should (?!) include:

• any Central Simple Algebra over a C1 field K is split (i.e. is isomorphic as $K$-algebra to $\operatorname{Mat}_n(K)$ for some n : PNat)
• a quadratic form on a vector space of dimension $\ge 3$ over a C1 field $K$ is isotropic

I worry (?) a bit about the first one because (as far as I can tell) the "reduced norm" for a CSA isn't really developed yet. So that'll need to be done first.

And all this so far avoids mention of Galois cohomology, where one should really prove

• if K is C1, then K has cohomological dimension <=1.

(This last bit sounds very complicated as a formalization task to me, so I'm just writing it down here to glare at...)

[George McNinch]

George McNinch said:

I believe the defn should read something like:

def IsC1 (k : Type) [Field k] : Prop :=
  ∀ (n : ℕ),
  ∀ f : MvPolynomial (Fin n) k,
  ∀ {d : ℕ},
  MvPolynomial.IsHomogeneous f d → d < n →
  ∃ v  : Fin n → k, f.eval v = 0 ∧ v ≠ 0

So, I'd be happier to not "fix a basis" in giving this definition -- i.e. I believe I'd rather work with forms found in SymmetricAlgebra k V. Something like:

def IsCr (r : ℕ) : Prop :=
  ∀ (n : ℕ),
  ∀ (V:Type), [AddCommGroup V] → [Module k V] → [FiniteDimensional k V]
      → Module.finRank k V = n →
  ∀ f : SymmetricAlgebra k V,
  ∀ {d : ℕ},
  SymmetricAlgebra.IsHomogeneous f d → d^r < n →
  ∃ v  : Fin n → k, f.eval v = 0 ∧ v ≠ 0

But it looks like there is currently no grading on SymmetricAlgebra k V -- i.e.
SymmetricAlgebra.IsHomogeneous f d. Isn't defined yet.

I think (?) I saw a recent thread about more-or-less exactly this (i.e. grading on SymmetricAlgebera). Is someone working on this? Is there some reason to avoid this point-of-view?

(added: really, I guess I'd be happiest working with forms in what I'd write on the blackboard as $k[V]$ by which I mean the synmmetric algebra of the dual of V -- i.e. on V→ₗ[k] k.)

(added, again): Arguably my suggested redefinition goes against the spirit of the advice of @Yaël Dillies, here, so maybe I'm mistaken about changing the definition. It just seems to me that the main things to which one wants to apply the C1 condition are typically given as "forms on vector spaces" (quadratic forms, reduced norms,...) and converting them to MvPolynomials to apply the condition seems clumsy (?).

But at any rate, the question about homogeneous elements of SymmetricAlgebra seems significant whichever way the definition is given.

[Johan Commelin]

Great list of tasks/ideas! Would you mind revording these in a github issue on the mathlib4 repo? Because this zulip thread will be much harder to find + update compated to a checklist on github.

[Johan Commelin]

I also wanted the symmetric algebra for some work in Lie theory, but ended up working with mvpoly.

[Scott Carnahan]

As far as I know the question of existence of a C_{3/2} field that is not C_1 is open, but perhaps we should allow fractional values of r.

[Yaël Dillies]

George McNinch said:

the main things to which one wants to apply the C1 condition are typically given as "forms on vector spaces" (quadratic forms, reduced norms,...) and converting them to MvPolynomials to apply the condition seems clumsy (?).

The point is that ∀ (V:Type), [AddCommGroup V] → [Module k V] → [FiniteDimensional k V], ... doesn't mean "for all finite-dimensional k-vector space V, ..." but "for all small finite-dimensional k-vector space V, ...". As it happens, all finite-dimensional k-vector space V are small, but that's something you can prove rather than something that comes out of the definition

[Yaël Dillies]

@Eric Wieser is the canonical person to ask about grading

[Kevin Buzzard]

@Kenny Lau were you thinking about grading on symmetric algebra?

[Kenny Lau]

@George McNinch the grading on symmetric algebra will come via either of the two pathways:

1. define symmetric tensor power (#26192), and then map each to the symmetric algebra
2. define homogeneous relation (#27307), and show that the relation that is the kernel of TensorAlgebra -> SymmetricAlgebra is homogeneous

[Damiano Testa]

Btw, a book that I really liked about these topics is Lectures on forms in many variables by Marvin Greenberg.

I read it well before being interested in formalization, but, at the time, I thought that it was great.

[George McNinch]

Scott Carnahan said:

As far as I know the question of existence of a C_{3/2} field that is not C_1 is open, but perhaps we should allow fractional values of r.

So perhaps something like this (?):

def IsCr' (r : {q :ℚ // q≥0 }) : Prop :=
  ∀ (n : ℕ),
  ∀ f : MvPolynomial (Fin n) k,
  ∀ {d : ℕ},
  MvPolynomial.IsHomogeneous f d → (d:ℝ) ^ (r:ℝ) < (n:ℝ) →
  ∃ v  : Fin n → k, f.eval v = 0 ∧ v ≠ 0

(Or is there a smoother way to say "non-negative rational"?)

[George McNinch]

Johan Commelin said:

Would you mind revording these in a github issue on the mathlib4 repo? Because this zulip thread will be much harder to find + update compated to a checklist on github.

I will do that (later today I hope). Seems like a good suggestion.

[George McNinch]

Yaël Dillies said:

The point is that ∀ (V:Type), [AddCommGroup V] → [Module k V] → [FiniteDimensional k V], ... doesn't mean "for all finite-dimensional k-vector space V, ..." but "for all small finite-dimensional k-vector space V, ...". As it happens, all finite-dimensional k-vector space V are small, but that's something you can prove rather than something that comes out of the definition

I see - by "small" one means something like "in a fixed universe"?

(I see that I haven't been careful to write e.g. (V : Type u)...)

[Kenny Lau]

yes, that's what small means

[Kenny Lau]

I haven't read all of the context, but if you're quantifying over "all fg modules" or something like that then you need to be careful about universes

[Kenny Lau]

typically the constructor will quantify over Type u (same universe), and then there will be a theorem afterwards proving the same theorem for all Type v (different universe)

[George McNinch]

Kenny Lau said:

George McNinch the grading on symmetric algebra will come via either of the two pathways:

1. define symmetric tensor power (#26192), and then map each to the symmetric algebra
2. define homogeneous relation (#27307), and show that the relation that is the kernel of TensorAlgebra -> SymmetricAlgebra is homogeneous

RIght - that was the sense that I remember from the earlier thread.
I feel like 2. is important. More generally there should be a notion of "homogeneous relation" on "graded rings" for which the quotient is also "graded" and I don't quite see how to get that from the approach in 1.

Which is not to diminish the importance of 1...

I'm realizing I haven't looked at what is done for the exterior algebra, and that I should look more
carefully at the PRs you indicate.

[George McNinch]

George McNinch said:

Johan Commelin said:

Would you mind revording these in a github issue on the mathlib4 repo? Because this zulip thread will be much harder to find + update compated to a checklist on github.

I will do that (later today I hope). Seems like a good suggestion.

Finally got this done. # C_r fields #28320

(Hopefully I got the tone OK...)

[Bhavik Mehta]

Yaël Dillies said:

George McNinch said:

is it better to use Fintypes instead of Fin n for the MvPolynomials?

It's (probably) better to use Fin n in the definition, and subsequently prove that this implies the arbitrary fintype version

I agree with this entirely, but to add some more detail: It's often much more convenient to index everything in terms of Fintypes rather than Fin n, since Fin n comes with an additional ordering which is usually not relevant (eg in your context), all that matters is that it's indexed by some finite structure, and {1,...,n} is convenient informal shorthand for this. But there are exceptions, notably:

• if the Fin n structure actually is relevant (eg if you'll later do arithmetic with the indices), then you can't nicely use Fintype
• if you are quantifying over types, since this can introduce universe weirdness
  In your situation, the second exception applies, and Yaël's comment about the subsequent proof restores the Fintype version, so you get the benefits of that too

[Kenny Lau]

one benefit of Fin n as we were just discussing at #mathlib4 > Tactic for polynomial/algebra is that you can write notation name_poly_vars R[x,y,z] so that you can use x, y, and z to refer to the indeterminates