## 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?

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)

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

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.

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

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?

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 ∀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 _))


Last updated: May 11 2021 at 15:12 UTC