FROBENIUS: descent of char poly from B to A

[kbuzzard]

For the mathematical background, see the blueprint.

We have a ring hom A -> B with image the G-fixed elements, and a polynomial in B[X] which is G-stable descends back to A[X]; furthermore any nice properties (in particular, being monic of degree |G| and having b as as root) also descend.

Right now in the Lean I attempt to do this in quite a bad way, writing down a set-theoretic section from B to A and applying it to the polynomial. @morrison-daniel has suggested a better way here so the argument should be refactored to use his definition of M. This will make things much easier.

[kbuzzard]

The thorems were proved by Ruben van de Velde without the refactor.

[kbuzzard]

Frobenius elements are now on their way to mathlib in leanprover-community/mathlib4#17717 and in particular the sorry corresponding to this task is filled. Hence this task can be considered completed.