stuck with IntermediateField of IntermediateField

Stream: new members

[Jz Pan]

I'm sutck with problems regarding IntermediateField of IntermediateField:

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

example (F : Type) [Field F] (E : Type) [Field E] [Algebra F E]
    (K : IntermediateField F E) (L : IntermediateField F K) (α : E) : True := by
  have hdvd : minpoly K α ∣ Polynomial.map (algebraMap L K) (minpoly L α) :=
    sorry -- minpoly.dvd_map_of_isScalarTower L K α
  sorry

Lean complains that K is not an L-algebra. I have no idea how to fix it. Any suggestions?

[Jz Pan]

It typechecks if I change L to L.toSubfield, but the proof still doesn't work:

example (F : Type) [Field F] (E : Type) [Field E] [Algebra F E]
    (K : IntermediateField F E) (L : IntermediateField F K) (α : E) : True := by
  have hdvd : minpoly K α ∣ Polynomial.map (algebraMap L.toSubfield K) (minpoly L.toSubfield α) :=
    minpoly.dvd_map_of_isScalarTower L.toSubfield K α
  sorry

It complains that failed to synthesize SMul { x // x ∈ K } { x // x ∈ K }.

[Eric Wieser]

What's the full error? Does it say it timed out?

[Riccardo Brasca]

Yes that looks like a timeout, but sometimes it just says it doesn't find the instance.

[Kevin Buzzard]

Can you get away with L : IntermediateField F E and L <= K?

[Anne Baanen]

I've found that Lean is unfortunately not very good at nested structures, like IntermediateFields of IntermediateFields, or subalgebras of quotients of polynomials of splitting fields, etc. If you're taking an IntermediateField as an assumption, like here, very often you can replace it with an arbitrary field + IsScalarTower hypothesis:

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

example (F E K L : Type) [Field F] [Field E] [Algebra F E] [Field K] [Field L]
    [Algebra F K] [Algebra K E] [IsScalarTower F K E]
    [Algebra F L] [Algebra L K] [IsScalarTower F L K]
    [Algebra L E] [IsScalarTower L K E]
    (α : E) : True := by
  have hdvd : minpoly K α ∣ Polynomial.map (algebraMap L K) (minpoly L α) :=
    minpoly.dvd_map_of_isScalarTower L K α
  sorry

[Jz Pan]

Thanks. In fact I'm working on this:

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

open scoped Classical Polynomial

open FiniteDimensional Polynomial IntermediateField

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

variable [Algebra F E] [FiniteDimensional F E]

-- A finite simple extension has only finitely many intermediate fields
theorem Field.finite_intermediateField_of_exists_primitive_element :
    (∃ α : E, F⟮α⟯ = ⊤) → Finite (IntermediateField F E) := by
  intro ⟨α, h⟩
  -- Let `f` bethe minimal polynomial of `α ∈ E` over `F`
  let f : Polynomial F := minpoly F α
  -- If `K` is an intermediate field of `E/F`, let `g` be the minimal polynomial of `α ∈ E` over `K`
  let g : (K : IntermediateField F E) → Polynomial K := fun K => minpoly K α
  -- ... and let `L` be the field over `F` generated by coefficients of `g`
  let L : (K : IntermediateField F E) → IntermediateField F K := fun K =>
    IntermediateField.adjoin F (Set.range (g K).toFinsupp)
  -- Then `L = K`
  have hL : ∀ K, L K = ⊤ := fun K => by
    let h : Polynomial (L K).toSubfield := minpoly (L K).toSubfield α
    have hdvd : g K ∣ Polynomial.map (algebraMap (L K).toSubfield K) h :=
      sorry -- minpoly.dvd_map_of_isScalarTower (L K).toSubfield K α
    sorry
  let G := { g : Polynomial E // g.Monic ∧ g ∣ f.map (algebraMap F E) }
  -- ... and `g` is a monid factor of `f`
  let g' : IntermediateField F E → G := fun K =>
    ⟨(g K).map (algebraMap K E), ⟨Monic.map (algebraMap K E) $
      minpoly.monic $ isAlgebraic_iff_isIntegral.1 $ isAlgebraic_of_finite K α,
    by
      simp only
      have hdvd : minpoly K α ∣ Polynomial.map (algebraMap F K) (minpoly F α) :=
        minpoly.dvd_map_of_isScalarTower F K α
      sorry⟩⟩
  -- The map `K ↦ g` is injective
  have hinj : Function.Injective g' := by sorry
  -- and `f` has only finitely many monic factors
  have hfin : Finite G := by sorry
  -- therefore there are only finitely many intermediate fields
  exact Finite.of_injective g' hinj

and its statement naturally uses IntermediateField. Let me see if I can find a way to convert the statement to your form.

[Kevin Buzzard]

@Thomas Browning do you have any comments?

[Thomas Browning]

I would probably suggest redefining L to go from IntermediateField F E → IntermediateField F E by immediately applying docs#IntermediateField.lift

[Kevin Buzzard]

Right -- this is how you did normal closure, right? Normal closure of K (in F/E) was also in F/E rather than in F/K because it is easier to work with at the end of the day.

[Thomas Browning]

Yes, that's right. Staying within a single intermediate field type just seems to make life easier.

[Junyan Xu]

You just need injectivity of g and you don't need to take the subfield generated by the coefficients of the minimal polynomial: if p := minpoly K α = minpoly K' α (when coerced into E) then the coefficients lies in K ⊓ K', so q := minpoly (K ⊓ K') α divides p. But p has degree [E:K], which is smaller than the degree of q [E:K ⊓ K'], if K ≠ K'.

Given how docs#Ideal.finite_factors is proved, I suppose we don't have a lemma saying a nonzero element in a UFD has only finitely many factors up to associates. Minpolys are monic so g composed with the map E[X] -> Associates E[X] is still injective. (Update: Oh there is docs#UniqueFactorizationMonoid.fintypeSubtypeDvd which can be applied there but not here ...)

[Jz Pan]

Thanks. Now there is only a few sorrys to go.

[Jz Pan]

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

universe u v

open scoped Classical Polynomial

open FiniteDimensional Polynomial IntermediateField

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

variable [Algebra F E] [FiniteDimensional F E]

lemma Field.finite_intermediateField_of_exists_primitive_element.aux_1
    (α : E) (hprim : F⟮α⟯ = ⊤) (K : IntermediateField F E) :
    K⟮α⟯ = ⊤ := by
  sorry

lemma Field.finite_intermediateField_of_exists_primitive_element.aux_2
    (α : E) (hprim : F⟮α⟯ = ⊤) (K K' : IntermediateField F E)
    (heq : (minpoly K α).map (algebraMap K E) = (minpoly K' α).map (algebraMap K' E)) :
    K = K ⊓ K' := by
  set g := (minpoly K α).map (algebraMap K E)
  set g' := (minpoly K' α).map (algebraMap K' E)
  set K'' := K ⊓ K'
  have hcoeff : ∀ n : ℕ, g.coeff n ∈ K'' := fun n =>
    (mem_inf (S := K) (T := K')).2
      ⟨by rw [coeff_map]; exact ((minpoly K α).coeff n).property,
        by rw [heq, coeff_map]; exact ((minpoly K' α).coeff n).property⟩
  let p : Polynomial K'' := g.sum $ fun n _ => C ⟨g.coeff n, hcoeff n⟩ * X ^ n
  have hp : p.map (algebraMap K'' E) = g := by
    sorry
  let q := minpoly K'' α
  obtain ⟨r, hqdvdp⟩ := show q ∣ p by
    apply minpoly.dvd
    rw [aeval_def, eval₂_eq_eval_map, hp, ← eval₂_eq_eval_map, ← aeval_def]
    exact minpoly.aeval K α
  have hpne0 : p ≠ 0 := by
    apply_fun Polynomial.map (algebraMap K'' E)
    rw [hp, Polynomial.map_zero, Polynomial.map_ne_zero_iff $ NoZeroSMulDivisors.algebraMap_injective K E]
    exact minpoly.ne_zero $ isAlgebraic_iff_isIntegral.1 $ isAlgebraic_of_finite K α
  have hqne0 : q ≠ 0 := by rw [hqdvdp] at hpne0; exact left_ne_zero_of_mul hpne0
  have hrne0 : r ≠ 0 := by rw [hqdvdp] at hpne0; exact right_ne_zero_of_mul hpne0
  have hpdeg := IntermediateField.adjoin.finrank (K := K) (x := α) (hx := isIntegral_of_finite K α)
  rw [Field.finite_intermediateField_of_exists_primitive_element.aux_1 F E α hprim K,
    ← Polynomial.natDegree_map_eq_of_injective (NoZeroSMulDivisors.algebraMap_injective K E) (minpoly K α),
    show (minpoly K α).map (algebraMap K E) = g by rfl,
    ← hp,
    Polynomial.natDegree_map_eq_of_injective (NoZeroSMulDivisors.algebraMap_injective K'' E),
    hqdvdp,
    Polynomial.natDegree_mul hqne0 hrne0,
    ← IntermediateField.adjoin.finrank (K := K'') (x := α) (hx := isIntegral_of_finite K'' α),
    Field.finite_intermediateField_of_exists_primitive_element.aux_1 F E α hprim K''] at hpdeg
  -- FiniteDimensional.finrank_mul_finrank
  have h1 : K'' ≤ K := inf_le_left
  have h2 : finrank F K'' ≥ finrank F K := by sorry
  sorry

[Jz Pan]

• The first one is, if E/F is a field extension, α is an element of E such that F⟮α⟯ = E, then for any intermediate field K, we should also have K⟮α⟯ = E. I have no idea using existing API to prove this.
• The second one is, I have a polynomial in E but its coefficients are all come from K''. I just want to extract its coefficients and form a polynomial in K''. I suspect I used wrong API.
• The third one is my attempt to use FiniteDimensional.finrank_mul_finrank. Before it I got

hpdeg: finrank { x // x ∈ K } { x // x ∈ ⊤ } = finrank { x // x ∈ K'' } { x // x ∈ ⊤ } + natDegree r

and I want to transfer it into h2. However, the various spaces in it are expressed in weird and twisted ways.

• The last one is to conclude the result using h1 and h2. I suspect there should be an API for it, but I didn't find it yet.

Any suggestions?

[Jz Pan]

OK, finally there is only one sorry:

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

universe u v

open scoped Classical Polynomial

open FiniteDimensional Polynomial IntermediateField

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

variable [Algebra F E] [FiniteDimensional F E]

lemma Field.finite_intermediateField_of_exists_primitive_element.aux_1
    (S : Set E) (hprim : adjoin F S = ⊤) (K : IntermediateField F E) :
    adjoin K S = ⊤ := by
  apply restrictScalars_injective (K := F) (L' := K) (L := E)
  rw [restrictScalars_top, ← top_le_iff, ← hprim, adjoin_le_iff,
    coe_restrictScalars, ← adjoin_le_iff]

lemma Field.finite_intermediateField_of_exists_primitive_element.aux_2
    (α : E) (hprim : F⟮α⟯ = ⊤) (K K' : IntermediateField F E)
    (heq : (minpoly K α).map (algebraMap K E) = (minpoly K' α).map (algebraMap K' E)) :
    K = K ⊓ K' := by
  set g := (minpoly K α).map (algebraMap K E)
  set g' := (minpoly K' α).map (algebraMap K' E)
  set K'' := K ⊓ K'
  have hcoeff : ∀ n : ℕ, g.coeff n ∈ K'' := fun n =>
    (mem_inf (S := K) (T := K')).2
      ⟨by rw [coeff_map]; exact ((minpoly K α).coeff n).property,
        by rw [heq, coeff_map]; exact ((minpoly K' α).coeff n).property⟩
  let p : Polynomial K'' := Finset.sum g.support fun n => C ⟨g.coeff n, hcoeff n⟩ * X ^ n
  have hp : p.map (algebraMap K'' E) = g := by
    rw [← sum_C_mul_X_pow_eq g, Polynomial.sum_def, Polynomial.map_sum]
    congr
    funext n
    rw [Polynomial.map_mul, Polynomial.map_pow, Polynomial.map_X, Polynomial.map_C]
    congr
  let q := minpoly K'' α
  obtain ⟨r, hqdvdp⟩ := show q ∣ p by
    apply minpoly.dvd
    rw [aeval_def, eval₂_eq_eval_map, hp, ← eval₂_eq_eval_map, ← aeval_def]
    exact minpoly.aeval K α
  have hpne0 : p ≠ 0 := by
    apply_fun Polynomial.map (algebraMap K'' E)
    rw [hp, Polynomial.map_zero, Polynomial.map_ne_zero_iff $ NoZeroSMulDivisors.algebraMap_injective K E]
    exact minpoly.ne_zero $ isAlgebraic_iff_isIntegral.1 $ isAlgebraic_of_finite K α
  have hqne0 : q ≠ 0 := by rw [hqdvdp] at hpne0; exact left_ne_zero_of_mul hpne0
  have hrne0 : r ≠ 0 := by rw [hqdvdp] at hpne0; exact right_ne_zero_of_mul hpne0
  have hpdeg := IntermediateField.adjoin.finrank (K := K) (x := α) (hx := isIntegral_of_finite K α)
  rw [Field.finite_intermediateField_of_exists_primitive_element.aux_1 F E _ hprim K,
    ← Polynomial.natDegree_map_eq_of_injective (NoZeroSMulDivisors.algebraMap_injective K E) (minpoly K α),
    show (minpoly K α).map (algebraMap K E) = g by rfl,
    ← hp,
    Polynomial.natDegree_map_eq_of_injective (NoZeroSMulDivisors.algebraMap_injective K'' E),
    hqdvdp,
    Polynomial.natDegree_mul hqne0 hrne0,
    ← IntermediateField.adjoin.finrank (K := K'') (x := α) (hx := isIntegral_of_finite K'' α),
    Field.finite_intermediateField_of_exists_primitive_element.aux_1 F E _ hprim K''] at hpdeg
  let finrank_K_E : ℕ := ?_
  let finrank_K''_E : ℕ := ?_
  replace hpdeg : finrank_K_E = finrank_K''_E + r.natDegree := by exact hpdeg
  replace hpdeg : finrank_K_E ≥ finrank_K''_E := by linarith only [hpdeg, Nat.le_add_right]
  have h1 : finrank_K_E = finrank K E := by
    sorry
  have h2 : finrank_K''_E = finrank K'' E := by sorry
  exact (eq_of_le_of_finrank_le' inf_le_left $ h1.subst $ h2.subst hpdeg).symm

[Jz Pan]

I need to use the fact that IhtermediateField.restrictScalars does not change finrank. I can't find it in mathlib yet.

Besides, I failed to type the value of finrank_K_E by hand, it's shown as finrank { x // x ∈ K } { x // x ∈ ⊤ } in the infoview, I believe that both of the field are IntermediateField K E, but if I type them manually it doesn't typecheck. So I used the trick mentioned in Terry's thread.

[Jz Pan]

This is the full infoview before the first sorry:

F: Type u
E: Type v
inst✝³: Field F
inst✝²: Field E
inst✝¹: Algebra F E
inst✝: FiniteDimensional F E
α: E
hprim: F⟮α⟯ = ⊤
KK': IntermediateField F E
g: E[X] := Polynomial.map (algebraMap { x // x ∈ K } E) (minpoly { x // x ∈ K } α)
g': E[X] := Polynomial.map (algebraMap { x // x ∈ K' } E) (minpoly { x // x ∈ K' } α)
heq: g = g'
K'': IntermediateField F E := K ⊓ K'
hcoeff: ∀ (n : ℕ), coeff g n ∈ K''
p: { x // x ∈ K'' }[X] := Finset.sum (support g) fun n => ↑C { val := coeff g n, property := (_ : coeff g n ∈ K'') } * X ^ n
hp: Polynomial.map (algebraMap { x // x ∈ K'' } E) p = g
q: { x // x ∈ K'' }[X] := minpoly { x // x ∈ K'' } α
r: { x // x ∈ K'' }[X]
hqdvdp: p = q * r
hpne0: p ≠ 0
hqne0: q ≠ 0
hrne0: r ≠ 0
finrank_K_E: ℕ := finrank { x // x ∈ K } { x // x ∈ ⊤ }
finrank_K''_E: ℕ := finrank { x // x ∈ K'' } { x // x ∈ ⊤ }
hpdeg: finrank_K_E ≥ finrank_K''_E
⊢ finrank_K_E = finrank { x // x ∈ K } E

Do you have any suggestions? Thanks.

[Jz Pan]

Maybe this is sort of MWE:

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

universe u v

open scoped Classical Polynomial

open FiniteDimensional Polynomial IntermediateField

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

variable [Algebra F E] [FiniteDimensional F E]

lemma test (K : IntermediateField F E) (L : IntermediateField K E) :
    True := by
  let m := finrank F K -- OK
  let n := finrank K L -- does not typecheck
  /-
  failed to synthesize
    Module { x // x ∈ K } { x // x ∈ L }
  (deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)
  -/
  sorry

I assume that the finrank { x // x ∈ K } { x // x ∈ ⊤ } is a special case of finrank K L, but it turns out that finrank K L does not typecheck at all. The problem reduced to the very beginning of the thread. :(

[Jz Pan]

This is also not working:

  let K₁ : ?_ := ?_
  let E₁ : ?_ := ?_
  let K''₂ : ?_ := ?_
  let E₂ : ?_ := ?_
  replace hpdeg : finrank K₁ E₁ = finrank K''₂ E₂ + r.natDegree := by exact hpdeg

/-
failed to synthesize
  Module { x // x ∈ K } { x // x ∈ ⊤ }
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)

failed to synthesize
  Module { x // x ∈ K'' } { x // x ∈ ⊤ }
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)

application type mismatch
  @finrank { x // x ∈ K'' } E₂
argument
  E₂
has type
  ?intro.refine_3.refine_3.refine_3.refine_1 : Sort ?u.49665
but is expected to have type
  Type v : Type (v + 1)
-/

[Kevin Buzzard]

This is slightly surprising because at the end of the day you have a completely symmetric situation: you have inst : FiniteDimensional F E and K : IntermediateField F E and then finrank F K works, but you also have inst : FiniteDimensional K E (typeclass inference can find this) and L : IntermediateField K E but finrank K L fails. You say it does not typecheck but this is incorrect really, typeclass inference is timing out as opposed to a typechecking failure.

[Eric Wieser]

This works:

  let m := finrank F K -- OK
  -- these are both instances anyway, but it takes too long for lean to find them
  letI : Algebra K L := IntermediateField.algebra _
  letI : Module K L := Algebra.toModule
  let n := finrank K L -- OK

[Kevin Buzzard]

This doesn't:

lemma test (K : IntermediateField F E) (L : IntermediateField K E) :
    True := by
  let erm : AddCommMonoid L := inferInstance -- deterministic timeout

[Kevin Buzzard]

I am more horrified than amused by this :shock:

[Eric Wieser]

I think we already saw this a bunch when porting for the simpler case of L : Subalgebra R A

[Kevin Buzzard]

import Mathlib.FieldTheory.IntermediateField

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

variable [Algebra F E]

set_option synthInstance.maxHeartbeats 40000 in -- fails without this bump
instance (K : IntermediateField F E) (L : IntermediateField K E) : AddCommMonoid L := inferInstance

We can't even prove that an intermediate field is an AddCommMonoid without bumping heartbeats??

[Kevin Buzzard]

@Jz Pan can you just stick with everything being IntermediateField F E and have a hypothesis K <= L?

[Kevin Buzzard]

   [] ✅ apply @OrderedCancelAddCommMonoid.toAddCommMonoid to AddCommMonoid { x // x ∈ L }

That is such a costly mistake. There are so many ways to prove that something has an order and they're all taking 0.1 or more seconds to fail.

[Jz Pan]

Kevin Buzzard said:

Jz Pan can you just stick with everything being IntermediateField F E and have a hypothesis K <= L?

Currently I haven't find a way to do it yet. I think of several methods, bu they eventually they involve IntermediateField of IntermediateField. More specifically, it comes from IntermediateField.adjoin.finrank.

[Jz Pan]

Eric Wieser said:

This works:

  let m := finrank F K -- OK
  -- these are both instances anyway, but it takes too long for lean to find them
  letI : Algebra K L := IntermediateField.algebra _
  letI : Module K L := Algebra.toModule
  let n := finrank K L -- OK

Thanks, it works! At least I can write down a fake result which can be used in rw:

lemma test (K : IntermediateField F E) (L : IntermediateField K E) :
    haveI : Algebra K L := IntermediateField.algebra _
    haveI : Module K L := Algebra.toModule
    finrank K L = 42 := by
  sorry

-- ......

  have h1 : finrank_K_E = 42 := by
    exact test F E K _

Next step is to write down the correct version of the lemma (probably involving IntermediateField.restrictScalars) and then the whole proof is sorry-free.

[Matthew Ballard]

Kevin Buzzard said:

import Mathlib.FieldTheory.IntermediateField

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

variable [Algebra F E]

set_option synthInstance.maxHeartbeats 40000 in -- fails without this bump
instance (K : IntermediateField F E) (L : IntermediateField K E) : AddCommMonoid L := inferInstance

We can't even prove that an intermediate field is an AddCommMonoid without bumping heartbeats??

lean4#2478

[Jz Pan]

OK this is the last lemma I need to prove:

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

universe u v

open scoped Classical Polynomial

open FiniteDimensional Polynomial IntermediateField

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

variable [Algebra F E] [FiniteDimensional F E]

lemma test (K : IntermediateField F E) :
    haveI : Algebra K (⊤ : IntermediateField K E) := IntermediateField.algebra _
    haveI : Module K (⊤ : IntermediateField K E) := Algebra.toModule
    finrank K (⊤ : IntermediateField K E) = finrank K E := by
  sorry

It looks trivial but I'm not familiar with the finrank API yet.
Let's see if I can find a way to prove it.

[Eric Wieser]

I would guess docs#LinearEquiv.finrank_eq is what you need

[Jz Pan]

Junyan Xu said:

Given how docs#Ideal.finite_factors is proved, I suppose we don't have a lemma saying a nonzero element in a UFD has only finitely many factors up to associates. Minpolys are monic so g composed with the map E[X] -> Associates E[X] is still injective. (Update: Oh there is docs#UniqueFactorizationMonoid.fintypeSubtypeDvd which can be applied there but not here ...)

I think this should be easy to prove.

[Jz Pan]

In fact I suspect that in a Noetherian integral domain, any non-zero element has only finitely many factors up to unit (namely, any non-zero principal ideal is contained in finitely many principal ideals); maybe this is related to Krull's principal ideal theorem. I can't find a proof yet, though.

[Kevin Buzzard]

These are called finite factorization domains and there are examples of Noetherian IDs which are not finite factorization domains -- for example the subring of $\mathbb{C}[X]$ consisting of polynomials with real constant term is not an FFD because $zX$ divides $X^2$ for all non-zero complex $z$, but the units are only the non-zero reals.

[Jz Pan]

OK let's stick to UFD then.
Or is it true for Noetherian integrally closed domain? Your example is not integrally closed.

[Jz Pan]

Eric Wieser said:

I would guess docs#LinearEquiv.finrank_eq is what you need

Thanks, I'm trying. Meanwhile I found that I have to use letI instead of haveI otherwise Lean complains that two instances are not equal.

[Jz Pan]

I'm almost done (by a naive way) except for a map_smul':

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

universe u v

open scoped Classical Polynomial

open FiniteDimensional Polynomial IntermediateField

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

variable [Algebra F E] [FiniteDimensional F E]

lemma test (K : IntermediateField F E) :
    letI : Algebra K (⊤ : IntermediateField K E) := IntermediateField.algebra _
    letI : Module K (⊤ : IntermediateField K E) := Algebra.toModule
    finrank K (⊤ : IntermediateField K E) = finrank K E := by
  letI : Algebra K (⊤ : IntermediateField K E) := IntermediateField.algebra _
  letI : Module K (⊤ : IntermediateField K E) := Algebra.toModule
  apply LinearEquiv.finrank_eq
  let f : (⊤ : IntermediateField K E) → E := fun x => x.1
  let g : E → (⊤ : IntermediateField K E) := fun x => ⟨x, mem_top⟩
  exact {
    toFun := f,
    map_add' := fun x y => by simp only [top_toSubalgebra, Subsemiring.coe_add,
      Algebra.top_toSubsemiring, Subsemiring.coe_top],
    map_smul' := fun r x => by
      simp only [AddHom.toFun]
      simp
      sorry,
    invFun := g,
    left_inv := fun x => by simp only,
    right_inv := fun x => by simp only,
  }

At the second simp it is said that

failed to synthesize
  SMul { x // x ∈ K } { x // x ∈ K }
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)

I have no idea how to fix it. Perhaps I should use an algebra map from an IntermediateField K E to E provided in mathlib? Are there any?

[Jz Pan]

The thing I tried to prove is

r: { x // x ∈ K }
x: { x // x ∈ ⊤ }
⊢ ↑(r • x) = ↑(RingHom.id { x // x ∈ K }) r • ↑x

[Kevin Buzzard]

Jz Pan said:

OK let's stick to UFD then.
Or is it true for Noetherian integrally closed domain? Your example is not integrally closed.

Yes, my memory is that integrally closed Noetherian IDs are FFDs but I don't know a proof (it might not be hard, I just don't have time to think right now)

[Jz Pan]

Finally I use this:

lemma Field.finite_intermediateField_of_exists_primitive_element.aux_finrank
    (K : IntermediateField F E) :
    letI : Algebra K (⊤ : IntermediateField K E) := IntermediateField.algebra _
    letI : Module K (⊤ : IntermediateField K E) := Algebra.toModule
    finrank K (⊤ : IntermediateField K E) = finrank K E := by
  letI : Algebra K (⊤ : IntermediateField K E) := IntermediateField.algebra _
  letI : Module K (⊤ : IntermediateField K E) := Algebra.toModule
  apply LinearEquiv.finrank_eq
  exact {
    toFun := fun x => x.1,
    map_add' := fun x y => by simp only [IntermediateField.coe_add],
    map_smul' := fun r x => by
      simp only [AddHom.toFun, RingHom.id_apply]
      letI : SMul K K := Algebra.toSMul (self := Algebra.id K)
      letI : IsScalarTower K K E := IsScalarTower.left K
      exact IntermediateField.coe_smul (⊤ : IntermediateField K E) r x,
    invFun := fun x => ⟨x, mem_top⟩,
    left_inv := fun x => by simp only,
    right_inv := fun x => by simp only,
  }

and the whole proof is sorry-free.

[Jz Pan]

As for the finiteness of the monic factors, I use this:

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

universe u v

open scoped Classical Polynomial

open FiniteDimensional Polynomial IntermediateField

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

variable [Algebra F E] [FiniteDimensional F E]

lemma Field.finite_intermediateField_of_exists_primitive_element.aux_fin
    (f : Polynomial E) (h : f ≠ 0) :
    Finite { g : Polynomial E // g.Monic ∧ g ∣ f } := by
  set G := { g : Polynomial E // g.Monic ∧ g ∣ f }
  let y : Associates $ Polynomial E := Associates.mk f
  have hy : y ≠ 0 := Associates.mk_ne_zero.mpr h
  let H := { x : Associates $ Polynomial E // x ∣ y }
  have hfin : Finite H := @Finite.of_fintype _ $ UniqueFactorizationMonoid.fintypeSubtypeDvd y hy
  let i : G → H := fun x => ⟨Associates.mk x.1, Associates.mk_dvd_mk.2 x.2.2⟩
  have hinj : Function.Injective i := fun x y heq => by
    rw [Subtype.mk.injEq, Associates.mk_eq_mk_iff_associated] at heq
    obtain ⟨z, h⟩ := heq
    obtain ⟨c, ⟨_, h2⟩⟩ := Polynomial.isUnit_iff.1 (Units.isUnit z)
    have h' := congr_arg Polynomial.leadingCoeff h
    rw [mul_comm, Polynomial.leadingCoeff_mul_monic x.2.1, y.2.1,
      ← h2, Polynomial.leadingCoeff_C] at h'
    rw [← h2, h', map_one, mul_one] at h
    rwa [Subtype.mk.injEq]
  exact Finite.of_injective i hinj

[Eric Rodriguez]

Jz Pan said:

Finally I use this:

lemma Field.finite_intermediateField_of_exists_primitive_element.aux_finrank
    (K : IntermediateField F E) :
    letI : Algebra K (⊤ : IntermediateField K E) := IntermediateField.algebra _
    letI : Module K (⊤ : IntermediateField K E) := Algebra.toModule
    finrank K (⊤ : IntermediateField K E) = finrank K E := by
  letI : Algebra K (⊤ : IntermediateField K E) := IntermediateField.algebra _
  letI : Module K (⊤ : IntermediateField K E) := Algebra.toModule
  apply LinearEquiv.finrank_eq
  exact {
    toFun := fun x => x.1,
    map_add' := fun x y => by simp only [IntermediateField.coe_add],
    map_smul' := fun r x => by
      simp only [AddHom.toFun, RingHom.id_apply]
      letI : SMul K K := Algebra.toSMul (self := Algebra.id K)
      letI : IsScalarTower K K E := IsScalarTower.left K
      exact IntermediateField.coe_smul (⊤ : IntermediateField K E) r x,
    invFun := fun x => ⟨x, mem_top⟩,
    left_inv := fun x => by simp only,
    right_inv := fun x => by simp only,
  }

and the whole proof is sorry-free.

@loogle (Top.top : IntermediateField _ _)

[loogle]

Failure! Bot is unavailable

[Eric Rodriguez]

OK, docs#IntermediateField.topEquiv saves you from having to write all that

[Eric Wieser]

loogle said:

Failure! Bot is unavailable

But you asked for Top...?

[Eric Wieser]

@loogle finrank, Top.top

[loogle]

:exclamation: unknown identifier 'finrank'
Did you mean FiniteDimensional.finrank, Top.top or something else?

[Eric Wieser]

exact finrank_top should work too

[Jz Pan]

Thank you very much. Both of them works:

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

universe u v

open scoped Classical Polynomial

open FiniteDimensional Polynomial IntermediateField

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

variable [Algebra F E] [FiniteDimensional F E]

lemma Field.finite_intermediateField_of_exists_primitive_element.aux_finrank
    (K : IntermediateField F E) :
    letI : Algebra K (⊤ : IntermediateField K E) := IntermediateField.algebra _
    letI : Module K (⊤ : IntermediateField K E) := Algebra.toModule
    finrank K (⊤ : IntermediateField K E) = finrank K E := by
  letI : Algebra K (⊤ : IntermediateField K E) := IntermediateField.algebra _
  letI : Module K (⊤ : IntermediateField K E) := Algebra.toModule
  exact finrank_top K E
  -- exact LinearEquiv.finrank_eq $ (IntermediateField.topEquiv (F := K) (E := E)).toLinearEquiv

Interestingly, I remembered that I have tried finrank_top before, but it didn't work at that time.

[Jz Pan]

I'm stuck again :(

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

open scoped Classical Polynomial

open FiniteDimensional Polynomial IntermediateField

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

variable [Algebra F E]

namespace Field

example (halg : Algebra.IsAlgebraic F E) (S : Set E) [Finite S] :
    FiniteDimensional F (adjoin F S) := by
  let t : S → IntermediateField F E := fun x ↦ F⟮x.1⟯
  have h : ∀ x : S, FiniteDimensional F (t x) := fun x ↦
    adjoin.finiteDimensional <| isAlgebraic_iff_isIntegral.1 (halg x.1)
  have := finiteDimensional_iSup_of_finite (t := t)
  sorry

example (S T : Set E) : adjoin F S ⊔ adjoin F T = adjoin F (S ∪ T) := by
  sorry

end Field

I need $F(S)=\prod_{x\in S}F(x)$ but I can't find it in mathlib. In fact I even can't find $F(S)F(T)=F(S\cup T)$.

[Junyan Xu]

Yeah, the second sorry is apparently missing but should be easy from antisymmetry. The first example shouldn't be hard from docs#Set.Finite.induction_on and docs#IntermediateField.finiteDimensional_sup.

[Thomas Browning]

This also follows from docs#IntermediateField.gc

example (S T : Set E) : adjoin F S ⊔ adjoin F T = adjoin F (S ∪ T) :=
  gc.l_sup.symm

[Jz Pan]

Thanks. It's weird that exact? doesn't work for the second example. So probably I can also use gc.l_iSup for the first example.

[Jz Pan]

OK this works:

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

open scoped Classical Polynomial

open FiniteDimensional Polynomial IntermediateField

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

variable [Algebra F E]

namespace Field

example (halg : Algebra.IsAlgebraic F E) (S : Set E) [Finite S] :
    FiniteDimensional F (adjoin F S) := by
  let t : S → IntermediateField F E := fun x ↦ F⟮x.1⟯
  have h : ∀ x : S, FiniteDimensional F (t x) := fun x ↦
    adjoin.finiteDimensional <| isAlgebraic_iff_isIntegral.1 (halg x.1)
  have hfin := finiteDimensional_iSup_of_finite (t := t)
  have := (gc (F := F) (E := E)).l_iSup (f := fun (x : S) ↦ {x.1})
  simp only [Set.iSup_eq_iUnion, Set.iUnion_singleton_eq_range, Subtype.range_coe_subtype,
    Set.setOf_mem_eq] at this
  rwa [← this] at hfin

example (S T : Set E) : adjoin F S ⊔ adjoin F T = adjoin F (S ∪ T) := by
  exact gc.l_sup.symm

end Field