Zulip Chat Archive

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 (Sep 23 2023 at 09:43):

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 (Sep 23 2023 at 09:45):

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 (Sep 23 2023 at 09:52):

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

Kevin Buzzard (Sep 23 2023 at 10:59):

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 (Sep 23 2023 at 15:08):

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 (Sep 23 2023 at 17:53):

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 (Sep 23 2023 at 18:13):

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 (Sep 23 2023 at 18:21):

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 (Oct 30 2023 at 11:19):

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 (Oct 30 2023 at 11:23):

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 (Oct 30 2023 at 11:27):

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 (Oct 30 2023 at 11:30):

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 (Oct 30 2023 at 11:33):

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

Junyan Xu (Oct 30 2023 at 15:48):

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

Junyan Xu (Oct 30 2023 at 16:25):

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 (Oct 30 2023 at 20:14):

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 (Oct 31 2023 at 02:13):

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 (Oct 31 2023 at 06:58):

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 (Oct 31 2023 at 06:58):

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

Scott Morrison (Oct 31 2023 at 07:37):

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 (Oct 31 2023 at 07:43):

Anne Baanen said:

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

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

Jz Pan (Oct 31 2023 at 12:28):

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 (Oct 31 2023 at 12:32):

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 (Oct 31 2023 at 13:09):

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 (Oct 31 2023 at 13:09):

Sounds good to me!

Jz Pan (Nov 02 2023 at 13:37):

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 (Nov 02 2023 at 13:37):

BTW, I made a draft pull request #8117

Jz Pan (Nov 02 2023 at 19:20):

... 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 (Nov 02 2023 at 22:39):

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

Jz Pan (Nov 03 2023 at 00:38):

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

Antoine Chambert-Loir (Nov 07 2023 at 07:15):

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

Kevin Buzzard (Nov 07 2023 at 08:16):

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 (Nov 13 2023 at 10:37):

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 (Nov 13 2023 at 10:38):

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 (Nov 17 2023 at 02:26):

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

Jz Pan (Nov 28 2023 at 15:49):

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

Junyan Xu (Nov 28 2023 at 15:53):

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

Johan Commelin (Nov 28 2023 at 15:55):

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

Jz Pan (Nov 28 2023 at 16:03):

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 (Nov 28 2023 at 16:29):

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 (Nov 28 2023 at 20:38):

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 (Nov 28 2023 at 20:40):

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 (Nov 28 2023 at 20:56):

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 (Nov 28 2023 at 21:30):

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 (Nov 29 2023 at 01:18):

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

Jz Pan (Nov 29 2023 at 01:23):

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 (Nov 30 2023 at 22:56):

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 (Nov 30 2023 at 23:18):

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 (Nov 30 2023 at 23:20):

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 (Nov 30 2023 at 23:34):

Oh, thanks! It's great :rolling_on_the_floor_laughing:

Jz Pan (Dec 04 2023 at 19:31):

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 (Dec 04 2023 at 19:34):

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 (Dec 04 2023 at 19:59):

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 (Dec 05 2023 at 01:06):

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 (Dec 05 2023 at 06:08):

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 (Dec 05 2023 at 08:02):

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 (Dec 05 2023 at 12:50):

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 (Dec 05 2023 at 13:48):

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 (Dec 05 2023 at 13:55):

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 (Dec 05 2023 at 13:55):

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

Antoine Chambert-Loir (Dec 05 2023 at 22:12):

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 (Dec 06 2023 at 01:31):

Sure. Now the definition uses Nat.card instead.

Jz Pan (Dec 06 2023 at 01:33):

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 (Dec 06 2023 at 01:43):

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 (Dec 06 2023 at 05:06):

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 (Dec 06 2023 at 14:34):

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 (Dec 06 2023 at 15:00):

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 (Dec 06 2023 at 15:00):

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

Jz Pan (Dec 06 2023 at 18:19):

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 (Dec 06 2023 at 18:23):

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 (Dec 06 2023 at 18:24):

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 (Dec 06 2023 at 19:52):

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 (Dec 06 2023 at 19:57):

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 (Dec 06 2023 at 19:59):

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 (Dec 06 2023 at 20:05):

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

Yaël Dillies (Dec 06 2023 at 20:08):

Assuming you got the namespaces right, yes :smile:

Jz Pan (Dec 06 2023 at 20:59):

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 (Dec 06 2023 at 21:03):

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 (Dec 07 2023 at 00:22):

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 (Dec 07 2023 at 07:40):

Feel free to open the PR!

Junyan Xu (Dec 08 2023 at 07:07):

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 (Dec 08 2023 at 14:37):

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 (Dec 13 2023 at 23:54):

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 (Dec 13 2023 at 23:54):

It's mostly ready for review.

Jz Pan (Dec 26 2023 at 01:44):

Now I'm stuck with this:

import Mathlib.FieldTheory.Adjoin

open IntermediateField

noncomputable section

variable (F E : Type*) [Field F] [Field E] [Algebra F E]

lemma test {S : Set E} {x : E} (hx : x ∈ adjoin F S) :
    ∃ T : Finset E, (T : Set E) ⊆ S ∧ x ∈ adjoin F (T : Set E) := by
  simp_rw [← biSup_adjoin_simple S, ← iSup_subtype''] at hx
  obtain ⟨s, hx'⟩ := exists_finset_of_mem_iSup hx
  let T := s.map ⟨Subtype.val, Subtype.val_injective⟩
  refine ⟨T, ?_, ?_⟩
  · have : (T : Set E) ⊆ _ := s.coe_map_subset_range ⟨Subtype.val, Subtype.val_injective⟩
    erw [Subtype.range_coe] at this
    exact this
  sorry

I have no idea how to transfer hx' back to T using iSup_subtype'', etc.

Andrew Yang (Dec 26 2023 at 01:56):

Something like

lemma test {S : Set E} {x : E} (hx : x ∈ adjoin F S) :
    ∃ T : Finset E, (T : Set E) ⊆ S ∧ x ∈ adjoin F (T : Set E) := by
  simp_rw [← biSup_adjoin_simple S, ← iSup_subtype''] at hx
  obtain ⟨s, hx'⟩ := exists_finset_of_mem_iSup hx
  let T := s.map ⟨Subtype.val, Subtype.val_injective⟩
  refine ⟨T, by simp, SetLike.le_def.mp ?_ hx'⟩
  simp only [Finset.coe_map, Function.Embedding.coeFn_mk, iSup_le_iff, adjoin_le_iff,
    Set.le_eq_subset, Set.singleton_subset_iff, SetLike.mem_coe]
  intros x hx
  apply subset_adjoin
  simpa

Andrew Yang (Dec 26 2023 at 01:56):

(I believe you need open IntermediateField?)

Andrew Yang (Dec 26 2023 at 01:57):

The simp comes from simp? [-Subtype.forall] by the way.

Jz Pan (Dec 26 2023 at 01:58):

Andrew Yang said:

(I believe you need open IntermediateField?)

Oh sorry. I just copied from a larger file which open IntermediateField.

Jz Pan (Dec 26 2023 at 02:12):

I think this result could be called IntermediateField.exists_finset_of_mem_adjoin; I need to use it somewhere in purely inseparable.

Jz Pan (Dec 27 2023 at 00:23):

I'm stuck (mathematically) at the following result (which is a lemma used to prove the multiplicity of (infinite) separable degree):

If K / E / F is a field extension tower, such that E / F is algebraic, then separableClosure E K = adjoin E (separableClosure F K).

I have a proof, but it is quite lengthy, and it must involve LinearlyDisjoint (https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Linearly.20disjoint/near/409430232). Here are the steps:

It's easy to prove that adjoin E (separableClosure F K) is contained in separableClosure E K.
So we only need to prove the opposite side: separableClosure E K is contained in adjoin E (separableClosure F K).
The first step is: we may assume that E / F is finite. Suppose x is in separableClosure E K, consider E' which is F adjoin the coefficients of the minimal polynomial of x over E. Then E' / F is finite, and x is contained in separableClosure E' K. Now it's easy to see that we only need to show the result for K / E' / F.
The second step is: we may assume that E / F is finite purely inseparable. It's easy to prove the result when E / F is separable. Then we may consider K / E / S / F where S = separableClosure F E, so that S / F is finite separable and E / S is finite purely inseparable. If the result is true for K / S / F and K / E / S, then it's also true for K / E / F.
The last step is to prove the result for E / F finite purely inseparable. Suppose x is in separableClosure E K, then E(x) / F is finite separable, hence in this case we can use the product formula of (finite) separable degree. Let S = separableClosure F E(x), then we have [S : F] = [E(x) : F]_s = [E(x) : E]_s [E : F]_s = [E(x) : E], hence [E(x) : F] = [E(x) : E] [E : F] = [S : F] [E : F]. On the other hand, S and E are linearly disjoint over F, hence [E(S) : F] = [S : F] [E : F], while E(S) is contained in E(x). Therefore E(S) = E(x), in particular x is contained in E(S), thus is contained in adjoin E (separableClosure F K).

Jz Pan (Dec 27 2023 at 00:24):

Any suggestions for a simpler proof without involving linear disjoint?

Jz Pan (Dec 27 2023 at 00:29):

PS: linearly disjoint is also used from this lemma to the multiplicity of (infinite) separable degree. :sweat_smile:

Junyan Xu (Dec 27 2023 at 02:59):

If you just want to find (in your last bullet point) a basis of S over F that is also a basis of E(S) over E rather than develop the full theory of linear disjointness, you can follow the argument on Cohn's Algebra:
image.png
image.png
~~Lang's Corollary V.6.10 is pretty similar.~~
Cohn also proves that if one of the extensions is separable and one (possibly the same) is normal, then they are linearly disjoint if their intersection is the base field. This applies to our situation since a purely inseparable extension is always normal.

Junyan Xu (Dec 27 2023 at 04:02):

Lang's Corollary V.6.9 gives a pretty different and arguably simpler argument for [ES : F] = [S : F] [E : F]. The idea is that S/F being separable implies that ES/E is also separable, and E/F being purely inseparable implies ES/S is also purely inseparable. The separable degree of ES/E/F must all be contributed by ES/E and the separable degree of ES/S/F must all be contributed by S/F, so [ES:E]=[S:F].

Andrew Yang (Dec 27 2023 at 04:13):

Not sure what the definition you are using but isn't the easiest way to show the multiplicativity of separable degree is to show that $\operatorname{Hom}_K(F, A) \to \operatorname{Hom}_K(E, A)$ is surjective with fibers isomorphic to $\operatorname{Hom}_E(F, A)$

Junyan Xu (Dec 27 2023 at 04:46):

That's already in mathlib as docs#Field.finSepDegree_mul_finSepDegree_of_isAlgebraic. "E/F being purely inseparable implies ES/S is also purely inseparable" will require some characterization of inseparable elements in #9041 though.

Junyan Xu (Dec 27 2023 at 07:10):

Andrew Yang said:

Not sure what the definition you are using but isn't the easiest way to show the multiplicativity of separable degree is to show that $\operatorname{Hom}_K(F, A) \to \operatorname{Hom}_K(E, A)$ is surjective with fibers isomorphic to $\operatorname{Hom}_E(F, A)$

Oh I just realized you're referring to multiplicativity of the infinite separable degree. The answer is that the Hom definition doesn't work in the infinite case, because Hom_K(F,A) have cardinality equal to the continuum when F is a countably-infinite dimensional algebraic extension of K. (Original observed here)

We are now (re-)defining the general separable degree to be the dimension of the relative separable closure over the base field. (Similarly, we could define the inseparable degree to be the dimension of the extension field over the separable closure, and I think it's multiplicative as well.)

Junyan Xu (Dec 27 2023 at 07:52):

Back to the original question, I think this gives an easy proof of the desired fact: to show that separableClosure E K = adjoin E (separableClosure F K) we just need to show the LHS is simultaneously a separable and a purely inseparable extension of the RHS. It's separable because it's separable over E and therefore also separable over the larger field adjoin E _. It's purely inseparable because K is purely inseparable over separableClosure F K and therefore any intermediate field is also purely inseparable over the bigger field adjoin E (separableClosure F K).

Junyan Xu (Dec 27 2023 at 08:29):

A useful thing to show is that the separable closure of K/F is the minimal intermediate field L such that K/L is purely inseparable. (We already know it's the maximal intermediate field separable over F.) For any such intermediate field L, if (for contradiction) it doesn't contain the separable closure, then its intersection with the sep closure is strictly smaller than the sep closure. K can't be purely inseparable over the intersection because there are (separable) elements in the sep closure that is not in the intersection. Therefore L can't be purely inseparable over the intersection, and we may pick a separable element not in the intersection, i.e. not in the sep closure. But by transitivity of separability this element must lie in the sep closure, leading to a contradiction.

Jz Pan (Dec 27 2023 at 15:19):

Andrew Yang said:

Not sure what the definition you are using but isn't the easiest way to show the multiplicativity of separable degree is to show that $\operatorname{Hom}_K(F, A) \to \operatorname{Hom}_K(E, A)$ is surjective with fibers isomorphic to $\operatorname{Hom}_E(F, A)$

That is also already in mathlib as docs#Field.embProdEmbOfIsAlgebraic. However, I'm currently in redefining separable degree in infinite case (#9041), so this does not imply the multiplicity for (infinite) separable degree.

Jz Pan (Dec 27 2023 at 16:10):

Junyan Xu said:

A useful thing to show is that the separable closure of K/F is the minimal intermediate field L such that K/L is purely inseparable.

I already have this: separableClosure_le_iff, but it requires that K/F is algebraic.

Jz Pan (Dec 27 2023 at 16:23):

Junyan Xu said:

Back to the original question, I think this gives an easy proof of the desired fact: to show that separableClosure E K = adjoin E (separableClosure F K) we just need to show the LHS is simultaneously a separable and a purely inseparable extension of the RHS. It's separable because it's separable over E and therefore also separable over the larger field adjoin E _. It's purely inseparable because K is purely inseparable over separableClosure F K and therefore any intermediate field is also purely inseparable over the bigger field adjoin E (separableClosure F K).

Fantastic! The bold part only works when K / F is algebraic, though. A slight modification makes it works for general cases: let S4 := separableClosure F (separableClosure E K), then separableClosure E K / S4 is purely inseparable, since separableClosure E K / F is algebraic. Now S4 ≤ separableClosure F K ≤ adjoin E _ ≤ separableClosure E K, hence separableClosure E K / adjoin E _ is purely inseparable.

Jz Pan (Dec 27 2023 at 16:25):

This proof does not require E / F being finite, hence I can avoid "adjoin the coefficients of the minimal polynomial" (frange) part of proof.

Junyan Xu (Dec 27 2023 at 21:20):

I think we even have S4.map (separableClosure E K).val = separableClosure F K but you may not need that :)

Aside: when we add the general definition of separability of possibly transcendental extensions, should we name it TranscSeparable, or rename the current Separable to AlgSeparable? (The usual definition of the general case depends on the algebraic case.)

Jz Pan (Dec 27 2023 at 21:37):

Junyan Xu said:

Aside: when we add the general definition of separability of possibly transcendental extensions, should we name it TranscSeparable, or rename the current Separable to AlgSeparable? (The usual definition of the general case depends on the algebraic case.)

Hmm, frankly I never used that concept. From https://en.wikipedia.org/wiki/Transcendental_extension it's usually called has separating transcendence basis, or called separably generated.

Junyan Xu (Dec 27 2023 at 22:09):

In Pete Clark's Field Theory p.115-116:

A separating transcendence basis for a field extension K/F is an algebraically independent subset S of K such that K/F (S) is separable algebraic.
We say that a field extension K/F is separably generated if it admits a separating transcendence basis.
An arbitrary field extension K/F is separable if every finitely generated subextension admits a separating transcendence basis.

It's clear for an algebraic extension this is equivalent to the old definition.
There's also stacks#030I

Jz Pan (Dec 28 2023 at 13:29):

Oops, the LaTeX formula in https://leanprover-community.github.io/mathlib4_docs/Mathlib/FieldTheory/SeparableDegree.html is broken, probably due to two _ in the formula confuses the parser, make it think of being italic texts. :sweat_smile: I don't know how to fix it, though.

Ruben Van de Velde (Dec 28 2023 at 13:40):

"File a bug on dog-gen4", probably. I think this feature is known to be somewhat brittle

Utensil Song (Dec 28 2023 at 13:44):

Earlier discussion here, including the doc-gen3 way to fix this.

Jz Pan (Dec 28 2023 at 19:12):

I created #9318, but I don't know if this fix works, since I don't know how to preview it.

Jz Pan (Dec 29 2023 at 00:45):

Junyan Xu said:

I think we even have S4.map (separableClosure E K).val = separableClosure F K but you may not need that :)

Nice observation, I added this as separableClosure.eq_map_of_separableClosure_eq_bot.

Jz Pan (Dec 29 2023 at 00:54):

Now the draft PR #8696 consists of two new files:

Mathlib/FieldTheory/SeparableClosure.lean: the definition and basic properties of (relative) separable closure, about 400 lines.
Mathlib/FieldTheory/PurelyInseparable.lean: the definition and basic properties of purely inseparable extensions, more than 600 lines. This file also contains maximal purely inseparable subextension and its basic properties. I named it perfectClosure since it is just like (relative) perfect closure. Two questions:
- Is it a good name?
- Should I split this part into a new file, perhaps Mathlib/FieldTheory/RelPerfectClosure.lean? Currently this part is about 250 lines.

Andrew Yang (Dec 29 2023 at 01:12):

By the way it would be great to have purely inseparable iff epi in the category of fields.
This will be useful when defining radicial morphisms.

Andrew Yang (Dec 29 2023 at 01:13):

The answer to "should I split this file" is almost always yes.

Jz Pan (Dec 29 2023 at 01:54):

Andrew Yang said:

By the way it would be great to have purely inseparable iff epi in the category of fields.
This will be useful when defining radicial morphisms.

I've not heard it before. Let me study it later.

[EDIT] Currently I have this which may be related to what you said: isPurelyInseparable_iff_finSepDegree_eq_one

By the way, I've heard that it's not a good idea to define an object using universal property over all types, as this will introduce universe problems. Can someone clarify?

Junyan Xu (Dec 29 2023 at 04:05):

it would be great to have purely inseparable iff epi in the category of fields.

That's immediate from

theorem isPurelyInseparable_iff_mem_pow (q : ℕ) [hF : ExpChar F q] :
    IsPurelyInseparable F E ↔ ∀ x : E, ∃ n : ℕ, x ^ (q ^ n) ∈ (algebraMap F E).range := by

(permalink) together with injectivity of Frobenius in the codomain (which must also be of characteristic q).
(but it should go into some file that imports category theory ...)

Andrew Yang (Dec 29 2023 at 04:09):

I think this only gives one direction?

Junyan Xu (Dec 29 2023 at 04:18):

Oh I guess the other direction is what Jz posted, because the finSepDegree of E/F is equal to one means there is exactly one F-embedding of E into the algebraic closure, so if E/F is not purely inseparable there would be at least two embeddings, so F->E isn't an epimorphism.

Andrew Yang (Dec 29 2023 at 04:31):

Yes but we need epi -> algebraic to use that

Junyan Xu (Dec 29 2023 at 05:36):

I have a proof that epi -> algebraic (not yet formalized) but it depends on docs#IsTranscendenceBasis.isAlgebraic and docs#IsAlgClosure.equivOfEquiv. The idea is that you can take a maximal purely transcendental extension T of F in E, over which E is algebraic. If the transcendental basis is not empty (i.e. if E/F is transcendental), then T has nontrivial F-automorphisms (e.g. send a transcendental element x to x+1), which you can extend to its algebraic closure Tbar. If you compose an T-embedding of E into Tbar with this automorphism, you get a different F-embedding, since it's already different when restricted to T. Is there a simpler proof?

Andrew Yang (Dec 29 2023 at 05:40):

The proof I have is more or less the same. We don't have transcendental bases in mathlib afaik though

Junyan Xu (Dec 29 2023 at 05:42):

We have them! It's my first link above (just corrected).

Andrew Yang (Dec 29 2023 at 05:45):

Jz Pan said:

By the way, I've heard that it's not a good idea to define an object using universal property over all types, as this will introduce universe problems. Can someone clarify?

You cannot quantify over all universes so you will end up with a family of definitions and you will need to show that they are equivalent and it will be hard to deal with.

Junyan Xu (Dec 29 2023 at 06:09):

I think we can just generalize isPurelyInseparable_iff_finSepDegree_eq_one to the transcendental case; it's fortunate that our definition of Emb F E uses the algebraic closure of E rather than of F ... Maybe we should go back to revise the claim that "if E / F is not algebraic, then this definition makes no mathematical sense."

Junyan Xu (Dec 29 2023 at 06:23):

By the way, I've heard that it's not a good idea to define an object using universal property over all types, as this will introduce universe problems. Can someone clarify?

It's not forbidden to quantify over a universe in a definition but you have to be careful that the universe is large enough (usually the max of all universes involved) to contain the desired universal object, which would be the same (isomorphic) in all higher universes, but may be trivial in lower universes. (See "ulifting groups doesn't preserve colimits" here.) Plus it's often possible to restrict the objects you quantify over (e.g. for flatness it suffices to consider all (f.g.) ideals of the ring rather than all modules in a universe), and then prove the universal property in all universes higher or lower. It's generally preferable to have a definition that is easy to verify and derive strong consequences from the weak definition.

Jz Pan (Dec 29 2023 at 13:24):

I think maybe it's better not talking about category theory things directly in this file, instead, we may provide necessary results which lead to the desired conclusions directly. For example, for a purely inseparable extension E / F, we can provide a result that it's epi (just add (K : Type w) [Field K] ... to the parameters). Conversely, for an extension which is not purely inseparable, originally we should say "there is a field K which makes it not epi", but perhaps we can find K explicitly, for example, just take some algebraic closure? In this way we can avoid universe level problems.

Andrew Yang (Dec 29 2023 at 16:19):

It would be great if there are universe polymorphic versions, but

universe u
variable (F E : Type u) [Field F] [Field E] [Algebra F E]

example : IsPurelyInseparable F E ↔ ∀ {K : Type u} [Field K],
    Function.Injective (flip RingHom.comp (algebraMap F E) : (E →+* K) → _)

is good enough for me.

Junyan Xu (Dec 29 2023 at 17:01):

Yeah we could provide a category-theory-free version of this result in the PurelyInseparable file. No one would object importing transcendence bases into a new file, I guess.

~~By the way, I think my proof was overly complicated: we can directly compose with the automorphism and we need not use docs#IsAlgClosure.equivOfEquiv to extend it and compose with that.~~ Nope, we still need it.

Jz Pan (Dec 29 2023 at 19:09):

The second part of the PR, #9338, concerning on the separable closure, is ready for review.

Junyan Xu (Dec 29 2023 at 19:40):

Initial comments:

I wonder if it should just be called sepClosure for consistency with docs#IsSepClosure and docs#IsSepClosed? Maybe add a namespace so it becomes IntermediateField.sepClosure.
We don't currently have SepClosure right? Should we define it as the sepClosure in docs#AlgebraicClosure?

Jz Pan (Dec 29 2023 at 20:01):

We have IsAlgClosed, IsAlgClosure but algebraic closure is still called AlgebraicClosure. Not sure sepClosure is a good name.
Also I don't know if it's a good idea to put it into IntermediateField namespace. In my opinion, separableClosure is very like normalClosure, but normalClosure is not in namespace.
AlgebraicClosure is a Type but separableClosure is an IntermediateField. Should we define SeparableClosure as separableClosure converted to a type?

Junyan Xu (Dec 29 2023 at 20:14):

Okay, it seems you are following convention while my suggestions are not.

Lean will know every field has an extension satisfying IsSepClosure through docs#IsSepClosed.of_isAlgClosed and the new separableClosure.isSepClosure. Writing separableClosure F (AlgebraicClosure E) is a bit lengthy though. Maybe we could just add an abbrev SeparableClosure : Type _ := separableClosure F (AlgebraicClosure E).

Jz Pan (Dec 29 2023 at 22:16):

Andrew Yang said:

It would be great if there are universe polymorphic versions, but

universe u
variable (F E : Type u) [Field F] [Field E] [Algebra F E]

example : IsPurelyInseparable F E ↔ ∀ {K : Type u} [Field K],
    Function.Injective (flip RingHom.comp (algebraMap F E) : (E →+* K) → _)

is good enough for me.

What about this:

/-- If `E / F` is purely inseparable, then for any field `L`, the map `(E →+* L) → (F →+* L)`
induced by `algebraMap F E` is injective. In other words, a purely inseparable field extension
is an epimorphism in the category of fields. -/
theorem IsPurelyInseparable.injective_comp_algebraMap [h : IsPurelyInseparable F E]
    (L : Type w) [Field L] : Function.Injective fun f : E →+* L ↦ f.comp (algebraMap F E) := by
  intro f g heq
  ext x
  obtain ⟨q, hF⟩ := ExpChar.exists F
  obtain ⟨n, y, h⟩ := (isPurelyInseparable_iff_mem_pow F E q).1 h x
  replace heq := congr($heq y)
  simp_rw [RingHom.comp_apply, h] at heq
  cases' hF with _ _ hprime _
  · rwa [one_pow, pow_one] at heq
  haveI := charP_of_injective_ringHom (f.comp (algebraMap F E)).injective q
  haveI := Fact.mk hprime
  simp_rw [map_pow, ← iterate_frobenius] at heq
  exact iterate_frobenius_inj L q n heq

/-- If `L` is an algebraically closed field containing `E`, such that the map
`(E →+* L) → (F →+* L)` induced by `algebraMap F E` is injective, then `E / F` is
purely inseparable. In other words, epimorphisms in the category of fields must be
purely inseparable extensions. -/
theorem IsPurelyInseparable.of_injective_comp_algebraMap (L : Type w) [Field L] [IsAlgClosed L]
    (hn : Nonempty (E →+* L)) (h : Function.Injective fun f : E →+* L ↦ f.comp (algebraMap F E)) :
    IsPurelyInseparable F E := by
  sorry

Jz Pan (Dec 29 2023 at 22:18):

I hope the condition in IsPurelyInseparable.of_injective_comp_algebraMap is correct (copied from https://math.stackexchange.com/a/687914).

Junyan Xu (Dec 29 2023 at 22:58):

The statements look fine. In the first theorem [Field L] could be any reduced ring, in which Frobenius is injective. In the second theorem we could replace the IsAlgClosed + Nonempty by a standard minpoly_splits condition, but that requires L be an E-algebra ... Anyway I think we should extract a version of docs#IntermediateField.Lifts.exists_lift_of_splits where algebraMap F K is replaced by algebraMap x.carrier K, which would give us the "extension lemma" in the SE answer, and a simpler proof without using docs#IsAlgClosure.equivOfEquiv.

Jz Pan (Dec 30 2023 at 01:18):

Added separableClosure.eq_adjoin_of_isAlgebraic

If K / E / F is a field extension tower, such that E / F is algebraic, then separableClosure E K = adjoin E (separableClosure F K).

and IsPurelyInseparable.injective_comp_algebraMap.

Jz Pan (Dec 30 2023 at 20:14):

Junyan Xu said:

Anyway I think we should extract a version of docs#IntermediateField.Lifts.exists_lift_of_splits where algebraMap F K is replaced by algebraMap x.carrier K, which would give us the "extension lemma" in the SE answer, and a simpler proof without using docs#IsAlgClosure.equivOfEquiv.

Sounds a good idea. Would you like to do that? Since I'm not familiar with that codebase.

Junyan Xu (Jan 01 2024 at 19:57):

Opened #9392. Several outstanding tasks towards the proof (suggestion to alternative routes also welcome):

a version of docs#IsTranscendenceBasis.isAlgebraic with IntermediateField.adjoin instead of Algebra.adjoin using docs#Algebra.IsAlgebraic.tower_top_of_injective (the file doesn't currently import IntermediateField).
if f : ι → A is an F-AlgebraicIndependent family, then we have IsFractionRing (MvPolynomial ι R) (IntermediateField.adjoin F (Set.range f)) (you need to put the Algebra instance manually though). We can then use MvPolynomial.aeval and IsLocalization.lift to define maps out of adjoin F (Set.range f). In particular, there is an F-AlgHom sending any F-algebraic independent family in a field to any F-algebraic independent family in another field.
transform an algebraic independent family (e.g. replace one element by a nonzero rational function in it, or maybe something similar to Neilsen transformation for free groups) to obtain another indpendent family. Combined with the previous item we obtain nontrivial F-endomorphisms of the purely transcendental extension adjoin F (Set.range f). It would be nice to prove something about the cardinality of the AlgHom/AlgEquiv types, if more precise and general results are possible. (I'd expect F-AlgHoms from F(B) into a field K of transcendental degree d ≥ #B > 0 over F have cardinality equal to #K^#B, because being independent should be a generic property and not reduce the cardinality substantially. Being a generating set (which induces an AlgEquiv) is not generic, but I also expect it not to reduce the cardinality.)

BTW, apparently we don't have transcendence degree and its well-definedness yet.

Junyan Xu (Jan 03 2024 at 03:30):

/poll For an infinite separable algebraic extension E/F, we have #(E →ₐ[F] AlgebraicClosure E) = 2 ^ Module.rank F E.
It's mathematically trivial.
It's true but requires some proof.
I'm not sure if it's true.
It's not always true.

Junyan Xu (Jan 03 2024 at 03:31):

Just a fun survey to gauge how valuable it is to formalize this :)
The first option is meant to say: It is trivial given that the number of embeddings is equal to the rank in the finite case.

Antoine Chambert-Loir (Jan 03 2024 at 06:34):

I'd vote for the second option but am to shy to actually vote. The first one looks definitely wrong to me. On the other hand, I've never seen that result used in algebra; possibly model theory of alg closed fields would use it, I don't know.

Damiano Testa (Jan 03 2024 at 11:25):

I'm not sure if it is true, but I would be more inclined to vote for the second option if you had added the assertion that E/F has countable dimension.

Jz Pan (Jan 03 2024 at 12:05):

Junyan Xu said:

Just a fun survey to gauge how valuable it is to formalize this :)

Maybe you need a human-readable proof first :joy:

Junyan Xu (Jan 03 2024 at 14:37):

Here's some code that may convince you it should be true for arbitrary infinite rank :)

Junyan Xu (Jan 06 2024 at 08:11):

Junyan Xu said:

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.

Okay I've now successfully formalized in #9480 a proof of this conjecture which I made one month ago; some parts are tricky and it takes about 500 lines of code in total, and you can refer to the docstrings if you want to read about formalization details as well as a proof in natural language.
... except there's one sorry left for the general result about algebraic extensions (the separable case is sorry-free), which awaits @Jz Pan's work that shows E / separableClosure F E is purely inseparable to enter mathlib.

Jz Pan (Jan 06 2024 at 11:01):

Junyan Xu said:

... except there's one sorry left for the general result about algebraic extensions (the separable case is sorry-free), which awaits Jz Pan's work that shows E / separableClosure F E is purely inseparable to enter mathlib.

OK, let me submit the existing works of purely inseparable extensions as a PR.

Andrew Yang (Jan 06 2024 at 11:08):

By the way do we have $N_{L/F}(a) = (\prod\limits_{\iota}\iota(a))^{[L:F]_i}$ yet?

Jz Pan (Jan 06 2024 at 12:15):

It's unlikely we have this for general finite extensions. ~~Not sure if~~ it's already in mathlib for finite separable extensions (docs#Algebra.norm_eq_prod_embeddings). I think it is used extensively in algebraic number theory.

Andrew Yang (Jan 06 2024 at 12:22):

We do have the separable version. But this could allow us to drop separability conditions here and there (including docs#Algebra.isIntegral_norm, docs#Algebra.norm_norm etc.) and I was wondering if this will follow from your work?

Jz Pan (Jan 06 2024 at 12:25):

I think this should follows easily. Let me (or someone else) check later.

Jz Pan (Jan 06 2024 at 12:28):

For trace we have docs#trace_eq_sum_embeddings (why is it in global namespace?). By the way we don't have Algebra.charpoly, but only Matrix.charpoly and LinearMap.charpoly (Algebra.charpoly should be defined easily using Matrix.charpoly).

Jz Pan (Jan 06 2024 at 14:38):

The purely inseparable extension #9488 is ready for review. There are several small TODOs (e.g. move results to suitable files) I'll do later. There are also big TODOs I decided to leave for future PRs.

Junyan Xu (Jan 06 2024 at 19:00):

Jz Pan said:

By the way we don't have Algebra.charpoly, but only Matrix.charpoly and LinearMap.charpoly (Algebra.charpoly should be defined easily using Matrix.charpoly).

Can you take docs#LinearMap.charpoly of docs#LinearMap.lsmul, or is Algebra.charpoly is something else? docs#Algebra.lmul is used instead in the definition of trace and norm, but we need not use it for charpoly because charpoly isn't a homomorphism ...

Jz Pan (Jan 06 2024 at 19:45):

You're right, Algebra.charpoly is just S → R[X], it does not preserve addition or multiplication. It is just ~~fun x => (Algebra.lmul R S x).toLinearMap.charpoly~~ fun x => (Algebra.lmul R S x).charpoly.

Junyan Xu (Jan 06 2024 at 20:19):

Algebra.lmul R S is an AlgHom but Algebra.lmul R S x is already a LinearMap ...

Junyan Xu (Jan 06 2024 at 21:06):

Andrew Yang said:

By the way do we have $N_{L/F}(a) = (\prod\limits_{\iota}\iota(a))^{[L:F]_i}$ yet?

You can rewrite the LHS as $N_{L/S}(N_{S/F}(a))$ using docs#Algebra.norm_norm where S is separableClosure F L, and $N_{S/F}(a)= (\prod\limits_{\iota}\iota(a))$ by the separable case (notice the $\iota$ here are actually restrictions from L), and we have $[L:F]_i = [L:S]$ . For x in S, we have $N_{L/S}(x^{[L:S]})=(x^{[L:S]})^{[L:S]}$ by docs#Algebra.norm_algebraMap, because $x^{[L:S]}$ is in L, because L/S is purely inseparable. (Or you can take arbitrary q^n-th power of x that lies in L, not necessarily the [L:S]th power). Then by injectivity of Frobenius we have $N_{L/S}(x)=x^{[L:S]}$ , which concludes the proof.

Junyan Xu (Jan 06 2024 at 22:23):

Whoops, docs#Algebra.norm_norm currently requires separability ...

Andrew Yang (Jan 07 2024 at 04:20):

Yes. One of the applications is to relax the separability condition on that lemma.

Andrew Yang (Jan 07 2024 at 04:22):

For a proof, let $a^{p^n} = a' \in F_s$ , then $N_L/F(a') = N_{F_s/F}(a')^{[L:F]_i} = (\prod\limits_{\iota}\iota(a'))^{[L:F]_i}$ and use the fact that frobenius is injective.

Junyan Xu (Jan 07 2024 at 05:48):

(deleted)

Junyan Xu (Jan 07 2024 at 06:03):

Your first step uses the fact that for a tower L/K/F of extensions and x : K, we have norm F (algebraMap K L x) = norm F x ^ [L : K], which seems missing in mathlib. It can be proven by observing that L is isomorphic to the direct sum of [L : K] copies of K as a K-module and therefore also as an F-module, and that the LHS is the determinant of x acting on L while the RHS is the determinant of x acting on K ^ [L : K] (both as F-modules). The isomorphism conjugates one x-action to the other, so you can show the determinants are equal using docs#LinearMap.det_conj. To compute the determinant of K on K ^ [L : K], however, you probably need something like docs#LinearMap.trace_eq_sum_trace_restrict' (this feels too general; maybe you can work directly with docs#Matrix.blockDiagonal) ...

Junyan Xu (Jan 07 2024 at 06:09):

Hmm, I think docs#Algebra.smul_leftMulMatrix_algebraMap gets most of the way there. (It's used in docs#Algebra.norm_eq_norm_adjoin)

Andrew Yang (Jan 07 2024 at 06:24):

The first step is docs#Algebra.norm_algebraMap

Junyan Xu (Jan 07 2024 at 06:31):

I think it only applies when K=F?
Anyway, I've been able to generalize norm_eq_norm_adjoin itself.
Feel free to push to the branch; it would be nice to systematically generalize all Separable assumptions about norm and trace.

Andrew Yang (Jan 07 2024 at 06:49):

I pushed a generalization of Algebra.norm_algebraMap.

Junyan Xu (Jan 07 2024 at 07:15):

I also pushed a version not assuming finiteness. It would be nice if it doesn't make the proof 1x longer ...

Junyan Xu (Jan 07 2024 at 09:27):

I'd expect F-AlgHoms from F(B) into a field K of transcendental degree d ≥ #B > 0 over F have cardinality equal to #K^#B (here F(B) is a purely transcendental extension of F with basis B)

I thought more about this and by now have convinced myself this is true as well as the following (I now use |X| to denote the cardinality rather than #X):

For a transcendental extension $K/F$ with tr.deg. d > 0, both $\text{dim}_F(K)$ and $\left|K\right|$ are equal to $\max\{\left|F\right|, d, \aleph_0\}$ . (Clearly $\text{dim}_F(K)\le\left|K\right|$ , and the upper bound readily follows from docs#MvPolynomial.cardinal_mk_le_max and docs#Algebra.IsAlgebraic.cardinal_mk_le_max. For the lower bound, it's easy to exhibit linearly independent subsets of cardinalities |F| (take 1/(x-a) for a in F), d (take a transcendence basis), and ℵ₀ (take X^n for n in ℕ).
The number of F-AlgHoms from F(B) to K is clearly bounded above by |K|^|B|. To show it's bounded below by the same, note that |K|=max(|F|,d,ℵ₀) by the above. Showing there are at least |F|^|B| F-AlgHoms is easy: just choose an injective map $f$ from $B$ to a transcendence basis of K/F, then for every function $a : B \to F$ , there is a F-AlgHom sending $b$ to $f(b)+a(b)$ for all $b\in B$ . If d < ℵ₀, we show there are ℵ₀^|B| F-AlgHoms by sending $b$ to $f(b)^{n(b)}$ for each function $n : B \to \N$ . If d ≥ ℵ₀, then we can partition d into |B| (≤ d) parts of size d, so there are at least d^|B| injective maps from B to d, which gives rise to at least d^|B| F-AlgHoms. (If d < |B| there is no F-AlgHom at all, due to well-definedness of tr.deg.)

Junyan Xu (Jan 07 2024 at 09:27):

The same argument can be used to count the number of F-automorphisms (AlgEquiv) of F(B): those $f(b)+a(b)$ readily produce |F|^|B| automorphisms. If |B| ≥ ℵ₀, we have |B| = |B x B| and we can show B ≃ B has cardinality exactly |B|^|B| because for each function $f : B \to B$ and fixed $b_0 \in B$ , the map that sends $(b, b_0) \in B \times B$ to $(b, f(b))$ can be extended to a self-bijection of B x B. These self-bijections of B give rise to F-AlgEquivs of F(B). If |B| < ℵ₀, we need to exhibit ℵ₀^|B|=ℵ₀ F-AlgEquivs of F(B), which is possible if F is infinite, or if |B| > 1 (send (X,Y) to (X,Y+X^n) for algebraically independent X and Y). If F is a finite field and |B|=1, we get PGL(2,F) of order |F|^3-|F|.
To count Field.Emb F F(B), we specialize to K = algebraic closure of F(B), which has tr.deg. d = |B|, so the answer is |F(B)|^|B| = max{|F|,|B|,ℵ₀}^|B|. (This is not always determined by the dimension max{|F|,|B|,ℵ₀}.) A general transcendental extension E is an algebraic extension of some F(B), but the algebraic part E/F(B), even when small in dimension, can contribute disproportionately to Field.Emb F E. For example, there are only countably many embeddings of $\mathbb{Q}(X)/\mathbb{Q}$ into its algebraic closure, but uncountably many automorphisms of $\overline{\mathbb{Q}}/\mathbb{Q}$ , even though both extensions have countable dimension.
In general, we can't say much about the number of F-endomorphisms of an extension over F with a nontrivial algebraic part: it could be very small or very large. For example, the reals have no nontrivial endomorphisms despite having uncountable transcendental degree over the rationals.

Hopefully this gives as complete a picture as it can be regarding the number of embeddings of a transcendental extension.

Jz Pan (Jan 07 2024 at 21:34):

For the trace and norm thing, maybe an explicit description of Field.embProdEmbOfIsAlgebraic F E K is useful, in particular if one of the extensions is purely inseparable, then Field.Emb F E ≃ Field.Emb F K or Field.Emb E K ≃ Field.Emb F K, it's reasonable if we can give an explicit description of these isomorphisms.

Jz Pan (Jan 07 2024 at 21:36):

Or perhaps it's better to work with _ →ₐ[_] L instead of Field.Emb _ _ where L is a sufficient large common field.

Jz Pan (Jan 09 2024 at 20:10):

In the proof of multiplicativity of separable degree, I'm sutck with docs#IntermediateField.intermediateFieldMap, I think this result doesn't require that e to be an isomorphism, but only injective (which is satisfied automatically since they are fields). Same as docs#AlgEquiv.subalgebraMap. Am I missing something? The related one is docs#AlgEquiv.ofInjective, but it can only map the whole ring, but not subalgebras inside it.

Junyan Xu (Jan 09 2024 at 20:16):

The first two are computable so they require the inverses from the AlgEquivs.

Jz Pan (Jan 09 2024 at 20:19):

I see.

I think I have another way to tackle this. Suppose i : E →ₐ[F] K, S : IntermediateField F E, and S' := S.map i. Then S' = (i.comp S.val).fieldRange should be true. Then I can use AlgEquiv.ofInjective to get that isomorphism.

Jz Pan (Jan 09 2024 at 20:20):

We have two related results: docs#AlgHom.fieldRange_eq_map and docs#AlgHom.map_fieldRange, but not the result I mentioned.

Jz Pan (Jan 09 2024 at 20:23):

Oh, I can combine them with docs#Subalgebra.range_val, docs#IntermediateField.range_val or docs#IntermediateField.fieldRange_val. Great!

Jz Pan (Jan 12 2024 at 19:56):

I'm stuck with the following: do we have this?

If K / E / F are field extensions, L is an intermediate field of K / F, B is an F-basis of L, then B generates E(L) as an E-vector space. In particular, [E(L) : E] ≤ [L : F].

I think this holds whenever one of L / F and E / F is algebraic. It's not true if both of them are not algebraic, for example if K=F(X,Y), L=F(X) and E=F(Y).

Junyan Xu (Jan 13 2024 at 01:23):

I think the key is to show that the E-span of a B is a subalgebra (i.e. it contains 1 and is closed under multiplication), and then it follows easily that it equals the E-subalgebra of K generated by L (let me denote it by E[L]). For this you need to write the product of two elements in B as a F-linear combination of elements in B, which, when you multiply by an element of E, will be an E-linear combination of elements in B, i.e. in the E-span of B. Then, if L is algebraic over F then E[L] is algebraic over E (or maybe use docs#IntermediateField.adjoin_algebraic_toSubalgebra directly), and if E is algebraic over F then E[L] is algebraic over L (this one may be hard to state or prove), so in either case E[L] will be a field, so it must equal the intermediate field of K/E generated by L.

Jz Pan (Jan 13 2024 at 10:28):

Oh, and we could add a Subalgebra version of it, which doesn't require any algebraicity conditions I think.

Jz Pan (Jan 13 2024 at 12:07):

I think the following is equivalent to the above statement:

If { u_i } is an F-basis of L, { v_j } is an F-basis of E, then { u_i * v_j } generates E(L) as an F-vector space.

And this statement is symmetric in E and L (of course this means that they should be IntermediateField F K). I think it's closely related to linearly disjoint. Maybe we should call it LinearGenerates?

Jz Pan (Jan 13 2024 at 14:13):

Oh, and we could add a Subalgebra version of it, which doesn't require any algebraicity conditions I think.

Here we go:

import Mathlib.FieldTheory.Adjoin

variable (F E : Type*) [CommSemiring F] [CommSemiring E] [Algebra F E]

variable (K : Type*) [CommSemiring K] [Algebra F K]

variable [Algebra E K] [IsScalarTower F E K]

private lemma test1b (L : Subalgebra F K) {ι : Type*}
    (bL : Basis ι F L) : Subalgebra.toSubmodule (Algebra.adjoin E (L : Set K)) =
    Submodule.span E (Set.range fun i : ι ↦ (bL i).1) := by
  have h0 : (L : Set K) ⊆ Submodule.span E (Set.range fun i : ι ↦ (bL i).1) := fun x hx ↦ by
    erw [Finsupp.mem_span_range_iff_exists_finsupp]
    let y := bL.repr ⟨x, hx⟩
    use y.mapRange (algebraMap F E) (map_zero _)
    have : algebraMap L K (Finsupp.total _ _ _ _ y) = x :=
      congr_arg (algebraMap L K) (bL.total_repr ⟨x, hx⟩)
    rw [Finsupp.total_apply, Finsupp.sum, map_sum (algebraMap L K)] at this
    rw [Finsupp.sum_mapRange_index (by exact fun _ ↦ zero_smul _ _), Finsupp.sum, ← this]
    simp_rw [Algebra.smul_def, map_mul (algebraMap L K), ← IsScalarTower.algebraMap_apply]
    rfl
  have h1 : Algebra.adjoin E (L : Set K) = Algebra.adjoin E (Set.range fun i : ι ↦ (bL i).1) :=
    Algebra.adjoin_eq_of_le _ (h0.trans (Algebra.span_le_adjoin E _)) (Algebra.adjoin_mono <| by
      rintro _ ⟨i, rfl⟩; exact (bL i).2)
  have h2 : (Submonoid.closure (Set.range fun i : ι ↦ (bL i).1) : Set K) ⊆ L := fun _ h ↦
    Submonoid.closure_induction h (by rintro _ ⟨i, rfl⟩; exact (bL i).2) (one_mem L)
      (fun _ _ hx hy ↦ mul_mem hx hy)
  rw [h1]
  exact Algebra.adjoin_eq_span_of_subset _ (h2.trans h0)

It only requires CommSemiring but not Field.

I found that using Submodule.span is more convenient than using Function.Surjective (Finsupp.total ...), since it has more APIs.

Jz Pan (Jan 13 2024 at 19:40):

This is even shorter:

-- NOTE: In fact it only requires `F`, `E`, `K` to be `CommSemiring`.
private lemma test1b' (L : Subalgebra F K) (S : Set K)
    (h : Subalgebra.toSubmodule L = Submodule.span F S) :
    Subalgebra.toSubmodule (Algebra.adjoin E (L : Set K)) = Submodule.span E S := by
  have h0 := h.symm ▸ Submodule.span_le_restrictScalars F E S
  change (L : Set K) ⊆ Submodule.span E S at h0
  have hS : S ⊆ L := by simpa only [← h] using Submodule.subset_span (R := F) (s := S)
  have h1 : Algebra.adjoin E (L : Set K) = Algebra.adjoin E S :=
    Algebra.adjoin_eq_of_le _ (h0.trans (Algebra.span_le_adjoin E _)) (Algebra.adjoin_mono hS)
  have h2 : (Submonoid.closure S : Set K) ⊆ L := fun _ h ↦
    Submonoid.closure_induction h hS (one_mem L) (fun _ _ ↦ mul_mem)
  exact h1.symm ▸ Algebra.adjoin_eq_span_of_subset _ (h2.trans h0)

-- NOTE: In fact it only requires `F`, `E`, `K` to be `CommSemiring`.
private lemma test1b (L : Subalgebra F K) {ι : Type*}
    (bL : Basis ι F L) : Subalgebra.toSubmodule (Algebra.adjoin E (L : Set K)) =
    Submodule.span E (Set.range fun i : ι ↦ (bL i).1) := by
  refine test1b' F E K L _ ?_
  simpa only [← L.range_isScalarTower_toAlgHom, Submodule.map_span, Submodule.map_top,
    ← Set.range_comp] using congr_arg (Submodule.map L.val) bL.span_eq.symm

Jz Pan (Jan 13 2024 at 19:48):

What about calling it Subalgebra.adjoin_eq_span_of_eq_span and Subalgebra.adjoin_eq_span_basis?

Jz Pan (Jan 14 2024 at 00:30):

Now I'm stuck at this:

import Mathlib.FieldTheory.Adjoin

variable (F E : Type*) [Field F] [Field E] [Algebra F E]

variable (K : Type*) [Field K] [Algebra F K]

variable [Algebra E K] [IsScalarTower F E K]

-- TODO: move to suitable location
-- NOTE: In fact it only requires `F`, `E`, `K` to be `CommSemiring`.
variable {F K} in
lemma Subalgebra.adjoin_eq_span_of_eq_span (L : Subalgebra F K) {S : Set K}
    (h : Subalgebra.toSubmodule L = Submodule.span F S) :
    Subalgebra.toSubmodule (Algebra.adjoin E (L : Set K)) = Submodule.span E S := by
  have h0 := h.symm ▸ Submodule.span_le_restrictScalars F E S
  change (L : Set K) ⊆ Submodule.span E S at h0
  have hS : S ⊆ L := by simpa only [← h] using Submodule.subset_span (R := F) (s := S)
  have h1 : Algebra.adjoin E (L : Set K) = Algebra.adjoin E S :=
    Algebra.adjoin_eq_of_le _ (h0.trans (Algebra.span_le_adjoin E _)) (Algebra.adjoin_mono hS)
  have h2 : (Submonoid.closure S : Set K) ⊆ L := fun _ h ↦
    Submonoid.closure_induction h hS (one_mem L) (fun _ _ ↦ mul_mem)
  exact h1.symm ▸ Algebra.adjoin_eq_span_of_subset _ (h2.trans h0)

-- TODO: move to suitable location
-- NOTE: In fact it only requires `F`, `E`, `K` to be `CommSemiring`.
variable {F K} in
lemma Subalgebra.adjoin_eq_span_basis (L : Subalgebra F K) {ι : Type*}
    (bL : Basis ι F L) : Subalgebra.toSubmodule (Algebra.adjoin E (L : Set K)) =
    Submodule.span E (Set.range fun i : ι ↦ (bL i).1) := by
  refine L.adjoin_eq_span_of_eq_span E ?_
  simpa only [← L.range_isScalarTower_toAlgHom, Submodule.map_span, Submodule.map_top,
    ← Set.range_comp] using congr_arg (Submodule.map L.val) bL.span_eq.symm

-- TODO: move to suitable location
-- NOTE: In fact it only requires `F` be `Field`, others be `CommRing`.
variable {F K} in
lemma Subalgebra.adjoin_rank_le (L : Subalgebra F K) :
    Module.rank E (Algebra.adjoin E (L : Set K)) ≤ Module.rank F L := by
  obtain ⟨ι, ⟨bL⟩⟩ := Basis.exists_basis F L
  change Module.rank E (Subalgebra.toSubmodule (Algebra.adjoin E (L : Set K))) ≤ _
  rw [L.adjoin_eq_span_basis E bL, ← bL.mk_eq_rank'']
  exact rank_span_le _ |>.trans Cardinal.mk_range_le

-- TODO: move to suitable location
-- TODO: In fact it only requires either `L / F` or `E / F` is algebraic
variable {F K} in
lemma IntermediateField.adjoin_rank_le_of_isAlgebraic (L : IntermediateField F K)
    (halg : Algebra.IsAlgebraic F L) :
    Module.rank E (adjoin E (L : Set K)) ≤ Module.rank F L := by
  change Module.rank E (adjoin E (L.toSubalgebra : Set K)).toSubalgebra ≤ _
  have : _ ≤ Module.rank F L := L.toSubalgebra.adjoin_rank_le E
  have : ∀ x ∈ (L.toSubalgebra : Set K), IsAlgebraic E x := fun x hx ↦
    IsAlgebraic.tower_top E (isAlgebraic_iff.1 (halg ⟨x, hx⟩))
  -- rw [adjoin_algebraic_toSubalgebra this]
  sorry

Jz Pan (Jan 14 2024 at 00:31):

In the last result I want to rw something, but no matter what I have tried, it always complains about motive is not correct. What should I do?

Jz Pan (Jan 14 2024 at 00:47):

Problem solved (ad-hoc): use (Subalgebra.equivOfEq ...).toLinearEquiv.rank_eq

Jz Pan (Jan 15 2024 at 14:35):

Tower law for (infinite) separable degree is added in #9488. I'll look at the suggestions on perfectClosure by @Junyan Xu in the following days.

Jz Pan (Jan 15 2024 at 14:36):

I should say now it's too many codes in it.

Jz Pan (Feb 22 2024 at 00:47):

In my draft there are two results which are not used in the proof of multiplicity of separable degrees. I don't know if they are useful or not, and if they should be added into the purely inseparable file.

(A) If E / F is purely inseparable, f is a separable irreducible polynomial in F[X], then it is also irreducible in E[X].

(B) If K / E / F is a field extension tower such that E / F is purely inseparable, if x is an element of K whose minimal polynomial over F is separable, then it has the same minimal polynomial over F and over E.

Clearly the (B) implies (A) by taking K to be E adjoin a root of f.

Jz Pan (Feb 22 2024 at 00:56):

The proof of (B) can be proceeded as follows: from F(x) / F separable we know that E(x) / E is also separable (an easy consequence of docs#separableClosure.adjoin_eq_of_isAlgebraic), while E(x) / F(x)is purely inseparable (by pow_mem). Apply the multiplicity of (finite) separable degree we know that F(x) / F and E(x) / E have the same degree, which yields the conclusion. (Or one can use docs#Field.sepDegree_eq_of_isPurelyInseparable_of_isSeparable.) Any other simpler proof?

Kevin Buzzard (Feb 22 2024 at 07:38):

I would throw them in anyway

Jz Pan (Feb 29 2024 at 01:29):

Kevin Buzzard said:

I would throw them in anyway

added as #10882. Comments welcome.

Jz Pan (Mar 13 2024 at 04:00):

ping any progress on reviewing #10404?

Kim Morrison (Mar 13 2024 at 04:05):

@Junyan Xu, do you have time to look at this again? If you're happy with this I can merge.

Junyan Xu (Mar 13 2024 at 08:54):

Thanks for the ping, I've approved!

Riccardo Brasca (Mar 13 2024 at 10:17):

What is the situation of separability degree in mathlib? I remember we wanted (or maybe we did) change the definition, or something like that.

Jz Pan (Mar 13 2024 at 12:06):

Riccardo Brasca said:

What is the situation of separability degree in mathlib? I remember we wanted (or maybe we did) change the definition, or something like that.

We changed the definition of separable degree of infinite extensions. Now all the definitions are consistent, and almost all results are proved, except for the multiplicity of inseparable degree of infinite extensions (needs linearly disjointness), and one or two hard TODOs regarding transcendental extensions.

Another thing to be done is generalize results of traces, norms, characteristic polynomials, etc., of a finite extension to non-separable case, see the discussion in this thread.

Junyan Xu (Oct 23 2024 at 20:54):

One consequence of #(Emb F E) = 2^Module.rank F (separableClosure F E) (in the infinite case) is that the order of an infinite Galois group is always a power of 2. Since every profinite group can be realized as a Galois group, this shows the order of an infinite profinite group must be a power of 2. I have been able to find a direct proof of this fact in this paper, which also use transfinite induction:
image.png

Jz Pan (Oct 24 2024 at 06:02):

Junyan Xu said:

the order of an infinite profinite group must be a power of 2

Interesting.

Antoine Chambert-Loir (Oct 24 2024 at 20:54):

that's about cardinality, isn't it? so $2^{\aleph_0}=3^{\aleph_0}$ .

Junyan Xu (Oct 24 2024 at 21:28):

Yeah, in fact if c is infinite then c^c=2^c (docs#Cardinal.power_self_eq). I used docs#Cardinal.power_eq_two_power in my proof. But 2^c is probably the canonical form as it's clearly the cardinality of the power set of c.

Antoine Chambert-Loir (Oct 25 2024 at 10:24):

Yes, but my remark was that “the order of an infinite profinite group is a power of 2” is definitely misleading. I think everybody would understand its a pro-2-group (and then, it's not a pro-3-group), while the expression is used above to mean that its cardinality is the continuum.

Kevin Buzzard (Oct 25 2024 at 19:43):

Yes one of Serre's books has a definition of pro-order of a profinite group and it's of the form 2^a3^b5^c..., a possibly infinite product and where a,b,c,... are enats. This is a far more useful concept than the idea being talked about here.

Adam Topaz (Oct 25 2024 at 20:00):

I think Serre called them "supernatural" numbers :)

Adam Topaz (Oct 25 2024 at 20:01):

A ton of stuff from finite group theory carries through to profinite groups with this definition. E.g. you have essentially direct analogues of the Sylow theorems, the fact that given any supernatural number, there is a unique cyclic profinite group with that order, etc.

Kevin Buzzard (Oct 25 2024 at 20:22):

Maybe it is the case that the powers should be cardinals or something? (Serre only needed to distinguish the finite from the infinite). And then perhaps the "square" result follows, with the answer being that the order is something like 2^max(a,b,c,...)? Just guessing, didn't think too hard about it.

Jz Pan (Nov 08 2024 at 18:51):

Field.Emb is infinite for transcendental extension #18770 is ready for review, modulo dependencies.

Jz Pan (Nov 09 2024 at 06:10):

Another question: do you think it's good to change def Emb := ... to abbrev Emb := ...? Currently it's the first one. But this causes some small troubles: an element in Emb cannot be converted to an AlgHom directly...

Junyan Xu (Nov 09 2024 at 13:20):

You're very close to this now, right?

I think it's reasonable to make Emb an abbrev.

Jz Pan (Nov 09 2024 at 13:45):

Junyan Xu said:

You're very close to this now, right?

I think yes.

Junyan Xu (Nov 16 2024 at 00:51):

This is now included in #18770:
image.png

Junyan Xu (Jan 24 2025 at 00:53):

#Is there code for X? > Separability degree? @ 💬
OpenAI's o1-2024-12-17 has been able to come up with #(Emb F E) = 2^Module.rank F E for infinite separable algebraic extension E/F! And the reasoning looks reasonable too. The question I asked:

If E/F is a separable, infinite, algebraic extension of fields, how many embeddings are there from E into the algebraic closure of E over F? Compute the exact cardinality and express your answer in terms of the degree [E:F].

The models' responses:
image.png
image.png

You can throw your most difficult questions at the best models by submitting a question at agi.safe.ai/submit

Junyan Xu (Jan 24 2025 at 00:54):

I asked DeepSeek-r1 the same question three times yesterday and each time it was able to guess the correct answer somewhere in the middle of its thoughts, but later confused itself and outputted wrong answers. Finally I was able to get the right answer with a follow-up question. During the third conversation I first asked

If E/F is a separable algebraic extension of fields, how many embeddings are there from E into the algebraic closure of E over F? Is it a function of the degree [E:F]?

And it said in the finite case the answer is [E:F]. Then I asked

What happens in the infinite case? Is the number of embeddings still a function of [E:F]?

and it's able to produce the following answer after 61 seconds, but IMO it's reasoning isn't as solid as o1's.

image.png

Luigi Massacci (Jan 24 2025 at 15:50):

If you want to try an experiment that I’ve always found enlightening with chatgpt, fix some specific values for E and F, and then see if it still gets it right. In my experience it’s 50/50 at best

Luigi Massacci (Jan 24 2025 at 15:54):

Here is an example of my own from some time ago, with a similar mathematical question:
IMG_0877.jpeg
IMG_0876.jpeg

Junyan Xu (Jan 24 2025 at 16:14):

In the email notification I see you said "o1-mini", but you edited it to "chatgpt". Are you indeed using o1-mini regularly? I think o1-2024-12-17 is probably (a preview?) of the full version of o1. o1 might still be better than DS-r1 in some aspects, but it's very nice that DS-r1 shows the model's thoughts completely (it's open source after all) and is free (for now).

Luigi Massacci (Jan 25 2025 at 12:48):

My apologies for the confusion, I changed it to “chatgpt” since I realised that specific example came from a session with just the basic free 4o version. I’ve used o1-mini in the past (a former flatmate was paying…) and ran into similar issues

Luigi Massacci (Jan 25 2025 at 12:52):

Also, I just tried it with deepseek r1, and it got the answer wrong even for the “theoretical” version, though like in your case it actually nearly had the correct reasoning in between

Luigi Massacci (Jan 25 2025 at 12:52):

and I agree it’s nice you can see the whole chain of thought, and that it being open source is in itself valuable

Andrew Yang (Feb 17 2025 at 18:47):

Do we have the formula for norms (as a product of conjugates) for non-separable extensions?

Jz Pan (Feb 18 2025 at 05:59):

Andrew Yang said:

Do we have the formula for norms (as a product of conjugates) for non-separable extensions?

Not sure. I think there are some discussions in this thread, but seems that there are no PRs working on it.

Junyan Xu (Feb 19 2025 at 01:39):

Should be straightforward from the separable-purely inseparable factorization now that we have general transitivity of norms.

Last updated: May 02 2025 at 03:31 UTC

Stream: Is there code for X?

Topic: Separability degree?

Jz Pan (Sep 23 2023 at 09:41):

Jz Pan (Sep 23 2023 at 09:43):

Jz Pan (Sep 23 2023 at 09:45):

Ruben Van de Velde (Sep 23 2023 at 09:52):

Kevin Buzzard (Sep 23 2023 at 10:59):

Jz Pan (Sep 23 2023 at 15:08):

Junyan Xu (Sep 23 2023 at 17:53):

Junyan Xu (Sep 23 2023 at 18:13):

Junyan Xu (Sep 23 2023 at 18:21):

Jz Pan (Oct 30 2023 at 11:19):

Jz Pan (Oct 30 2023 at 11:23):

Jz Pan (Oct 30 2023 at 11:27):

Jz Pan (Oct 30 2023 at 11:30):

Jz Pan (Oct 30 2023 at 11:33):

Junyan Xu (Oct 30 2023 at 15:48):

Junyan Xu (Oct 30 2023 at 16:25):

Jz Pan (Oct 30 2023 at 20:14):

Junyan Xu (Oct 31 2023 at 02:13):

Anne Baanen (Oct 31 2023 at 06:58):

Anne Baanen (Oct 31 2023 at 06:58):

Scott Morrison (Oct 31 2023 at 07:37):

Mario Carneiro (Oct 31 2023 at 07:43):

Jz Pan (Oct 31 2023 at 12:28):

Anne Baanen (Oct 31 2023 at 12:32):

Jz Pan (Oct 31 2023 at 13:09):

Anne Baanen (Oct 31 2023 at 13:09):

Jz Pan (Nov 02 2023 at 13:37):

Jz Pan (Nov 02 2023 at 13:37):

Jz Pan (Nov 02 2023 at 19:20):

Kevin Buzzard (Nov 02 2023 at 22:39):

Jz Pan (Nov 03 2023 at 00:38):

Antoine Chambert-Loir (Nov 07 2023 at 07:15):

Kevin Buzzard (Nov 07 2023 at 08:16):

Jz Pan (Nov 13 2023 at 10:37):

Riccardo Brasca (Nov 13 2023 at 10:38):

Jz Pan (Nov 17 2023 at 02:26):

Jz Pan (Nov 28 2023 at 15:49):

Junyan Xu (Nov 28 2023 at 15:53):

Johan Commelin (Nov 28 2023 at 15:55):

Jz Pan (Nov 28 2023 at 16:03):

Junyan Xu (Nov 28 2023 at 16:29):

Jz Pan (Nov 28 2023 at 20:38):

Jz Pan (Nov 28 2023 at 20:40):

Junyan Xu (Nov 28 2023 at 20:56):

Jz Pan (Nov 28 2023 at 21:30):

Jz Pan (Nov 29 2023 at 01:18):

Jz Pan (Nov 29 2023 at 01:23):

Jz Pan (Nov 30 2023 at 22:56):

Junyan Xu (Nov 30 2023 at 23:18):

Junyan Xu (Nov 30 2023 at 23:20):

Jz Pan (Nov 30 2023 at 23:34):

Jz Pan (Dec 04 2023 at 19:31):

Jz Pan (Dec 04 2023 at 19:34):

Junyan Xu (Dec 04 2023 at 19:59):

Jz Pan (Dec 05 2023 at 01:06):

Junyan Xu (Dec 05 2023 at 06:08):

Antoine Chambert-Loir (Dec 05 2023 at 08:02):

Jz Pan (Dec 05 2023 at 12:50):

Kevin Buzzard (Dec 05 2023 at 13:48):

Jz Pan (Dec 05 2023 at 13:55):

Kevin Buzzard (Dec 05 2023 at 13:55):

Antoine Chambert-Loir (Dec 05 2023 at 22:12):

Jz Pan (Dec 06 2023 at 01:31):

Jz Pan (Dec 06 2023 at 01:33):

Jz Pan (Dec 06 2023 at 01:43):

Junyan Xu (Dec 06 2023 at 05:06):

Jz Pan (Dec 06 2023 at 14:34):

Riccardo Brasca (Dec 06 2023 at 15:00):

Riccardo Brasca (Dec 06 2023 at 15:00):

Jz Pan (Dec 06 2023 at 18:19):

Jz Pan (Dec 06 2023 at 18:23):

Junyan Xu (Dec 06 2023 at 18:24):

Jz Pan (Dec 06 2023 at 19:52):

Jz Pan (Dec 06 2023 at 19:57):

Yaël Dillies (Dec 06 2023 at 19:59):

Jz Pan (Dec 06 2023 at 20:05):

Yaël Dillies (Dec 06 2023 at 20:08):

Jz Pan (Dec 06 2023 at 20:59):