Zulip Chat Archive

Stream: maths

Topic: Construction of Algebraic Closure


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?

Johan Commelin (May 29 2018 at 18:06):

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

Kenny Lau (May 29 2018 at 18:06):

I don't

Johan Commelin (May 29 2018 at 18:06):

Ok, so how do you do addition and multiplication?

Kenny Lau (May 29 2018 at 18:06):

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

Kenny Lau (May 29 2018 at 18:07):

then just, you know, do the thing

Kenny Lau (May 29 2018 at 18:07):

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

Kenny Lau (May 29 2018 at 18:07):

no this doesn't work

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

Johan Commelin (May 29 2018 at 18:08):

So that makes me suspicious

Kenny Lau (May 29 2018 at 18:09):

do you need choice for the direct limit construction?

Johan Commelin (May 29 2018 at 18:12):

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

Johan Commelin (May 29 2018 at 18:15):

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

Kenny Lau (May 29 2018 at 18:15):

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

Kenny Lau (May 29 2018 at 18:15):

no, that doesn't

Kenny Lau (May 29 2018 at 18:15):

and how do you know about the project

Johan Commelin (May 29 2018 at 18:15):

Kevin mentioned somewhere that you were working on some algebraic stuff

Johan Commelin (May 29 2018 at 18:15):

for a project that he gave you

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.

Johan Commelin (May 29 2018 at 18:16):

I haven't worked with Choice yet in Lean

Kenny Lau (May 29 2018 at 18:17):

nice

Johan Commelin (May 29 2018 at 18:17):

But we really need Galois theory

Kenny Lau (May 29 2018 at 18:17):

stop before you are corrupted by choice

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

Johan Commelin (May 29 2018 at 18:17):

Yes, I also reject infinity (-;

Kevin Buzzard (May 29 2018 at 18:23):

Yes you can't do add this way Kenny

Kevin Buzzard (May 29 2018 at 18:24):

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

Kevin Buzzard (May 29 2018 at 18:24):

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

Kevin Buzzard (May 29 2018 at 18:24):

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

Kevin Buzzard (May 29 2018 at 18:24):

and unfortunately this is not in general a field

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

Kevin Buzzard (May 29 2018 at 18:25):

You order the roots of both of them

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

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

Kenny Lau (May 29 2018 at 18:26):

but we all know that Q-bar is computable

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?

Kevin Buzzard (May 29 2018 at 18:26):

The problem is that whilst g is irreducible over Q

Kevin Buzzard (May 29 2018 at 18:27):

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

Kevin Buzzard (May 29 2018 at 18:27):

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

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

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.

Kenny Lau (May 29 2018 at 21:03):

thanks

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.

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

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

Assia Mahboubi (May 29 2018 at 21:05):

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

Kenny Lau (May 29 2018 at 21:05):

then it should still be constructive in Lean

Mario Carneiro (May 29 2018 at 21:07):

There is a choice operator on countable types in lean

Mario Carneiro (May 29 2018 at 21:08):

encodable.choose in data.encodable

Patrick Massot (May 29 2018 at 21:08):

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

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.

Mario Carneiro (May 29 2018 at 21:09):

The axiomatically basic one is nat.find

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.

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

Kenny Lau (Aug 15 2020 at 17:25):

h is not decidable

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.

Kenny Lau (Aug 15 2020 at 17:35):

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

Junyan Xu (Aug 15 2020 at 17:36):

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

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

Kenny Lau (Aug 15 2020 at 17:37):

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

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.

Junyan Xu (Aug 15 2020 at 17:48):

tuto_lib contains attribute [instance] classical.prop_decidable

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

Mario Carneiro (Aug 15 2020 at 18:01):

lean#446

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

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

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

Mario Carneiro (Aug 15 2020 at 18:22):

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

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

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.

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)

Mario Carneiro (Aug 15 2020 at 18:25):

but this means they can't keep the nolint

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?

Mario Carneiro (Aug 15 2020 at 18:27):

that too

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

Mario Carneiro (Aug 15 2020 at 18:28):

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

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.

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.

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

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

Mario Carneiro (Aug 15 2020 at 18:43):

and what is needed to make VM builtins work

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: Dec 20 2023 at 11:08 UTC