!4#4856 FieldTheory.Normal

Stream: mathlib4

[Riccardo Brasca]

I will not work on !4#4856 until tomorrow if someone wants to continue.

[Anne Baanen]

I have about 45 minutes to 1 hour to spend on this right now!

[Anne Baanen]

docs#alg_hom.lift_normal uses some weird tricks to use with custom typeclass instances instead of ones that are available in the context. I think I got it ported correctly, but is this really the right way to define this map?

[Riccardo Brasca]

There is a similar problem in FieldTheory.Adjoin... I had to use show_term in mathlib3 to figure out the right morphism

[Riccardo Brasca]

I agree that this not the best way

[Anne Baanen]

Hmm... I need to go now, could you please remind me to make an issue to fix this after the port?

[Riccardo Brasca]

Can you recall me what (_) does? It's almost as good as in Lean3!

[Eric Rodriguez]

Iirc, it leaves a blank without leaving TC to infer them

[Riccardo Brasca]

There is a proof that is

@AlgHom.commutes K₁ E E _ _ _ _ (_) _ _

so someone (probably Lean?) has to fill the (_)... but still the proof works, and if we write _ it doesn't.

[Eric Rodriguez]

I guess this is exactly what Anne means; that instance is only fillable in by unification instead of TC

[Riccardo Brasca]

Aaahhh, I see.

[Riccardo Brasca]

Thanks!

[Scott Morrison]

I fixed a few more steps in !4#4856, but with one sorry to go, feel like I'm stuck.

[Scott Morrison]

There is a proof that used to be filled in by unification, and I can not work out how to restore this behaviour.

[Scott Morrison]

I wanted to work around this for now by just giving the proof again, but apparently I don't know my Galois theory and wasn't sure how to finish.

[Scott Morrison]

If anyone would like to look at this sorry that would be great.

[Scott Morrison]

The goal state there is:

_: IsScalarTower F K L
h: Normal F L
x: K
y: L
hy: y ∈ roots (Polynomial.map (algebraMap F L) (minpoly F x))
⊢ minpoly F x = minpoly F y

And if that sounds wrong, I guess I went wrong a step or two earlier. :-)

[Scott Morrison]

This is currently the "highest" file in all.pdf!

[Thomas Browning]

I've fixed the last sorry, but it was more annoying than I expected

[Riccardo Brasca]

I've fixed the names, it's ready to be reviewed.