Zulip Chat Archive

Stream: Is there code for X?

Topic: separable/purely inseparable extension and separable closure


view this post on Zulip Jz Pan (Dec 29 2020 at 12:21):

I believe that there is code for separable extension (haven't checked yet). Are there codes for separable closed field, separable closure, and purely inseparable extensions (as well as their classifications)?

view this post on Zulip Jz Pan (Dec 29 2020 at 12:22):

Now I just need the concept of separable closed field. I just use the following definition for now: any non-constant separable polynomial has a root.

view this post on Zulip Johan Commelin (Dec 29 2020 at 13:41):

@Thomas Browning @Patrick Lutz are our field extension experts.

view this post on Zulip Johan Commelin (Dec 29 2020 at 13:42):

I think we don't have separable closure or separable closed fields yet.

view this post on Zulip Jz Pan (Dec 29 2020 at 13:44):

OK, now I just use the following code:

def my_sep_closed (K : Type*) [field K] :=
 f : polynomial K, f.separable  f.degree  0   x : K, polynomial.eval₂ (ring_hom.id K) x f = 0

lemma alg_closed_implies_sep_closed (K : Type*) [field K] :
is_alg_closed K  my_sep_closed K :=
begin
  intros hac f hsep hdeg,
  have hsplit := @polynomial.splits' K K _ hac _ (ring_hom.id K) f,
  exact polynomial.exists_root_of_splits (ring_hom.id K) hsplit hdeg,
end

view this post on Zulip Johan Commelin (Dec 29 2020 at 13:45):

@Jz Pan note that eval2 id ... can be written as eval ...

view this post on Zulip Jz Pan (Dec 29 2020 at 14:01):

Sure.

view this post on Zulip Thomas Browning (Dec 29 2020 at 16:35):

Johan Commelin said:

I think we don't have separable closure or separable closed fields yet.

I don't think so either.


Last updated: May 17 2021 at 15:13 UTC