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

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