Construction of Algebraic Closure

Stream: maths

[Kenny Lau]

I saw many constructions of the algebraic closure of a field k using direct limit, but I have a different construction in mind:
The set k-bar is { (f,n) in k[X] x N | f is irreducible and n < deg f }. The n represents the n-th root of the polynomial.
Addition and multiplicatoin can be defined using resultant.
Is this construction valid? Would this be a better construction?

[Johan Commelin]

Hmm, maybe I'm being silly. But how do you order the roots?

[Kenny Lau]

I don't

[Johan Commelin]

Ok, so how do you do addition and multiplication?

[Kenny Lau]

For f and g, I use resultant to construct h that contains all the roots

[Kenny Lau]

then just, you know, do the thing

[Kenny Lau]

if f has deg m and g has deg n, then h has deg mn

[Kenny Lau]

no this doesn't work

[Johan Commelin]

I mean, your approach looks very constructive. But we know that you need choice for k-bar

[Johan Commelin]

So that makes me suspicious

[Kenny Lau]

do you need choice for the direct limit construction?

[Johan Commelin]

Yes, you want to use Zorn to pick a maximal element

[Johan Commelin]

Does this mean you are going to refuse the project that Kevin gave you?

[Kenny Lau]

I think the problem is when I add 1+sqrt(2) and -sqrt(2)

[Kenny Lau]

no, that doesn't

[Kenny Lau]

and how do you know about the project

[Johan Commelin]

Kevin mentioned somewhere that you were working on some algebraic stuff

[Johan Commelin]

for a project that he gave you

[Johan Commelin]

Anyway, I think it is very cool. I have been thinking about Galois theory. But I was daunted by defining the algebraic closure.

[Johan Commelin]

I haven't worked with Choice yet in Lean

[Kenny Lau]

nice

[Johan Commelin]

But we really need Galois theory

[Kenny Lau]

stop before you are corrupted by choice

[Kenny Lau]

I mean, your approach looks very constructive. But we know that you need choice for k-bar

we all know that you don't need choice for F_p-bar or Q-bar or R-bar

[Johan Commelin]

Yes, I also reject infinity (-;

[Kevin Buzzard]

Yes you can't do add this way Kenny

[Kevin Buzzard]

The problem is that what you are doing in your head, is this:

[Kevin Buzzard]

if you have have two polynomials f(X) and g(X), irreducible in k[X] say

[Kevin Buzzard]

then you are doing mathematics in the ring k[X]/(f) tensor_k k[X]/(g)

[Kevin Buzzard]

and unfortunately this is not in general a field

[Kevin Buzzard]

Consider the polynomials f(X)=X^3-2 and g(X)=(X+1)^3-2. Both are irredudible over Q

[Kevin Buzzard]

You order the roots of both of them

[Mario Carneiro]

If you do this construction, I would like to have a computable algebraic numbers construction from it

[Kevin Buzzard]

but who is to say that if a,b,c was the first order then a-1,b-1,c-1 was the second one

[Kenny Lau]

but we all know that Q-bar is computable

[Kevin Buzzard]

so who can possibly tell when (root 1 of f) - (root 1 of g) is 1 or not?

[Kevin Buzzard]

The problem is that whilst g is irreducible over Q

[Kevin Buzzard]

it is not irreducible over the larger field Q[X]/(f)

[Kevin Buzzard]

indeed, it factors into a linear and an irreducible quadric over this larger field

[Kevin Buzzard]

so now all of a sudden the roots are not as indistinguishable as they used to be

[Assia Mahboubi]

Hi @Kenny Lau here is a formalized construction of the algebraic closure of countable fields. It heavily relies on this, the existence of an algebraically closed field with an automorphism of order 2. Here is an abstract construction of algebraic numbers. I can help deciphering the statements and proofs if you're interested. But several of these files have long headers describing what's done in them.

[Kenny Lau]

thanks

[Assia Mahboubi]

And all this is constructive. It only relies on the fact that there is choice operator on countable types with a decidable equality. This is provable in Coq without extra axioms, but using a subtle singleton elimination argument. I do not know if the same holds in Lean.

[Kenny Lau]

we don't have the axiom of unique choice in Lean, if that's what you mean

[Kenny Lau]

I suppose we can look at the preimage under the bijection from N and find the minimum element

[Assia Mahboubi]

No this is not what I mean, unique choice does not hold in Coq either.

[Kenny Lau]

then it should still be constructive in Lean

[Mario Carneiro]

There is a choice operator on countable types in lean

[Mario Carneiro]

encodable.choose in data.encodable

[Patrick Massot]

Noooo! Assia, please don't encourage Kenny in his constructive deviance

[Assia Mahboubi]

Ah thanks @Mario Carneiro, I was trying to dig into Lean to see if I could find it.

[Mario Carneiro]

The axiomatically basic one is nat.find

[Assia Mahboubi]

Hi again @Patrick Massot! Don't worry, I am just saying that for countable fields, classical proofs are constructive, in fact. I don't think that constructivism is the difficult issue here but I may well have forgotten how easy classical life is.

[Junyan Xu]

Mario Carneiro said:

The axiomatically basic one is nat.find

What do you mean by axiomatically basic? #print axioms nat.find shows classical.choice quot.sound and propext, so essentially all the axioms.
In ZF set theory it doesn't require any choice. I wonder if adding the axiom of unique choice makes Lean suitable for formalizing implications between different forms of choice in set theory, like dependent choice or ultrafilter lemma.
The use of choice seems to make nat.find noncomputable, which is confusing as it's just the mu-operator (as in mu-recursive functions, even with a termination guarantee). Is Lean using a stronger notion of computability somewhere between primitive recursive and recursive? To be clear, nat.find itself isn't labeled noncomputable, but the following code

def bld_extr (p : ℕ → ℕ → Prop)
  (h : ∀ m N, ∃ n ≥ N, p m n) : ℕ → ℕ
  -- build a extraction (indices for increasing subsequence) satisfying condition p
  | 0 := nat.find (h 0 0)
  | (m+1) := nat.find (h (m+1) (bld_extr m + 1))

yields the message

equation compiler failed to generate bytecode for 'bld_extr._main'
nested exception message:
code generation failed, VM does not have code for 'classical.choice'

which disappears when I add the noncomputable prefix.

However, the code def f := nat.find (by use 0; trivial : ∃n:ℕ, n=n) yields a different message definition 'f' is noncomputable, it depends on 'classical.prop_decidable'.

[Kenny Lau]

h is not decidable

[Junyan Xu]

The first message points to choice as a problem, while the second message is strange:
def nat.​find {p : ℕ → Prop} [decidable_pred p] : (∃ (n : ℕ), p n) → ℕ only requires p to be decidable. In this case, p is n=n, which Lean should know/be able to infer is decidable.

[Kenny Lau]

no, p is ∃ n ≥ 0, p 0 n

[Junyan Xu]

The second example is def f := nat.find (by use 0; trivial : ∃n:ℕ, n=n)

[Junyan Xu]

you can replace it with def f := nat.find (by use 0 : ∃n:ℕ, true) and get the same message

[Kenny Lau]

if you have open_locale classical then the decidable instance is by default the classical one

[Junyan Xu]

Good point! I was working in a file in the tutorial exercises and tuto_lib was imported. I switched to an empty file and def f := nat.find (⟨0,true.intro⟩ : ∃n:ℕ, true) and no error message appears.

[Junyan Xu]

tuto_lib contains attribute [instance] classical.prop_decidable

[Mario Carneiro]

What do you mean by axiomatically basic? #print axioms nat.find shows classical.choice quot.sound and propext, so essentially all the axioms.

What? That should not be, nat.find should require no axioms

[Mario Carneiro]

lean#446

[Mario Carneiro]

What the hell? I just noticed that the section https://github.com/leanprover-community/mathlib/blob/55d430ca22bad157799afdf5e3d9a26597ee37f9/src/algebra/order.lean#L125-L180 of choiceless proofs about decidable linear orders was completely destroyed by the decidable classical linter

[Bryan Gin-ge Chen]

Looks like the discussion was in this thread: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.232332/near/193211152

[Mario Carneiro]

Yes, I didn't realize that they actually went forward with the theorem defacement. In any case I've restored the theorems in #3799

[Mario Carneiro]

They have been marked @[nolint classical_decidable] this time, so hopefully this won't happen again

[Mario Carneiro]

If we decide these don't deserve to exist in mathlib, then they should be deleted, not trivialized

[Bryan Gin-ge Chen]

It'd be good to add a library note or some other documentation about the decidable namespace too.

[Mario Carneiro]

I was actually thinking of moving these theorems to core so that they can support things like lean#446 (which was the original reason I wrote them)

[Mario Carneiro]

but this means they can't keep the nolint

[Bryan Gin-ge Chen]

We can always add nolint in mathlib.

I thought we were planning to move order-stuff out of core rather than into it though?

[Mario Carneiro]

that too

[Mario Carneiro]

I would like the proof that int is a ring to not use the axiom of choice. If all the lemmas come out of core then these can come with

[Mario Carneiro]

Like does init.data.nat.lemmas need to exist?

[Junyan Xu]

I think the three axioms are not so bad as a single invocation of classical.em in the proof will make the theorem depend on all three, because of how classical.em is proved. Would be nice to have a command that tells whether a proof uses only excluded middle and not choice (as is the case for most of the incidence geometry problems). Maybe designate certain important theorems from where you don't trace further back.

[Junyan Xu]

I think core.init.data.nat.lemmas contains many useful lemmas. It's the go-to place when I can't find what I need in data.nat.basic.

[Mario Carneiro]

Of course the contents of init.data.nat.lemmas are important, I'm not saying to delete them! I mean to move everything to mathlib

[Mario Carneiro]

the question is really what is the minimal substrate that lean needs to pass its test suite

[Mario Carneiro]

and what is needed to make VM builtins work

[Junyan Xu]

I studied the proof of nat.find to convince myself it works and to learn the terse proof style, and I just came up with a different, shorter proof. Unfortuantely it uses nat.decreasing_induction which is not in the core, but it doesn't use addition. Let me know if it is worth PRing or can be further simplified.

parameter {p : ℕ → Prop}
variables [decidable_pred p] (H : ∃n, p n)
private def lbp (m n : ℕ) : Prop := m = n + 1 ∧ ¬p n
protected def find_x : {n // p n ∧ ∀m < n, ¬p m} :=
@well_founded.fix_F _ lbp (λk, (∀n<k, ¬p n) → {n // p n ∧ ∀m<n, ¬p m})
  (λk h al, if pk: p k then ⟨k,pk,al⟩ else h (k+1) ⟨rfl,pk⟩
    (λn pn, (lt_or_eq_of_le (nat.le_of_lt_succ pn)).elim
      (λh, al n h) (λh, by rwa h))) 0
  (let ⟨n,pn⟩ := H in suffices ∀m≤n, acc lbp m, from this 0 n.zero_le,
    λ_ hm, nat.decreasing_induction
      (λ_ hn, ⟨_, λ_ hy, by rwa hy.1⟩) hm ⟨_, λ_ hy, absurd pn hy.2⟩)
  (λ_ h, absurd h (nat.not_lt_zero _))