kernel hangs on a proof

Stream: mathlib4

[Junyan Xu]

When Lean attempts to compile the proof nonempty_algHom_of_exists_roots here, the yellow bar (see screenshot) never disappears. However if you comment out the line starting with refine (DFunLike.congr_fun then it disappears quickly. This line makes use of somewhat convoluted defeq, and I wonder if the Lean kernel enters some loop when typechecking, even though the tactic mode accepts the proof.
image.png

Indeed, after a long time, the error messages say

Isaacs.lean:38:8
(kernel) deterministic timeout
Isaacs.lean:73:8
(kernel) deterministic timeout

[Johan Commelin]

I haven't gotten to the bottom of this, but I'll just record here that

    generalize_proofs pf₁ pf₂ at hω
    set x := AdjoinSimple.gen F α.1
    have := DFunLike.congr_fun hω <| AdjoinSimple.gen F α.1
    dsimp only [AlgHom.coe_comp, Function.comp_apply] at this
    have aux : (inclusion pf₂) (AdjoinSimple.gen F α.1) = α := rfl
    rw [aux] at this
    rw [this] --fails

shows that there are some implicit vars that are not lining up.

[Johan Commelin]

If you turn on pp.all, then the expression for M fills ~10 pages on my large desktop monitor... :scream:

[Junyan Xu]

Thanks! I'll probably extract an existential statement for my proof (SplittingField is probably too complicated), and on the other hand try to minimize this slow-rfl (?) example.

[Johan Commelin]

I managed to get a sorry-free proof that the kernel accepts:

variable {F E K K' FS : Type*} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K]
variable [alg : Algebra.IsAlgebraic F E]
variable [Field K'] [Algebra K K']
variable [Algebra F K'] [IsScalarTower F K K']
variable [Field FS] [Algebra F FS] [Algebra FS E]

theorem foobar (h : ∀ (x : E), ∃ y : K, (aeval y) (minpoly F x) = 0) (S : Finset E)
    (p : Polynomial K) (hp : p = Polynomial.map (algebraMap F K) (S.prod (minpoly F)))
    [IsSplittingField K K' p] (α : FS) (hα : F⟮algebraMap FS E α⟯ ≤ adjoin F (S : Set E))
    [Algebra FS (adjoin F (S : Set E))]
    [IsScalarTower F FS (adjoin F (S : Set E))]
    [IsScalarTower FS (adjoin F (S : Set E)) E]
    :
    ∃ ω : FS →ₐ[F] K', α ∈ comap ω (restrictScalars F (⊥ : IntermediateField K K')) := by
  have splits s (hs : s ∈ S) : (minpoly F s).Splits (algebraMap F K') := by
    subst p
    set p := Polynomial.map (algebraMap F K) (S.prod (minpoly F))
    have := splits_of_splits_of_dvd _
      (Finset.prod_ne_zero_iff.mpr fun _ _ ↦ minpoly.ne_zero <| (alg.isIntegral).1 _)
      ((splits_map_iff _ _).mp <| IsSplittingField.splits K' p) (Finset.dvd_prod_of_mem _ hs)
    rwa [IsScalarTower.algebraMap_eq F K K']
  set α' := (algebraMap FS E α)
  have ⟨β, hβ⟩ := h α'
  let ϕ : F⟮α'⟯ →ₐ[F] K' := (IsScalarTower.toAlgHom _ _ _).comp ((AdjoinRoot.liftHom _ _ hβ).comp
    (adjoinRootEquivAdjoin F <| (alg.isIntegral).1 _).symm.toAlgHom)
  obtain ⟨ω, hω⟩ :=
    exists_algHom_adjoin_of_splits (fun s hs ↦ ⟨(alg.isIntegral).1 _, splits s hs⟩) ϕ hα
  use ω.comp (IsScalarTower.toAlgHom F FS (adjoin F (S : Set E))), β
  dsimp
  have := DFunLike.congr_fun hω <| AdjoinSimple.gen F α'
  convert this.symm using 1
  · rw [AlgHom.comp_apply, AlgHom.comp_apply, AlgEquiv.coe_algHom,
      adjoinRootEquivAdjoin_symm_apply_gen, AdjoinRoot.liftHom_root, Algebra.ofId_apply,
      IsScalarTower.coe_toAlgHom']
  · simp only [AlgHom.comp_apply]
    congr 1
    ext
    simp only [coe_inclusion, AdjoinSimple.coe_gen]
    show algebraMap (adjoin F (S : Set E)) E _ = α'
    have := IsScalarTower.coe_toAlgHom' F FS (adjoin F (S : Set E))
    erw [this]
    rw [← IsScalarTower.algebraMap_apply]

theorem nonempty_algHom_of_exists_roots (h : ∀ x : E, ∃ y : K, aeval y (minpoly F x) = 0) :
    Nonempty (E →ₐ[F] K) := by
  refine nonempty_algHom_of_exists_lifts_finset
    fun S ↦ ⟨⟨adjoin F S, Nonempty.some ?_⟩, subset_adjoin _ _⟩
  let p := (S.prod <| minpoly F).map (algebraMap F K)
  let K' := SplittingField p
  let K₀ := (⊥ : IntermediateField K K').restrictScalars F
  set FS := adjoin F (S : Set E)
  let Ω := FS →ₐ[F] K'
  have := finiteDimensional_adjoin (S := (S : Set E)) fun _ _ ↦ (alg.isIntegral).1 _
  let M (ω : Ω) := Subalgebra.toSubmodule (K₀.comap ω).toSubalgebra
  have : ⋃ ω : Ω, ↑(M ω) = @Set.univ FS := Set.eq_univ_of_forall fun α ↦ Set.mem_iUnion.mpr <| by
    simp [M, K₀]
    apply foobar (S := S) (p := p) h rfl
    rw [IntermediateField.adjoin_simple_le_iff]
    simp
  have ⟨ω, hω⟩ : ∃ ω : Ω, ⊤ ≤ M ω := by
    cases finite_or_infinite F
    · have ⟨α, hα⟩ := exists_primitive_element_of_finite_bot F FS
      have ⟨ω, hω⟩ := Set.mem_iUnion.mp (this ▸ Set.mem_univ α)
      exact ⟨ω, show ⊤ ≤ K₀.comap ω by rwa [← hα, adjoin_simple_le_iff]⟩
    · simp_rw [top_le_iff, Subspace.exists_eq_top_of_iUnion_eq_univ this]
  exact ⟨((botEquiv K K').toAlgHom.restrictScalars F).comp <|
    ω.codRestrict K₀.toSubalgebra fun x ↦ hω trivial⟩

[Johan Commelin]

But this is pretty awful!

[Junyan Xu]

Thanks! I have some other ideas to try that hopefully work out to give a shorter/nicer proof. Isaacs' original argument uses AlgebraicClosure, which I replaced with SplittingField. In the branch I also avoided the dependency of PrimitiveElements on AlgebraicClosure. This means this theorem can be used to simplify the construction of AlgebraicClosure, showing adjoining roots of all polynomials once is enough, and there's no need to repeat this countably many times (see Conrad, and cc @Thomas Browning). I'll surely PR Isaacs' theorem to mathlib, but I'm not sure whether to implement this simplification, it will probably mean introducing more dependency into AlgebraicClosure.
image.png

[Johan Commelin]

I managed to squeeze that last ugly bit if foobar down to

  · simp only [AlgHom.comp_apply]
    congr 1
    ext
    simp only [coe_inclusion, AdjoinSimple.coe_gen, α',
      IsScalarTower.algebraMap_apply FS (adjoin F (S : Set E)) E]
    rfl

[Johan Commelin]

But we shouldn't need to fight like this

[Junyan Xu]

Okay I minimized it.

import Mathlib.FieldTheory.Adjoin

variable {F E} [Field F] [Field E] [Algebra F E]

open IntermediateField

lemma no_timeout (FS : IntermediateField F E) (α : FS) :
    inclusion (adjoin_simple_le_iff.mpr α.2) (AdjoinSimple.gen F α.1) = α :=
  rfl

lemma no_timeout' (S : Set E) (α : adjoin F S) :
    inclusion (adjoin_simple_le_iff.mpr α.2) (AdjoinSimple.gen F α.1) = α :=
  no_timeout _ _

lemma no_timeout'' (S : Set E) (α : adjoin F S) :
    inclusion (adjoin_simple_le_iff.mpr α.2) (AdjoinSimple.gen F α.1) = α := by
  cases α; rfl

lemma kernel_timeout (S : Set E) (α : adjoin F S) :
    inclusion (adjoin_simple_le_iff.mpr α.2) (AdjoinSimple.gen F α.1) = α :=
  rfl

I bet this is connected to eta reduction of Subtype.
The peak memory is over 16000MB on my machine (I need to check whether this is for the full proof or the extracted lemma kernel_timeout). (Update: no need of aux lemma, just destruct α.)

[Junyan Xu]

Pushed a proof that the kernel accepts and it becomes 3 lines longer than my original.

[Junyan Xu]

Johan Commelin said:

generalize_proofs pf₁ pf₂ at hω
    set x := AdjoinSimple.gen F α.1
    have := DFunLike.congr_fun hω <| AdjoinSimple.gen F α.1
    dsimp only [AlgHom.coe_comp, Function.comp_apply] at this
    have aux : (inclusion pf₂) (AdjoinSimple.gen F α.1) = α := rfl
    rw [aux] at this
    rw [this] --fails

Does this piece of code come directly after have ⟨ω, hω⟩? What's the goal that you attempt to rw [this]?

[Thomas Browning]

@Junyan Xu Does this mean that you have a construction of AlgebraicClosure that bypasses splitting fields? That would be nice since it would give a more direct construction of splitting fields.

[Johan Commelin]

@Junyan Xu Thanks for minimizing this!

[Johan Commelin]

@Junyan Xu That code snippet went between the two refines on L59/60 (if I remember correctly).

[Junyan Xu]

@Thomas Browning No, my proof of Isaacs' theorem still uses splitting fields. The theorem can be used to show docs#AlgebraicClosure.AdjoinMonic is already an algebraic closure and there's no need of docs#AlgebraicClosure.Step or taking DirectLimit. The construction without using splitting field is another one (I claimed there are some defeqs of the data fields that need to be fixed, but now I no longer see what are necessary). Sorry, by reading the thread again I realized that we want to make SplittingField depend on AlgebraicClosure, not the other way around, and it's the construction of SplittingField that we'd like to simplify. I'll port the that construction to Lean 4 sometime.

[Junyan Xu]

The PR on Isaacs' theorem is #18412