Zulip Chat Archive

Stream: maths

Topic: algebraic closure construction


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Jan 23 2019 at 21:27):

Yes, but that's quite a messy argument.

view this post on Zulip Johannes Hölzl (Jan 23 2019 at 21:27):

it is

view this post on Zulip Kenny Lau (Jan 23 2019 at 21:28):

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

view this post on Zulip Kevin Buzzard (Jan 23 2019 at 21:29):

Wasn't I telling you this last Thursday?

view this post on Zulip Kenny Lau (Jan 23 2019 at 21:29):

maybe I wasn't listening :P

view this post on Zulip 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 :-)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Jan 24 2019 at 18:18):

no, direct limit is the easiest part

view this post on Zulip 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