## Stream: Is there code for X?

### Topic: separable/purely inseparable extension and separable closure

#### 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)?

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

#### Johan Commelin (Dec 29 2020 at 13:41):

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

#### Johan Commelin (Dec 29 2020 at 13:42):

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

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


#### Johan Commelin (Dec 29 2020 at 13:45):

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

Sure.

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