algebraic closure construction

Stream: maths

[Chris Hughes]

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]

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]

Yes, but that's quite a messy argument.

[Johannes Hölzl]

it is

[Kenny Lau]

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

[Kevin Buzzard]

Wasn't I telling you this last Thursday?

[Kenny Lau]

maybe I wasn't listening :P

[Kevin Buzzard]

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]

@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]

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

[Kenny Lau]

no, direct limit is the easiest part

[Kenny Lau]

but I might work on direct limit today