separable/purely inseparable extension and separable closure

Stream: Is there code for X?

[Jz Pan]

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]

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]

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

[Johan Commelin]

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

[Jz Pan]

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]

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

[Jz Pan]

Sure.

[Thomas Browning]

Johan Commelin said:

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

I don't think so either.

[Jz Pan]

Sorry to bump this message. Now there is separable extension in mathlib4. I'm working on separable closed field and separable closure. I think purely inseparable extension is still not here, but not hard to add.