Zulip Chat Archive

Stream: maths

Topic: Construction of Algebraic Closure


view this post on Zulip Kenny Lau (May 29 2018 at 18:03):

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?

view this post on Zulip Johan Commelin (May 29 2018 at 18:06):

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

view this post on Zulip Kenny Lau (May 29 2018 at 18:06):

I don't

view this post on Zulip Johan Commelin (May 29 2018 at 18:06):

Ok, so how do you do addition and multiplication?

view this post on Zulip Kenny Lau (May 29 2018 at 18:06):

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

view this post on Zulip Kenny Lau (May 29 2018 at 18:07):

then just, you know, do the thing

view this post on Zulip Kenny Lau (May 29 2018 at 18:07):

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

view this post on Zulip Kenny Lau (May 29 2018 at 18:07):

no this doesn't work

view this post on Zulip Johan Commelin (May 29 2018 at 18:08):

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

view this post on Zulip Johan Commelin (May 29 2018 at 18:08):

So that makes me suspicious

view this post on Zulip Kenny Lau (May 29 2018 at 18:09):

do you need choice for the direct limit construction?

view this post on Zulip Johan Commelin (May 29 2018 at 18:12):

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

view this post on Zulip Johan Commelin (May 29 2018 at 18:15):

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

view this post on Zulip Kenny Lau (May 29 2018 at 18:15):

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

view this post on Zulip Kenny Lau (May 29 2018 at 18:15):

no, that doesn't

view this post on Zulip Kenny Lau (May 29 2018 at 18:15):

and how do you know about the project

view this post on Zulip Johan Commelin (May 29 2018 at 18:15):

Kevin mentioned somewhere that you were working on some algebraic stuff

view this post on Zulip Johan Commelin (May 29 2018 at 18:15):

for a project that he gave you

view this post on Zulip Johan Commelin (May 29 2018 at 18:16):

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

view this post on Zulip Johan Commelin (May 29 2018 at 18:16):

I haven't worked with Choice yet in Lean

view this post on Zulip Kenny Lau (May 29 2018 at 18:17):

nice

view this post on Zulip Johan Commelin (May 29 2018 at 18:17):

But we really need Galois theory

view this post on Zulip Kenny Lau (May 29 2018 at 18:17):

stop before you are corrupted by choice

view this post on Zulip Kenny Lau (May 29 2018 at 18:17):

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

view this post on Zulip Johan Commelin (May 29 2018 at 18:17):

Yes, I also reject infinity (-;

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:23):

Yes you can't do add this way Kenny

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:24):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:24):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:24):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:24):

and unfortunately this is not in general a field

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:25):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:25):

You order the roots of both of them

view this post on Zulip Mario Carneiro (May 29 2018 at 18:25):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:25):

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

view this post on Zulip Kenny Lau (May 29 2018 at 18:26):

but we all know that Q-bar is computable

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:26):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:26):

The problem is that whilst g is irreducible over Q

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:27):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:27):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 18:27):

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

view this post on Zulip Assia Mahboubi (May 29 2018 at 21:02):

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.

view this post on Zulip Kenny Lau (May 29 2018 at 21:03):

thanks

view this post on Zulip Assia Mahboubi (May 29 2018 at 21:04):

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.

view this post on Zulip Kenny Lau (May 29 2018 at 21:05):

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

view this post on Zulip Kenny Lau (May 29 2018 at 21:05):

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

view this post on Zulip Assia Mahboubi (May 29 2018 at 21:05):

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

view this post on Zulip Kenny Lau (May 29 2018 at 21:05):

then it should still be constructive in Lean

view this post on Zulip Mario Carneiro (May 29 2018 at 21:07):

There is a choice operator on countable types in lean

view this post on Zulip Mario Carneiro (May 29 2018 at 21:08):

encodable.choose in data.encodable

view this post on Zulip Patrick Massot (May 29 2018 at 21:08):

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

view this post on Zulip Assia Mahboubi (May 29 2018 at 21:09):

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

view this post on Zulip Mario Carneiro (May 29 2018 at 21:09):

The axiomatically basic one is nat.find

view this post on Zulip Assia Mahboubi (May 29 2018 at 21:15):

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.

view this post on Zulip Junyan Xu (Aug 15 2020 at 17:24):

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

view this post on Zulip Kenny Lau (Aug 15 2020 at 17:25):

h is not decidable

view this post on Zulip Junyan Xu (Aug 15 2020 at 17:34):

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.

view this post on Zulip Kenny Lau (Aug 15 2020 at 17:35):

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

view this post on Zulip Junyan Xu (Aug 15 2020 at 17:36):

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

view this post on Zulip Junyan Xu (Aug 15 2020 at 17:36):

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

view this post on Zulip Kenny Lau (Aug 15 2020 at 17:37):

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

view this post on Zulip Junyan Xu (Aug 15 2020 at 17:44):

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.

view this post on Zulip Junyan Xu (Aug 15 2020 at 17:48):

tuto_lib contains attribute [instance] classical.prop_decidable

view this post on Zulip Mario Carneiro (Aug 15 2020 at 17:53):

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

view this post on Zulip Mario Carneiro (Aug 15 2020 at 18:01):

lean#446

view this post on Zulip Mario Carneiro (Aug 15 2020 at 18:08):

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

view this post on Zulip Bryan Gin-ge Chen (Aug 15 2020 at 18:18):

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

view this post on Zulip Mario Carneiro (Aug 15 2020 at 18:22):

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

view this post on Zulip Mario Carneiro (Aug 15 2020 at 18:22):

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

view this post on Zulip Mario Carneiro (Aug 15 2020 at 18:23):

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

view this post on Zulip Bryan Gin-ge Chen (Aug 15 2020 at 18:24):

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

view this post on Zulip Mario Carneiro (Aug 15 2020 at 18:25):

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)

view this post on Zulip Mario Carneiro (Aug 15 2020 at 18:25):

but this means they can't keep the nolint

view this post on Zulip Bryan Gin-ge Chen (Aug 15 2020 at 18:26):

We can always add nolint in mathlib.

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

view this post on Zulip Mario Carneiro (Aug 15 2020 at 18:27):

that too

view this post on Zulip Mario Carneiro (Aug 15 2020 at 18:28):

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

view this post on Zulip Mario Carneiro (Aug 15 2020 at 18:28):

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

view this post on Zulip Junyan Xu (Aug 15 2020 at 18:40):

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.

view this post on Zulip Junyan Xu (Aug 15 2020 at 18:40):

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.

view this post on Zulip Mario Carneiro (Aug 15 2020 at 18:42):

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

view this post on Zulip Mario Carneiro (Aug 15 2020 at 18:43):

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

view this post on Zulip Mario Carneiro (Aug 15 2020 at 18:43):

and what is needed to make VM builtins work

view this post on Zulip Junyan Xu (Aug 17 2020 at 02:28):

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 mn, 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 _))

Last updated: May 11 2021 at 15:12 UTC