Restriction to subextensions in identified separable closures

A field extension identifies its absolute Galois group with the subgroup fixing its image in a separable closure of the base. When normal subextensions in the two separable closures are identified by a compatible ring embedding, restriction to those subextensions commutes with this subgroup identification. This is the finite-level group square used to compare inflation of cocycles with restriction of Galois cohomology classes.

References

• J.-P. Serre, Local Fields, GTM 67 (1979), Chapter X, §5.

theorem TauCeti.restrictNormalHom_equivFixingSubgroup (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (E : IntermediateField K (SeparableClosure K)) [Normal K ↥E] (F : IntermediateField L (SeparableClosure L)) [Normal L ↥F] (ι : ↥E →+* ↥F) (π : Gal(↥F/L) →* Gal(↥E/K)) (hι : ∀ (x : ↥E), (separableClosureRingEquiv K L σ).symm (E.val x) = F.val (ι x)) (hπ : ∀ (g : Gal(↥F/L)) (x : ↥E), ι ((π g) x) = g (ι x)) (g : AbsoluteGaloisGroup L) : π ((AlgEquiv.restrictNormalHom ↥F) g) = (AlgEquiv.restrictNormalHom ↥E) ↑((absoluteGaloisGroupEquivFixingSubgroup K L σ) g)

Restriction to normal subextensions commutes with the identification of absolute Galois groups along a field extension. The ring embedding ι identifies the subextensions inside the two separable closures, and π intertwines their finite-level automorphisms.