feat: InfiniteGalois.normalAutEquivQuotient (leanprover-community#32372)

If `H` is a _closed_ normal subgroup of `Gal(K / k)`, then `Gal(fixedField H / k)` is isomorphic to `Gal(K / k) ⧸ H`.

Co-authored-by: bwangpj <70694994+bwangpj@users.noreply.github.com>

Author: bwangpj

Mathlib/FieldTheory/Galois/Infinite.lean

@@ -220,6 +220,21 @@ def GaloisCoinsertionIntermediateFieldSubgroup [IsGalois k K] :
   u_l_le K := le_of_eq (fixedField_fixingSubgroup K)
   choice_eq _ _ := rfl
 
+open IntermediateField in
+/-- If `H` is a closed normal subgroup of `Gal(K / k)`,
+then `Gal(fixedField H / k)` is isomorphic to `Gal(K / k) ⧸ H`. -/
+noncomputable def normalAutEquivQuotient [IsGalois k K]
+    (H : ClosedSubgroup Gal(K/k)) [H.Normal] :
+    Gal(K/k) ⧸ H.1 ≃* Gal(fixedField H.1/k) :=
+  (QuotientGroup.quotientMulEquivOfEq ((fixingSubgroup_fixedField H).symm.trans
+    (fixedField H.1).restrictNormalHom_ker.symm)).trans <|
+      QuotientGroup.quotientKerEquivOfSurjective _ <| restrictNormalHom_surjective K
+
+open IntermediateField in
+lemma normalAutEquivQuotient_apply [IsGalois k K]
+    (H : ClosedSubgroup Gal(K/k)) [H.Normal] (σ : Gal(K/k)) :
+    normalAutEquivQuotient H σ = restrictNormalHom (fixedField H.1) σ := rfl
+
 open IntermediateField in
 theorem isOpen_iff_finite (L : IntermediateField k K) [IsGalois k K] :
     IsOpen L.fixingSubgroup.carrier ↔ FiniteDimensional k L := by