!4#5159 FieldTheory.PolynomialGaloisGroup

Stream: mathlib4

[Xavier Roblot]

There seems to be a diamond for IsScalarTower ℚ ℝ ℂ. Here is a #mwe coming from the port of #5159

import Mathlib.Algebra.Algebra.Tower
import Mathlib.Data.Complex.Module

example := AlgEquiv.restrictScalars ℚ Complex.conjAe  -- failed to synthesize instance  IsScalarTower ℚ ℝ ℂ

Lean wants

@IsScalarTower ℚ ℝ ℂ Algebra.toSMul Algebra.toSMul Algebra.toSMul

but the inferred instances are either docs#Complex.instIsScalarTowerComplexInstSMulComplexInstSMulComplex giving

@IsScalarTower ℚ ℝ ℂ Algebra.toSMul Complex.instSMulComplex Complex.instSMulComplex

or docs#IsScalarTower.rat giving

@IsScalarTower ℚ ℝ ℂ SMulZeroClass.toSMul SMulZeroClass.toSMul SMulZeroClass.toSMul

I tried to find out which instance was giving the term

@IsScalarTower ℚ ℝ ℂ Algebra.toSMul Algebra.toSMul Algebra.toSMul

but I was unsuccessful.

[Riccardo Brasca]

I think docs#instIsScalarTowerComplexInstSMulComplexInstSMulComplex and docs#IsScalarTower.rat give exactly the same term

[Riccardo Brasca]

I mean, syntactically

[Riccardo Brasca]

That is

@IsScalarTower ℚ ℝ ℂ
  (@Algebra.toSMul ℚ ℝ Rat.commSemiring Real.semiring
    (@algebraRat ℝ Real.instDivisionRingReal
      (_ :
        @CharZero ℝ
          (@AddCommMonoidWithOne.toAddMonoidWithOne ℝ
            (@NonAssocSemiring.toAddCommMonoidWithOne ℝ
              (@Semiring.toNonAssocSemiring ℝ (@StrictOrderedSemiring.toSemiring ℝ Real.strictOrderedSemiring)))))))
  (@Complex.instSMulComplex ℝ
    (@Algebra.toSMul ℝ ℝ Real.instCommSemiringReal Real.semiring (@Algebra.id ℝ Real.instCommSemiringReal)))
  (@Complex.instSMulComplex ℚ
    (@Algebra.toSMul ℚ ℝ Rat.commSemiring Real.semiring
      (@algebraRat ℝ Real.instDivisionRingReal
        (_ :
          @CharZero ℝ
            (@AddCommMonoidWithOne.toAddMonoidWithOne ℝ
              (@NonAssocSemiring.toAddCommMonoidWithOne ℝ
                (@Semiring.toNonAssocSemiring ℝ (@StrictOrderedSemiring.toSemiring ℝ Real.strictOrderedSemiring))))))))

[Riccardo Brasca]

Lean wants

@IsScalarTower ℚ ℝ ℂ
  (@Algebra.toSMul ℚ ℝ Rat.commSemiring (@CommSemiring.toSemiring ℝ Real.instCommSemiringReal)
    (@algebraRat ℝ Real.instDivisionRingReal
      (_ :
        @CharZero ℝ
          (@AddCommMonoidWithOne.toAddMonoidWithOne ℝ
            (@NonAssocSemiring.toAddCommMonoidWithOne ℝ
              (@Semiring.toNonAssocSemiring ℝ (@StrictOrderedSemiring.toSemiring ℝ Real.strictOrderedSemiring)))))))
  (@Algebra.toSMul ℝ ℂ Real.instCommSemiringReal Complex.instSemiringComplex
    (@Complex.instAlgebraComplexInstSemiringComplex ℝ Real.instCommSemiringReal
      (@Algebra.id ℝ Real.instCommSemiringReal)))
  (@Algebra.toSMul ℚ ℂ Rat.commSemiring Complex.instSemiringComplex
    (@algebraRat ℂ (@Field.toDivisionRing ℂ Complex.instFieldComplex) Complex.charZero))

[Riccardo Brasca]

It looks like again the CharZero diamond, if I convert the instance the goal is

@Eq (SMul ℚ ℂ)
  (@Algebra.toSMul ℚ ℂ Rat.commSemiring Complex.instSemiringComplex
    (@algebraRat ℂ (@Field.toDivisionRing ℂ Complex.instFieldComplex) Complex.charZero))
  (@Complex.instSMulComplex ℚ
    (@Algebra.toSMul ℚ ℝ Rat.commSemiring Real.semiring
      (@algebraRat ℝ Real.instDivisionRingReal
        (_ :
          @CharZero ℝ
            (@AddCommMonoidWithOne.toAddMonoidWithOne ℝ
              (@NonAssocSemiring.toAddCommMonoidWithOne ℝ
                (@Semiring.toNonAssocSemiring ℝ (@StrictOrderedSemiring.toSemiring ℝ Real.strictOrderedSemiring))))))))

[Riccardo Brasca]

No sorry, it's not exactly that one. In any case this is the diamond

import Mathlib.Data.Complex.Module

example : (Complex.instSMulComplex : SMul ℚ ℂ) = (Algebra.toSMul : SMul ℚ ℂ) := rfl --fails

[Anne Baanen]

The CharZero diamond should be fixable by giving the right qsmul field to docs#Complex.instFieldComplex.

[Riccardo Brasca]

Let me try this

[Chris Hughes]

I'm just about to open a PR myself

[Riccardo Brasca]

OK, I can review it then :D

[Xavier Roblot]

But why is it working in mathlib3 but not in mathlib4?

[Chris Hughes]

It doesn't work in mathlib3 either

[Chris Hughes]

I guess the file field_theory.polynomial_galois_group works because of some accident about which instance it finds first somewhere.

[Xavier Roblot]

I don't understand. This works:

import data.complex.module

example : (complex.has_smul : has_smul ℚ ℂ) = (algebra.to_has_smul : has_smul ℚ ℂ) := rfl

Am I missing something?

[Chris Hughes]

It works at the end of the file data.complex.module, but not if you put that line directly after the has_smul instance.

[Chris Hughes]

It works before the algebra instance on line 95 in that file, but not after, to be precise.