multiplicity of root in extension field

Stream: Is there code for X?

[Kevin Buzzard]

I was happily counting roots and then I ran into this:

import field_theory.splitting_field

open_locale polynomial

open polynomial

variables {K L : Type*} [field K] [field L] (f : K →+* L)
(p : K[X]) (a : K) [decidable_eq K] [decidable_eq L]

example (hp : p \ne 0) (h : eval a p = 0) : root_multiplicity (f a) (p.map f) =
multiset.count a p.roots :=
begin
  sorry
end

It says that if a is a root of p, then the multiplicity of a as a root of p doesn't change when you increase the base field. In general this multiplicity can jump from 0 to positive as the field gets bigger, but if it's already positive then it can't go up any more.

[Junyan Xu]

It can jump from 0 to positive only if a is not in K ... You want a : L right? But then it seems impossible to write down the statement ... Actually, I think it can never jump.

[Junyan Xu]

The jump might refer to the inequality in docs#polynomial.count_map_roots may be a strict equality. But that's because multiset.map ⇑f p.roots doesn't count roots outside of K at all.

[Junyan Xu]

I believe the injective hypothesis can be replaced with p.map f ≠ 0 in both docs#polynomial.le_root_multiplicity_map and docs#polynomial.count_map_roots; with the injectivity hypothesis we ought be be able to prove equalities.

[Junyan Xu]

Anyway, the sorry in the statement as is, can be filled with this new lemma (#14839) together with docs#polynomial.count_roots.

[Kevin Buzzard]

Thank you!

[Junyan Xu]

You're most welcome! I now think docs#polynomial.roots_map_of_injective_card_eq_total_degree can also have the injectivity hypothesis replaced by map f p ≠ 0. My planned proof will use docs#polynomial.C_leading_coeff_mul_prod_multiset_X_sub_C, which is in splitting_field.lean, but I think I can give an easier proof using docs#polynomial.eq_of_monic_of_dvd_of_nat_degree_le, docs#finset.prod_dvd_of_coprime and docs#finset.prod_multiset_count, and the result could then be moved to the end of ring_division.lean. I'll try to carry out the plan tomorrow.

[Kevin Buzzard]

So just to explain what's happening: Maria Ines is pushing for B_{dR} but she still has a few missing proofs. For one argument involving extension of norms to bigger fields she needs to pass to a normal closure. But we have 0 about normal in mathlib -- we have the definition and the "big theorem" (normal iff splitting field for finite extensions). Normal is not used for splitting fields or algebraic closures, and the only reason it's used in Galois theory is in the definition of Galois, which is the usual normal-separable thing. You can define Galois to be "#automorphisms = degree" (it's always <=) and then it seems to me that you can develop the entire fundamental theorem of Galois theory without ever saying the word "normal", and the only bit that you are missing is the bit saying "by the way, the subgroup is normal iff the subfield is normal". This is what the FTG seems to look like in mathlib, I can't find the statements that normal match up and so I'm fiddling around with splitting fields to get a better API for normal and then hopefully I can find someone who can take over :-)

[Riccardo Brasca]

B_{dR}?! That's great!!

[Kevin Buzzard]

Yeah she spoke at London Learning Lean about it earlier this week!

[Kevin Buzzard]

But there's still some missing pieces. The other big one is theta, but that should be do-able.

[Junyan Xu]

I've been able to significantly golf (+51 -138) some proofs in splitting_field.lean at #14862. I think this would not be hard to review! :)

[Johan Commelin]

A golf indeed! Well done :golf: :hole_in_one:

[Junyan Xu]

Second golfing PR #14888 with a few new lemmas. +119 -172 this time :)