Separability degree?

Stream: Is there code for X?

[Jz Pan]

I need to use the maximal separable subextension in the work of separable closure. Thus I need to prove that the sum, difference and product of two separable elements is also separable. This is not in mathlib4 yet. I check the standard textbook and it looks like that the separability degree is needed.

• If L/K is finite algebraic extension of fields, define the separability degree $[L:K]_s$ to be the number of embeddings of L to a fixed algebraic closure $\overline{K}$ of K which is compatible with $K\to L$ and $K\to\overline{K}$.

[Jz Pan]

It has the following properties:

• $[L:K]_s\leq [L:K]$.
• multiplicative: $[M:K]_s=[M:L]_s[L:K]_s$.
• An element $\alpha\in L$ is separable over K if and only if $[K(\alpha):K]_s=[K(\alpha):K]$.
• $[L:K]_s=[L:K]$ if and only if every element $\alpha\in L$ is separable over K, i.e. L/K is a separable field extension.
• As a corollary, if $\alpha_1,\cdots,\alpha_n$ are separable elements over K, then $K(\alpha_1,\cdots,\alpha_n)/K$ is a separable field extension.

Are these in mathlib4 yet?

[Jz Pan]

Besides, if L/K is an algebraic extension of characteristic p fields, x is an element of L, then x is separable over K if and only if K(x)=K(x^p). This is relatively easy to proof. Is it in mathlib4 yet?

[Ruben Van de Velde]

Is this related to the separable degree of a polynomial docs#Polynomial.HasSeparableContraction.degree ?

[Kevin Buzzard]

Really we want the separable degree of a finite extension of fields. If the extension is simple $K(\alpha)/K$ then I suspect that the separable degree of the extension is just the degree of the separable contraction of the min poly of $\alpha$, but there are non-simple extensions all over the place when you drop separability assumptions.

[Jz Pan]

Kevin Buzzard said:

If the extension is simple $K(\alpha)/K$ then I suspect that the separable degree of the extension is just the degree of the separable contraction of the min poly of $\alpha$

Yes I think that's true. The $[K(\alpha):K]_s$ should be just the number of distinct roots of the minimal polynomial of $\alpha$ over K. Is it equal to the degree of the separable contraction?

but there are non-simple extensions all over the place when you drop separability assumptions.

We may use the multiplicity. The $[K(\alpha_1,\cdots,\alpha_n):K]_s$ is the product of $[K(\alpha_1,\cdots,\alpha_i):K(\alpha_1,\cdots,\alpha_{i-1})]_s$ over all 1<=i<=n.

[Junyan Xu]

I think you have a good plan! The items you listed are not in mathlib4 as far as I know, but should be relatively straightforward from what's already there. For example, docs#IntermediateField.adjoin.finrank and docs#IntermediateField.card_algHom_adjoin_integral give you one direction of the third item.

The trickiest one is probably multiplicativity, where you need to switch from the algebraic closure of K to that of L, so it would be easier if you prove any IsAlgClosed extension of the base field gives you the same separable degree.

[Junyan Xu]

I found docs#cardinal_mk_algHom which gives the first item easily (the RHS is obviously equal to finrank K V); otherwise it would take some effort (induction) to prove.

(I found these by looking at files that import Mathlib.FieldTheory.Separable)

[Junyan Xu]

Such general result docs#linearIndependent_toLinearMap should probably be moved much earlier ...
Interesting that what mathlib attributes to Dedekind (docs#linearIndependent_monoidHom) is also attributed to Artin.

[Jz Pan]

Let me post the first WIP draft here:

import Mathlib.FieldTheory.SplittingField.Construction
import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
import Mathlib.FieldTheory.Separable
import Mathlib.RingTheory.IntegralDomain

open scoped Classical Polynomial

open FiniteDimensional Polynomial IntermediateField

noncomputable section

universe u v v' w

variable (F : Type u) (E : Type v) [Field F] [Field E]

variable [Algebra F E]

namespace Field

/-- If `E / F` is an algebraic extension, then the separable degree of `E / F`
is the number of `F`-algebra homomorphisms from `E` to the algebraic closure of `E`.
Note that if `E / F` is not algebraic, then this definition makes no mathematical sense,
for example `sepDegree ℚ ℚ(X)` is countably infinite,
whereas `sepDegree ℚ ℝ` is one (!).
-/
def sepDegree := Cardinal.mk (E →ₐ[F] (AlgebraicClosure E))

def finSepDegree : ℕ := Cardinal.toNat (sepDegree F E)

section Adhoc

variable {F E}

lemma test1 {K : Type w} [Field K] [Algebra F K] (i : E →ₐ[F] K) :
    i.comp (AlgEquiv.ofInjectiveField i).symm.toAlgHom = i.fieldRange.val := by
  sorry

lemma test3 {K : Type w} [Field K] [Algebra F K] (i : E →ₐ[F] K) [IsAlgClosed E] :
    IsAlgClosed i.fieldRange where
  splits := fun p ↦ by
    sorry

lemma test4 (halg : Algebra.IsAlgebraic F E)
    {K : Type w} [Field K] [Algebra F K] (i : E →ₐ[F] K)
    (E' : IntermediateField F K) [IsAlgClosed E'] :
    i.fieldRange ≤ E' := by
  sorry

lemma test5 (halg : Algebra.IsAlgebraic F E)
    {E' : Type v'} [Field E'] [Algebra F E'] [IsAlgClosed E']
    {K : Type w} [Field K] [Algebra F K] (i : E →ₐ[F] K) (i' : E' →ₐ[F] K) :
    i.fieldRange ≤ i'.fieldRange := by
  haveI : IsAlgClosed i'.fieldRange := test3 i'
  exact test4 halg i i'.fieldRange

end Adhoc

lemma sepDegree_nonempty : Nonempty (E →ₐ[F] (AlgebraicClosure E)) :=
  Nonempty.intro <| IsScalarTower.toAlgHom F E (AlgebraicClosure E)

lemma sepDegree_nezero : NeZero (sepDegree F E) := NeZero.mk <| by
  haveI := sepDegree_nonempty F E
  simp only [sepDegree]
  exact Cardinal.mk_ne_zero _

lemma finSepDegree_nezero_of_finiteDimensional [FiniteDimensional F E] :
    NeZero (finSepDegree F E) := NeZero.mk <| by
  haveI := minpoly.AlgHom.fintype F E (AlgebraicClosure E)
  haveI := sepDegree_nonempty F E
  simp only [finSepDegree, sepDegree, Cardinal.mk_toNat_eq_card]
  exact Fintype.card_ne_zero

def sepDegree_equiv_of_equiv (E' : Type v') [Field E'] [Algebra F E'] (i : E ≃ₐ[F] E') :
    (E →ₐ[F] (AlgebraicClosure E)) ≃ (E' →ₐ[F] (AlgebraicClosure E')) := by
  sorry

theorem sepDegree_eq_of_equiv (E' : Type v') [Field E'] [Algebra F E'] (i : E ≃ₐ[F] E') :
    Cardinal.lift.{v'} (sepDegree F E) = Cardinal.lift.{v} (sepDegree F E') := by
  have := ((Equiv.ulift.{v'} (α := E →ₐ[F] (AlgebraicClosure E))).trans
    (sepDegree_equiv_of_equiv F E E' i)).trans
      (Equiv.ulift.{v} (α := E' →ₐ[F] (AlgebraicClosure E'))).symm
  simpa only [Cardinal.mk_uLift] using this.cardinal_eq

theorem finSepDegree_eq_of_equiv (E' : Type v') [Field E'] [Algebra F E'] (i : E ≃ₐ[F] E') :
    finSepDegree F E = finSepDegree F E' := by
  simpa only [Cardinal.toNat_lift] using congr_arg Cardinal.toNat
    (sepDegree_eq_of_equiv F E E' i)

def sepDegree_equiv_of_isAlgClosed (halg : Algebra.IsAlgebraic F E)
    (K : Type w) [Field K] [Algebra F K] [IsAlgClosed K] :
    (E →ₐ[F] (AlgebraicClosure E)) ≃ (E →ₐ[F] K) := by
  have hac := IsAlgClosure.ofAlgebraic F E (AlgebraicClosure E) halg
  let i := IsAlgClosed.lift (M := K) hac.algebraic
  have h1 : Function.Injective i := by
    sorry
  have h2 : Function.Injective (i.comp (A := E)) := by
    sorry
  let i' := AlgEquiv.ofInjectiveField i
  let toFun : (E →ₐ[F] (AlgebraicClosure E)) → (E →ₐ[F] K) :=
    fun f ↦ i.comp f
  let invFun : (E →ₐ[F] K) → (E →ₐ[F] (AlgebraicClosure E)) :=
    fun f ↦ i'.symm.toAlgHom.comp (IntermediateField.inclusion <|
      test5 halg f i) |>.comp f.rangeRestrict
  have right_inv : Function.RightInverse invFun toFun := fun f ↦ by
    simp only
    rw [AlgHom.comp_assoc, ← AlgHom.comp_assoc, test1]
    rfl
  have left_inv : Function.LeftInverse invFun toFun := fun f ↦ by
    exact h2 <| right_inv <| i.comp f
  exact {
    toFun := toFun,
    invFun := invFun,
    left_inv := left_inv,
    right_inv := right_inv,
  }

theorem sepDegree_eq_of_isAlgClosed (halg : Algebra.IsAlgebraic F E)
    (K : Type w) [Field K] [Algebra F K] [IsAlgClosed K] :
    Cardinal.lift.{w} (sepDegree F E) = Cardinal.mk (E →ₐ[F] K) := by
  simpa only [Cardinal.mk_uLift] using ((Equiv.ulift.{w} (α := E →ₐ[F] (AlgebraicClosure E))).trans
    (sepDegree_equiv_of_isAlgClosed F E halg K)).cardinal_eq

theorem finSepDegree_eq_of_isAlgClosed (halg : Algebra.IsAlgebraic F E)
    (K : Type w) [Field K] [Algebra F K] [IsAlgClosed K] :
    finSepDegree F E = Cardinal.toNat (Cardinal.mk (E →ₐ[F] K)) := by
  simpa only [Cardinal.toNat_lift] using congr_arg Cardinal.toNat
    (sepDegree_eq_of_isAlgClosed F E halg K)

theorem sepDegree_self : sepDegree F F = 1 :=
  le_antisymm
    (show sepDegree F F ≤ 1 from Cardinal.le_one_iff_subsingleton.2 AlgHom.subsingleton)
      (Cardinal.one_le_iff_ne_zero.2 (sepDegree_nezero F F).out)

theorem finSepDegree_self : finSepDegree F F = 1 := by
  simp only [finSepDegree, sepDegree_self, Cardinal.one_toNat]

theorem sepDegree_bot : sepDegree F (⊥ : IntermediateField F E) = 1 := by
  have := sepDegree_eq_of_equiv _ _ _ (IntermediateField.botEquiv F E)
  rwa [sepDegree_self, Cardinal.lift_one, ← Cardinal.lift_one.{u, v}, Cardinal.lift_inj] at this

theorem finSepDegree_bot : finSepDegree F (⊥ : IntermediateField F E) = 1 := by
  simp only [finSepDegree, sepDegree_bot, Cardinal.one_toNat]

theorem sepDegree_top : sepDegree F (⊤ : IntermediateField F E) = sepDegree F E := by
  simpa only [Cardinal.lift_id] using sepDegree_eq_of_equiv F _ E IntermediateField.topEquiv

theorem finSepDegree_top : finSepDegree F (⊤ : IntermediateField F E) = finSepDegree F E := by
  simp only [finSepDegree, sepDegree_top]

theorem sepDegree_bot' (K : Type w) [Field K] [Algebra F K] [Algebra E K]
    [IsScalarTower F E K] : Cardinal.lift.{v} (sepDegree F (⊥ : IntermediateField E K)) =
      Cardinal.lift.{w} (sepDegree F E) := by
  exact sepDegree_eq_of_equiv _ _ _ ((IntermediateField.botEquiv E K).restrictScalars F)

theorem finSepDegree_bot' (K : Type w) [Field K] [Algebra F K] [Algebra E K]
    [IsScalarTower F E K] : finSepDegree F (⊥ : IntermediateField E K) = finSepDegree F E := by
  simpa only [Cardinal.toNat_lift] using congr_arg Cardinal.toNat (sepDegree_bot' F E K)

theorem sepDegree_top' (K : Type w) [Field K] [Algebra F K] [Algebra E K]
    [IsScalarTower F E K] : sepDegree F (⊤ : IntermediateField E K) = sepDegree F K := by
  simpa only [Cardinal.lift_id] using sepDegree_eq_of_equiv _ _ _
    ((IntermediateField.topEquiv (F := E) (E := K)).restrictScalars F)

theorem finSepDegree_top' (K : Type w) [Field K] [Algebra F K] [Algebra E K]
    [IsScalarTower F E K] : finSepDegree F (⊤ : IntermediateField E K) = finSepDegree F K := by
  simp only [finSepDegree, sepDegree_top']

-- theorem sepDegree_le_rank : sepDegree F E ≤ Module.rank F E := by sorry

theorem lift_sepDegree_mul_lift_sepDegree_of_isAgebraic_of_adjoin_simple
    (K : Type w) [Field K] [Algebra F K] [Algebra E K]
    [IsScalarTower F E K] (halg : Algebra.IsAlgebraic F E)
    (α : K) (halga : IsAlgebraic E α) :
    Cardinal.lift.{w} (sepDegree F E) * Cardinal.lift.{v} (sepDegree E E⟮α⟯) =
      Cardinal.lift.{v} (sepDegree F E⟮α⟯) := by
  sorry

/-- If `E / F` is an algebraic extension, `K / E` is a finite extension, then
$[K:F]_s = [E:F]_s [K:E]_s$. See also `lift_rank_mul_lift_rank`. -/
theorem lift_sepDegree_mul_lift_sepDegree_of_isAgebraic_of_finiteDimensional
    (K : Type w) [Field K] [Algebra F K] [Algebra E K]
    [IsScalarTower F E K] (halg : Algebra.IsAlgebraic F E) [FiniteDimensional E K] :
    Cardinal.lift.{w} (sepDegree F E) * Cardinal.lift.{v} (sepDegree E K) =
      Cardinal.lift.{v} (sepDegree F K) := by
  let P : IntermediateField E K → Prop := fun L ↦
    Cardinal.lift.{w} (sepDegree F E) * Cardinal.lift.{v} (sepDegree E L) =
      Cardinal.lift.{v} (sepDegree F L)
  have base : P ⊥ := by
    simp only [sepDegree_bot', sepDegree_self, Cardinal.lift_one, mul_one]
  have ih : ∀ (L : IntermediateField E K) (x : K), P L → P (L⟮x⟯.restrictScalars E) := by
    intro L α h
    simp only at h ⊢
    haveI : IsScalarTower F L K := IsScalarTower.of_algebraMap_eq (congrFun rfl)
    have halgL : Algebra.IsAlgebraic F L := by sorry
    have := lift_sepDegree_mul_lift_sepDegree_of_isAgebraic_of_adjoin_simple
      F L K halgL α (isAlgebraic_of_finite L α)
    -- sepDegree ... restrictScalars
    sorry
  simpa only [sepDegree_top'] using induction_on_adjoin P base ih ⊤

theorem finSepDegree_le_finrank_of_adjoin_simple (α : E) (halg : IsAlgebraic F α) :
    finSepDegree F F⟮α⟯ ≤ finrank F F⟮α⟯ := by
  sorry

theorem finSepDegree_le_finrank [FiniteDimensional F E] :
    finSepDegree F E ≤ finrank F E := by
  let P : IntermediateField F E → Prop := fun K ↦
    finSepDegree F K ≤ finrank F K
  have base : P ⊥ := by
    simp only
    rw [finSepDegree_bot, IntermediateField.finrank_bot]
  have ih : ∀ (K : IntermediateField F E) (x : E), P K → P (K⟮x⟯.restrictScalars F) := by
    sorry
  have := induction_on_adjoin P base ih ⊤
  simp only at this
  erw [finrank_top F E] at this
  rwa [finSepDegree_top] at this

end Field

[Jz Pan]

The first goal is to prove:

• Multiplicativity: If E / F is an algebraic extension, K / E is a finite extension, then
  $[K:F]_s = [E:F]_s [K:E]_s$. This should be proved by induction on K / E. When K = E(x), we should have a non-canonical bijection $\operatorname{Hom}_{F}(E,\overline E)\times\operatorname{Hom}_E(E(x),\overline E)\xrightarrow\sim\operatorname{Hom}_F(E(x),\overline E)$

[Jz Pan]

Note that $\operatorname{Hom}_E(E(x),\overline E)$ is 1-to-1 correspondence to the distinct roots in $\overline{E}$ of the minimal polynomial f of x over E, and the above bijection maps $(\phi,\beta)$ to a ring homomorphism $E(x)\to\overline E$ whose restriction on E is $\phi$, and maps x to $\beta$.

[Jz Pan]

• Then we can prove $[E:F]_s\leq [E:F]$ for finite extension E / F by induction, using the simple extension case and the above multiplicativity.

[Jz Pan]

Should these be put inside Mathlib.FieldTheory.SeparableDegree, or in a new file?

[Junyan Xu]

You mean Mathlib.FieldTheory.Separable? I think that file is long enough to warrant a new file.

[Junyan Xu]

we should have a non-canonical bijection

Rather than that, it may work nicer to use docs#Equiv.sigmaFiberEquiv and docs#Cardinal.mk_sigma.

[Jz Pan]

Junyan Xu said:

You mean Mathlib.FieldTheory.Separable? I think that file is long enough to warrant a new file.

No, I mean this https://leanprover-community.github.io/mathlib4_docs/Mathlib/FieldTheory/SeparableDegree.html

[Junyan Xu]

Oh sorry I forgot about that file ... It's short enough and you may want to relate your new results with polynomials' separable degree, so it would be reasonable to put them in the same file. If you start a new file, I'm not sure what it should be named: maybe move the polynomial file to Mathlib/RingTheory/Polynomial/SeparableDegree so you can name your new file Mathlib/FieldTheory/SeparableDegree.

[Anne Baanen]

I'm going to advocate for starting a new file, because the existing file imports much less. My rule of thumb for splitting a file is either when it would grow past 500 - 1000 lines, or when the imports would change.

[Anne Baanen]

(Does file#Mathlib.FieldTheory.SeparableDegree work?)

[Scott Morrison]

Yes, please don't add imports to existing files, essentially ever. (And reviewers, please be very skeptical of this, maybe to the point we want a robot to complain about it.) It is a major cause of rot.

[Mario Carneiro]

Anne Baanen said:

(Does file#Mathlib.FieldTheory.SeparableDegree work?)

I think it has to be separated by / not .: file#Mathlib/FieldTheory/SeparableDegree

[Jz Pan]

Scott Morrison said:

Yes, please don't add imports to existing files, essentially ever. (And reviewers, please be very skeptical of this, maybe to the point we want a robot to complain about it.) It is a major cause of rot.

I see. Fortunately, file#Mathlib/FieldTheory/SeparableDegree is not imported by any other files. So I assume it's OK for this special case? Except for external projects.

[Anne Baanen]

I would still just create a new file: it's much better to have many small files than one huge file, and the best time to split is when writing new things.

[Jz Pan]

I see. So is the current plan to

• rename current Mathlib/FieldTheory/SeparableDegree to Mathlib/RingTheory/Polynomial/SeparableDegree
• ... and create new Mathlib/FieldTheory/SeparableDegree?

[Anne Baanen]

Sounds good to me!

[Jz Pan]

It's tempted to define the notation Field.Emb E F to be E →ₐ[F] (AlgebraicClosure E), which is used in several textbooks. Is it a good idea?

[Jz Pan]

BTW, I made a draft pull request #8117

[Jz Pan]

... just the number of distinct roots of the minimal polynomial of α over K

... and that's the definition of the separable degree of a polynomial in Stacks https://stacks.math.columbia.edu/tag/09H5 . It should be equal to the degree of the separable contraction.

However, currently we lack the definition of the separable degree of a general polynomial; the definition of separable contraction requires the character to be known in advance. So maybe we should add that definition?

[Kevin Buzzard]

Certainly when I've lectured this material, your Field.Emb has played a prominent role in discussions of separability.

[Jz Pan]

Added Emb F E as well as some basic properties to #8117

[Antoine Chambert-Loir]

I don't think so, because that definition singles one particular algebraic closure. And any algebraically closed extension suffices.

[Kevin Buzzard]

But for a definition we use a fixed algebraic closure, and then prove a theorem saying it's the same for any alg closed extension, right? You can't make a definition saying "for all alg closures it's this number which might a priori depend on the choice".

[Jz Pan]

Currently the newly added code in #8117 is more than 300 lines. Should I submit the PR now or should I add more codes to it?

[Riccardo Brasca]

It is already a long PR, so you shouldn't add more stuff. Of course we look forward for more results in others PRs!

[Jz Pan]

I also finished another 300 (:joy:) lines of code about the basic results of separable degree of polynomials.

[Jz Pan]

What is the current progress of #8117? It was "ready-to-merge" for several days, but no further automatic processes taking action.

[Junyan Xu]

Hmm. I didn't notice it's not merged. Probably a bors glitch. Could @Johan Commelin please call bors again?

[Johan Commelin]

I kicked it on the queue again. Hopefully no glitches this time round!

[Jz Pan]

By the way, currently the following things are finished (only stay in my computer for now):

• basic results of separable degree of polynomials
• relation of separable degree of field extensions to that of polynomials
• separable degree of field extensions divides (and hence smaller or equal to) the degree of field extensions
• (relative) separable closure, or called maximal separable subextension, proved that it forms anIntermediateField

The next thing is to prove some separably closed and purely inseparable properties of (relative) separable closure. But I think these two files are not imported by the separable degree file yet.

Is it OK to add these two imports to separable degree file, or it's better to create a new files for (relative) separable closure, and add these two files for import?

[Junyan Xu]

Do you wan to add imports to FieldTheory/SeparableDegree or RingTheory/Polynomial/SeparableDegree? Both are leaf files so I wouldn't mind. Edit: I think AlgebraicClosure is a somewhat heavy import, so maybe the SepClosed file should import the SeparableDegree file(s), not the other way around?

(relative) separable closure, or called maximal separable subextension, proved that it forms anIntermediateField

I have defined the relative algebraic closure as an intermediate field in a branch, and this lemma might be useful to you.

[Jz Pan]

Junyan Xu said:

Do you wan to add imports to FieldTheory/SeparableDegree or RingTheory/Polynomial/SeparableDegree? Both are leaf files so I wouldn't mind. Edit: I think AlgebraicClosure is a somewhat heavy import, so maybe the SepClosed file should import the SeparableDegree file(s), not the other way around?

Currently the FieldTheory/SeparableDegree already imports AlgebraicClosure since the Emb is already defined to be the type of embeddings into AlgebraicClosure. What I want to do is also import IsSepClosed to FieldTheory/SeparableDegree, but only used for stating properties of relative separable closure. But maybe the other way around is better? Or perhaps create a new file SeparableClosure which imports IsSepClosed and SeparableDegree?

PS: I remembered that there seems to be purely inseparable in mathlib, but I didn't find them. Maybe there are no such definitions yet. The only one is Polynomial.contraction_degree_eq_or_insep which mentions insep.

(relative) separable closure, or called maximal separable subextension, proved that it forms anIntermediateField

I have defined the relative algebraic closure as an intermediate field in a branch, and this lemma might be useful to you.

No worries, I already proved that if x is a separable element, then F(x) / F is a separable extension. In particular 1/x is also a separable element.

[Jz Pan]

By the way, currently the following things are finished (only stay in my computer for now)

I will create a (draft) PR soon. :yum:

[Junyan Xu]

Oh indeed! If it already import AlgebraicClosure, importing IsSepClosed adds very little, since IsSepClosed only imports AlgebraicClosure. (IsSepClosed doesn't currently use AlgebraicClosure, but your TODOs will need it.)

[Jz Pan]

Junyan Xu said:

(IsSepClosed doesn't currently use AlgebraicClosure, but your TODOs will need it.)

My plan is some of the remaining TODOs will be implemented in other files :sweat_smile:

[Jz Pan]

I created a new draft PR #8696. Comments are welcomed.

[Jz Pan]

I suspect that there are some redundant codes, for example, it's possible that I used some lengthy code in earlier theorems, but in later theorems I found a simpler way to write code, but I forgot to adapt it to earlier codes.

[Jz Pan]

I want to prove that the degree of the relative separable closure L of a finite extension E/F over the base field F is equal to the separable degree of E/F. But I found that maybe it's harder than what I think before.

As usual, it should be proved by induction:

• If E=F(x), let f be the minimal polynomial of x, with f(X)=g(X^(p^n)) where g is separable. Then I claim that L=F(x^(p^n)). To prove it is indeed the relative separable closure, I should prove that L/F is separable while E/L is purely inseparable, and then I should prove that such characterization is equivalent to L being the relative separable closure. (Note that currently purely inseparable is not defined yet.)
• If K/E/F is a field extension tower, L1, L2, L3 are relative separable closures of E/F, K/E, K/F, respectively, then I should prove that [L3:F] = [L1:F] * [L2:E]. To prove this, first I claim that L3 is indeed equal to the relative separable closure of K/L1. Secondly, I claim that [L3:L1] = [L2:E], which should be proved via that E/L1 is purely inseparable, while L3/L1 is separable, hence they are linearly disjoint over L1. (I think linearly disjoint is not in mathlib yet.) Lastly, L2 should be equal to the compositum of E and L3 over L1, which gives my second claim.

Any suggestions to a simpler proof?

[Junyan Xu]

I think it's easy to show [E:L] must be purely inseparable in general (not just in the E=F(x) case). (If the minimal polynomial of some element x in E has more than 1 root, you contract it to a separable irreducible polynomial with more than 1 root, and adjoining such a root (which exists in E, of the form x^(p^n)) gives you a larger separable subextension of E/F.) By the tower law you've proven, you just need to show the separable degree of a purely inseparable extension is 1, but that easily follows from the definition + induction, as the minimal polynomials have only one root.

[Junyan Xu]

Oh, you also need the separable degree of a separable extension is equal to its degree. Maybe it's in your PRs, didn't look yet ...

[Jz Pan]

Oh, thanks! It's great :rolling_on_the_floor_laughing:

[Jz Pan]

I made a mistake in defining sepDegree F E. Currently it is defined to be the cardinality of Emb F E. Originally I want to prove that it is equal to Module.rank E (separableClosure F E) if E / F is algebraic. It turns out that this is true only when sepDegree F E is finite. When it is infinite, it behaves badly.

[Jz Pan]

For example, $\mathrm{Hom}_{\mathbb{Q}\text{-alg}}(\mathbb{Q}(\mu_{p^\infty}),\overline{\mathbb{Q}})\cong\mathbb{Z}_p^\times$ which is uncountable, but $[\mathbb{Q}(\mu_{p^\infty}):\mathbb{Q}]$ is only countable. So it's possible that the separable degree of an infinite field extension is larger than the degree of the field extension itself :sweat_smile:

Anyone has suggestions? Currently I tend to remove the sepDegree, but only leave Emb and finSepDegree. Then I redefine sepDegree F E to be Module.rank F (separableClosure F E), and I can prove that when Emb is finite, it coincides with the previous definition.

[Junyan Xu]

Indeed, it happens for any algebraic extension of infinite separable degree, where you make infinitely many choices to define an embedding. I suspect #(Emb F E) = 2^Module.rank F (separableClosure F E) is always true in the infinite case (<= is easy but >= may require transfinite induction), and I agree sepDegree should be redefined and finSepDegree can be kept.

[Jz Pan]

OK. I managed to remove sepDegree in #8696.

By the way, it seems that the file SeparableDegree gets too long. Perhaps the new contents should be split into 3 files:

• results directly related to separable degree should be keep in SeparableDegree file
• SeparableClosure should have results related to (relative) separable closure and its properties not involving purely inseparable
• PurelyInseparableshould have the definition of purely inseparable, its properties and its relation to separable closure

I still need to figure out how to organize the latter two files since I found that these properties are usually mixed together. Do you have any suggestions?

[Junyan Xu]

Haven't looked at the PR close enough to form educated suggestions about organization, unfortunately.

Just sharing a random observation: the integrality condition in docs#IsSeparable is redundant when the base ring is nontrivial, because of docs#minpoly.eq_zero and docs#Polynomial.not_separable_zero :)

[Antoine Chambert-Loir]

Couldn't you just define the inseparable degree of an algebraic extension $E \to F$ as $[F : E_s]$, where $E_s$ is the separable closure of $E$ in $F$. And prove the coincidence in the finite case?

[Jz Pan]

Antoine Chambert-Loir said:

Couldn't you just define the inseparable degree of an algebraic extension $E \to F$ as $[F : E_s]$, where $E_s$ is the separable closure of $E$ in $F$. And prove the coincidence in the finite case?

This is my plan. Currently inseparable degree is not defined yet; only separable degree is defined.

I prefer to keep current finSepDegree F E := Cardinal.toNat (Cardinal.mk (Emb F E)) definition since it's crucial to develop the theory of separable closure; without it you can't even prove that the set of separable elements form a field. Then I can define sepDegree F E := Module.rank F (separableClosure F E), and I can prove that finSepDegree F E = Cardinal.toNat (sepDegree F E), namely, they are both finite or infinite, and if they are finite, they coincide.

[Kevin Buzzard]

Why not use docs#Nat.card then? Does anyone care about the cardinality if it's infinite? With Nat.card you just get the answer 0 for infinite sets, and as the degree can't actually be 0 this seems like a really nice use case.

[Jz Pan]

You're right. Nat.card α := Cardinal.toNat (Cardinal.mk α) and that's what I'm exactly looking for. Sorry I overlooked it before. I'll change it later.

[Kevin Buzzard]

Don't apologise -- I'm just trying to help :-)

[Antoine Chambert-Loir]

I rapidly looked at Bourbaki's algebra, and saw they make finiteness assumptions here and there, and couldn't find a general definition by browsing the web. Using docs#Nat.card is nice because that does not assert that the number might be relevant when infinite. In math, we may add an hypothesis to a definition,but that is less natural in Lean.

[Jz Pan]

Sure. Now the definition uses Nat.card instead.

[Jz Pan]

Now I'm stuck with a stupid question: if a vector space is not FiniteDimensional, and given any natural number n, how can I choose n linearly independent elements of it?

[Jz Pan]

More specifically, if E / F is an infinite algebraic extension, for any natural number n, I want to find an intermediate field L such that L / F is finite of degree >= n.

[EDIT] OK, I think induction by n should work. Suppose L / Fis finite of degree >= n, choose any x not in L, then L(x) / F is finite of degree >= n + 1 :joy:

[Junyan Xu]

Jz Pan said:

Now I'm stuck with a stupid question: if a vector space is not FiniteDimensional, and given any natural number n, how can I choose n linearly independent elements of it?

The easiest way I can think of uses docs#IsNoetherian.iff_rank_lt_aleph0, docs#IsNoetherian.iff_fg, docs#Module.rank_def, docs#lt_iSup_iff

[Jz Pan]

OK, finally I'm stuck with this:

lemma _root_.IntermediateField.eq_of_le_of_finrank_le''
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    {F E : IntermediateField K L} [FiniteDimensional K E] (h_le : F ≤ E)
    (h_finrank : finrank K E ≤ finrank K F) : F = E := by
  sorry

This is same as IntermediateField.eq_of_le_of_finrank_le but with FiniteDimensional K L replaced by FiniteDimensional K E. It must be correct. Why is it not in mathlib yet? :sweat_smile:

[Riccardo Brasca]

This

import Mathlib

open FiniteDimensional

lemma _root_.IntermediateField.eq_of_le_of_finrank_le''
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    {F E : IntermediateField K L} [hfin : FiniteDimensional K E] (h_le : F ≤ E)
    (h_finrank : finrank K E ≤ finrank K F) : F = E := by
  apply IntermediateField.toSubalgebra_injective
  apply Subalgebra.toSubmodule_injective
  have : Module.Finite K (Subalgebra.toSubmodule E.toSubalgebra) := hfin
  exact FiniteDimensional.eq_of_le_of_finrank_le h_le (by simpa)

works.

[Riccardo Brasca]

And I think it is a better statement than docs#IntermediateField.eq_of_le_of_finrank_le (it is more general)

[Jz Pan]

Riccardo Brasca said:

And I think it is a better statement than docs#IntermediateField.eq_of_le_of_finrank_le (it is more general)

I think so. Same as other three similar statements (in two of them, replace FiniteDimensional K L by FiniteDimensional F L).

The problem is that does this change make the existing code works seamlessly, namely, can we get FiniteDimensional K E from FiniteDimensional K L automatically via typeclass inference. But the answer is "no" I think? Therefore we need to add four new statements, otherwise the existing code breaks?

[Jz Pan]

Oh, I see that in FiniteDimensional.eq_of_le_of_finrank_le the condition corresponds to FiniteDimensional K E. So the problem is the IntermediateField version being not general enough.

[Junyan Xu]

Yeah the instance from FiniteDimensional K L to FiniteDimensional K E should be safe (where E : IntermediateField K L). If it's not there we should just add it.

[Jz Pan]

Junyan Xu said:

Yeah the instance from FiniteDimensional K L to FiniteDimensional K E should be safe (where E : IntermediateField K L). If it's not there we should just add it.

I found them. They are docs#IntermediateField.finiteDimensional_left and docs#IntermediateField.finiteDimensional_right.

[Jz Pan]

In https://github.com/leanprover-community/mathlib4/blob/561ab0981d6df710afb3d34423378152195e3440/Mathlib/FieldTheory/IntermediateField.lean#L710C77-L710C77

nonrec theorem eq_of_le_of_finrank_le [FiniteDimensional K L] (h_le : F ≤ E)
    (h_finrank : finrank K E ≤ finrank K F) : F = E :=
  toSubalgebra_injective <|
    Subalgebra.toSubmodule.injective <| eq_of_le_of_finrank_le h_le h_finrank

What does the nonrec mean?

[Yaël Dillies]

It means that eq_of_le_of_finrank_le is non-recursive, ie it won't refer to itself (as it would if it were a proof by induction). Without it, Lean would think eq_of_le_of_finrank_le is referring to itself in eq_of_le_of_finrank_le h_le h_finrank even though it's referring to a different theorem (they look the same here because some namespaces have been opened) because of how name resolution works.

[Jz Pan]

I see. Is it not necessary if it's written as FiniteDimensional.eq_of_le_of_finrank_le in the proof?

[Yaël Dillies]

Assuming you got the namespaces right, yes :smile:

[Jz Pan]

I tried to generalize the second statement without success, because its proof uses the first statement, so I have to convert these intermediate fields back and forth :(

import Mathlib.FieldTheory.IntermediateField
import Mathlib.FieldTheory.Adjoin

open FiniteDimensional IntermediateField

lemma _root_.IntermediateField.eq_of_le_of_finrank_le''
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    {F E : IntermediateField K L} [hfin : FiniteDimensional K E] (h_le : F ≤ E)
    (h_finrank : finrank K E ≤ finrank K F) : F = E :=
  haveI : Module.Finite K (Subalgebra.toSubmodule E.toSubalgebra) := hfin
  IntermediateField.toSubalgebra_injective <| Subalgebra.toSubmodule_injective <|
    FiniteDimensional.eq_of_le_of_finrank_le h_le h_finrank

lemma _root_.IntermediateField.eq_of_le_of_finrank_le''''
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    {F E : IntermediateField K L} [hfin : FiniteDimensional F L] (h_le : F ≤ E)
    (h_finrank : finrank F L ≤ finrank E L) : F = E := by
  letI : Algebra F E := (inclusion h_le).toAlgebra
  letI : Module F E := Algebra.toModule
  letI : SMul F E := Algebra.toSMul
  haveI : IsScalarTower F E L := IsScalarTower.of_algebraMap_eq (congrFun rfl)
  haveI := FiniteDimensional.left F E L
  haveI := FiniteDimensional.right F E L
  let E' : IntermediateField F L := (IsScalarTower.toAlgHom F E L).fieldRange
  letI : Algebra F E' := Subalgebra.algebra E'.toSubalgebra
  letI : Module F E' := Algebra.toModule
  letI : SMul F E' := Algebra.toSMul
  have hE : E = restrictScalars K E' := sorry
  have := eq_of_le_of_finrank_le'' (K := F) (L := L) (F := ⊥) (E := E') bot_le <| by
    rw [IntermediateField.finrank_bot]
    have h1 := finrank_mul_finrank F E L
    have h2 : finrank F E = finrank F E' := by
      -- rw [hE] -- this doesn't work
      sorry
    have h3 : 0 < finrank E L := finrank_pos
    nlinarith
  apply_fun restrictScalars K at this
  rw [hE, ← this, restrictScalars_bot_eq_self]

[Jz Pan]

Currently, in mathlib, the proof of the second statement uses the first one. But I suspect there are other proofs?
(PS: Fortunately, I only need to use the generalization of the first statement.)

[Jz Pan]

I tried that the changes to IntermediateField.eq_of_le_of_finrank_le won't break mathlib (https://github.com/leanprover-community/mathlib4/pull/8696/files#diff-136515d94d81377fde45d93d4247bec3ef961127a852be2706600dd0c2424c08). @Riccardo Brasca , would you like to open a PR for these changes? Or should I open a PR?

[Riccardo Brasca]

Feel free to open the PR!

[Junyan Xu]

Here's a proof:

lemma _root_.IntermediateField.eq_of_le_of_finrank_le''''
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    {F E : IntermediateField K L} [hfin : FiniteDimensional F L] (h_le : F ≤ E)
    (h_finrank : finrank F L ≤ finrank E L) : F = E := by
  letI : Algebra F E := (inclusion h_le).toAlgebra
  suffices (⊥ : Subalgebra F E) = ⊤ from h_le.antisymm fun x hx ↦ by
    obtain ⟨x', hx'⟩ := this.ge (by trivial : ⟨x, hx⟩ ∈ ⊤)
    convert ← x'.prop
    exact Subtype.ext_iff.mp hx'
  rw [Subalgebra.bot_eq_top_iff_finrank_eq_one]
  letI : Module F E := Algebra.toModule
  letI : SMul F E := Algebra.toSMul
  letI : IsScalarTower F E L := IsScalarTower.of_algebraMap_eq fun _ ↦ rfl
  haveI := left F E L
  haveI := right F E L
  refine (Nat.le_of_mul_le_mul_left ?_ (finrank_pos : 0 < finrank E L)).antisymm finrank_pos
  rwa [mul_comm, finrank_mul_finrank' F E L, mul_one]

Feel free to PR. I think with some effort we may remove the finiteness conditions from docs#FiniteDimensional.finrank_mul_finrank (and this proof would become a little shorter), and maybe the primed version (with finite free modules) as well.

[Jz Pan]

Junyan Xu said:

Here's a proof: ...

Thank you very much, but @Riccardo Brasca already came up with a proof at https://github.com/leanprover-community/mathlib4/pull/8873#discussion_r1419362683 . I forgot to mention it here.

[Jz Pan]

Currently I'm splitting my PR into small parts, here is the part one: #9041 which consists of the results before separable closure.

[Jz Pan]

It's mostly ready for review.