!4#5424 FieldTheory.AbelRuffini

Stream: mathlib4

[Jeremy Tan]

!4#5424 There seems to be some sort of diamond issue in a rewrite in induction2:

theorem induction2 {α β γ : solvableByRad F E} (hγ : γ ∈ F⟮α, β⟯) (hα : P α) (hβ : P β) : P γ := by
  let p := minpoly F α
  let q := minpoly F β
  have hpq := Polynomial.splits_of_splits_mul _
    (mul_ne_zero (minpoly.ne_zero (isIntegral α)) (minpoly.ne_zero (isIntegral β)))
    (SplittingField.splits (p * q))
  let f : ↥F⟮α, β⟯ →ₐ[F] (p * q).SplittingField := Classical.choice <| algHom_mk_adjoin_splits (by
    intro x hx
    cases' hx with hx hx
    rw [hx]
    exact ⟨isIntegral α, hpq.1⟩
    cases hx
    exact ⟨isIntegral β, hpq.2⟩)
  have key : minpoly F γ = minpoly F (f ⟨γ, hγ⟩) := by
    refine' minpoly.eq_of_irreducible_of_monic
      (minpoly.irreducible (isIntegral γ)) _ (minpoly.monic (isIntegral γ))
    suffices aeval (⟨γ, hγ⟩ : F⟮α, β⟯) (minpoly F γ) = 0 by
      rw [aeval_algHom_apply, this, AlgHom.map_zero]
    -- Porting note: this instance is needed for the following `apply`
    haveI := @IntermediateField.toAlgebra F (solvableByRad F E) _ _ _ F⟮α, β⟯
      (solvableByRad F E) _ (Algebra.id (solvableByRad F E))
    apply (algebraMap (↥F⟮α, β⟯) (solvableByRad F E)).injective
    haveI alge := Algebra.id (solvableByRad F E)
    haveI modu := alge.toModule
    haveI ist := F⟮α, β⟯.isScalarTower_mid'
    rw [RingHom.map_zero]
    rw [← @aeval_algebraMap_apply _ _ _ _ _ _ _ _ _ ist] -- here
    exact minpoly.aeval F γ
  rw [P, key]
  refine' gal_isSolvable_of_splits ⟨Normal.splits _ (f ⟨γ, hγ⟩)⟩ (gal_mul_isSolvable hα hβ)
  apply SplittingField.instNormal

The error is

application type mismatch
  @aeval_algebraMap_apply F { x // x ∈ F⟮α, β⟯ } { x // x ∈ solvableByRad F E } Semifield.toCommSemiring
    (Subalgebra.toCommSemiring F⟮α, β⟯.toSubalgebra) (Subalgebra.toSemiring (solvableByRad F E).toSubalgebra)
    (algebra F⟮α, β⟯) this (algebra (solvableByRad F E)) ist
argument
  ist
has type
  @IsScalarTower F { x // x ∈ F⟮α, β⟯ } { x // x ∈ solvableByRad F E } Algebra.toSMul
    (Subalgebra.instSMulSubtypeMemSubalgebraInstMembershipInstSetLikeSubalgebra F⟮α, β⟯.toSubalgebra)
    Algebra.toSMul : Prop
but is expected to have type
  @IsScalarTower F { x // x ∈ F⟮α, β⟯ } { x // x ∈ solvableByRad F E } Algebra.toSMul Algebra.toSMul
    Algebra.toSMul : Prop

How can I get the hidden arguments to line up? (note that in mathlib3 ist could be synthed perfectly and it was just rw [← aeval_algebraMap_apply]

[Jeremy Tan]

Also the last exact minpoly.aeval F γ can't close the goal

[Riccardo Brasca]

Having a look

[Riccardo Brasca]

It's fixed.

[Riccardo Brasca]

The problem with exact minpoly.aeval F γ is that the goal is

↑(aeval { val := γ, property := hγ }) (minpoly F γ) = 0

so you are evaluating the minimal polynomial of γ not exactly at γ, but at γ as an element of F⟮α, β⟯, that is a subtype of the type of γ. Of course evaluating a polynomial commutes with the coercion to the original type, and this is what docs#Polynomial.aeval_subalgebra_coe says.