feat(RingTheory/Ideal): restriction maps on decomposition and inertia groups in a Galois tower#36544
feat(RingTheory/Ideal): restriction maps on decomposition and inertia groups in a Galois tower#36544xroblot wants to merge 2 commits intoleanprover-community:masterfrom
Conversation
PR summary 55217bd0cdImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
|
Can you please fix the conflict? |
| `AlgEquiv.restrictNormalHom F : Gal(L/K) →* Gal(F/K)`. | ||
| -/ | ||
| @[simps! apply_coe] | ||
| noncomputable def stabilizerMapOfLiesOver : |
There was a problem hiding this comment.
I may be wrong, but we now have Gal(A/B): do we really need to introduce all these fields? The notation is becoming a nightmare.
I understand we want more flexibility, but if we completely remove fields from the statement then in proofs we can just use the fraction field (where hopefully instances are easy to provide).
There was a problem hiding this comment.
As you know, the main application I have in mind is for number fields, where K is not defeq to FractionRing (𝓞 K), so removing the fields from the statements would make things very painful in practice. I agree though that the number of hypotheses is becoming unwieldy and I don't have a good solution for this.
There was a problem hiding this comment.
I mean, remove any mention to the field from statements, using the Galois group Gal(A/B).
There was a problem hiding this comment.
Oh, I see. But in this case, it would be very helpful to have a ring version of AlgEquiv.restrictNormalHom. I thought we had something like that but I cannot find it anymore.
There was a problem hiding this comment.
Yeah, would be good to add an analogue of this for rings (or, better yet, generalize to rings?)
4 participants
Adds a new file
Mathlib/RingTheory/Ideal/Galois.leanwith results on the action ofGal(L/K)on ideals of a ringB ⊆ Lfor a Galois subextensionF/KofL/K. The main results are the surjectivity and kernel descriptions of the natural maps from the decomposition (resp. inertia) group ofPinGal(L/K)to the decomposition (resp. inertia) group ofpinGal(F/K), induced by restriction.