# Zulip Chat Archive

## Stream: maths

### Topic: algebraic closure construction

#### Chris Hughes (Jan 23 2019 at 20:27):

So I'm trying out Tom Hales' construction of algebraic closure. The argument is to use zorn on this type ordered by subset, such that the inclusion map is a field hom.

def extensions : set (Σ s : set (big_type K), discrete_field s) := {s | ∃ h : set.range (embedding K) ⊆ s.1, by letI := s.2; exact is_field_hom (inclusion h) ∧ ∀ x : s.1, in_algebraic_closure _ (inclusion h) x}

This involves putting a field structure on the Union of a chain within this type. This is very messy. All the operations are noncomputable, and to prove `add_assoc`

, I end up with four different definitions of addition, with a tactic state like this.

K : Type u, c : set ↥(extensions K), hc : chain (λ (m a : ↥(extensions K)), m ≤ a) c, x y z : ↥⋃ (s : ↥c), ((s.val).val).fst ⊢ (⟨↑z, _⟩ + ⟨(⟨↑x, _⟩ + ⟨↑y, _⟩).val, _⟩).val = (⟨↑x, _⟩ + ⟨(⟨↑y, _⟩ + ⟨↑z, _⟩).val, _⟩).val

Is there a nicer approach?

#### Johannes Hölzl (Jan 23 2019 at 21:26):

Just to understand how you need to continue: since `hc`

tells you that `c`

forms a chain it is enough to select a maximal element and know that `x`

, `y`

, or `z`

are all in this maximal field.

#### Chris Hughes (Jan 23 2019 at 21:27):

Yes, but that's quite a messy argument.

#### Johannes Hölzl (Jan 23 2019 at 21:27):

it is

#### Kenny Lau (Jan 23 2019 at 21:28):

I just realized today that Artin's construction does not require splitting fields.

#### Kevin Buzzard (Jan 23 2019 at 21:29):

Wasn't I telling you this last Thursday?

#### Kenny Lau (Jan 23 2019 at 21:29):

maybe I wasn't listening :P

#### Kevin Buzzard (Jan 23 2019 at 21:29):

I think you convinced me it did, and then I tried to convince Neil in Amsterdam and he convinced me it didn't :-)

#### Johannes Hölzl (Jan 23 2019 at 21:38):

@Chris Hughes I don't know how these proofs work in general. But maybe you need to write more infrastructure around `extensions`

. First, instead of defining it as a `set`

a `Type`

may be more helpful. You need to add a `partial_order`

type class on it, then use `zorn_partial_order`

. Also provide a local `discrete_field (field_of_extension ...)`

instance. Then at least the type class instances shouldn't be a problem. In the end the work is the same, but it might be clearer to see what is required

#### Chris Hughes (Jan 24 2019 at 18:18):

I thought about this, and I've realised it would be easy if we had direct limit.

#### Kenny Lau (Jan 24 2019 at 18:18):

no, direct limit is the easiest part

#### Kenny Lau (Jan 24 2019 at 18:19):

but I might work on direct limit today

Last updated: May 10 2021 at 07:15 UTC