feat(FieldTheory/Galois): Lemmas of galois theory

Mathlib/Algebra/Group/Subgroup/Pointwise.lean

@@ -396,6 +396,15 @@ theorem Normal.conjAct {G : Type*} [Group G] {H : Subgroup G} (hH : H.Normal) (g
 theorem smul_normal (g : G) (H : Subgroup G) [h : Normal H] : MulAut.conj g • H = H :=
   h.conjAct g
 
+theorem Normal.of_conjugate_fixed {G : Type*} [Group G] {H : Subgroup G}
+    (h : ∀ g : G, (MulAut.conj g) • H = H) : H.Normal := by
+  constructor
+  intro n hn g
+  rw [← h g, Subgroup.mem_pointwise_smul_iff_inv_smul_mem, ← map_inv, MulAut.smul_def,
+    MulAut.conj_apply, inv_inv, mul_assoc, mul_assoc, inv_mul_cancel, mul_one,
+    ← mul_assoc, inv_mul_cancel, one_mul]
+  exact hn
+
 theorem normalCore_eq_iInf_conjAct (H : Subgroup G) :
     H.normalCore = ⨅ (g : ConjAct G), g • H := by
   ext g

Mathlib/FieldTheory/Galois/Basic.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2020 Thomas Browning, Patrick Lutz. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Thomas Browning, Patrick Lutz
+Authors: Thomas Browning, Patrick Lutz, Yongle Hu, Jingting Wang
 -/
 import Mathlib.FieldTheory.Fixed
 import Mathlib.FieldTheory.NormalClosure
@@ -278,6 +278,77 @@ def galoisCoinsertionIntermediateFieldSubgroup [FiniteDimensional F E] [IsGalois
 
 end IsGalois
 
+section
+
+/-In this section we prove that the normal subgroups correspond to the Galois subextensions
+in the Galois correspondence and its related results.-/
+
+variable {K L : Type*} [Field K] [Field L] [Algebra K L]
+
+open IntermediateField
+
+open scoped Pointwise
+
+lemma AlgEquiv.restrictNormalHomKer (E : IntermediateField K L) [Normal K E]:
+    (restrictNormalHom E).ker = E.fixingSubgroup := by
+  ext σ
+  apply ((((mem_fixingSubgroup_iff (L ≃ₐ[K] L)).trans ⟨fun h ⟨x, hx⟩ ↦ Subtype.val_inj.mp <|
+    (restrictNormal_commutes σ E ⟨x, hx⟩).trans (h x hx) , _⟩).trans
+      AlgEquiv.ext_iff.symm)).symm
+  intro h x hx
+  have hs : ((restrictNormalHom E) σ) ⟨x, hx⟩ = σ • x :=
+    restrictNormal_commutes σ E ⟨x, hx⟩
+  exact hs ▸ (Subtype.val_inj.mpr (h ⟨x, hx⟩))
+
+namespace IsGalois
+
+variable (E : IntermediateField K L)
+
+/-- If `H` is a normal Subgroup of `Gal(L / K)`, then `fixedField H` is Galois over `K`. -/
+instance of_fixedField_normal_subgroup [IsGalois K L]
+    (H : Subgroup (L ≃ₐ[K] L)) [hn : Subgroup.Normal H] : IsGalois K (fixedField H) where
+  to_isSeparable := Algebra.isSeparable_tower_bot_of_isSeparable K (fixedField H) L
+  to_normal := by
+    apply normal_iff_forall_map_le'.mpr
+    rintro σ x ⟨a, ha, rfl⟩ τ
+    exact (symm_apply_eq σ).mp (ha ⟨σ⁻¹ * τ * σ, Subgroup.Normal.conj_mem' hn τ.1 τ.2 σ⟩)
+
+/-- If `H` is a normal Subgroup of `Gal(L / K)`, then `Gal(fixedField H / K)` is isomorphic to
+`Gal(L / K) ⧸ H`. -/
+noncomputable def normalAutEquivQuotient [FiniteDimensional K L] [IsGalois K L]
+    (H : Subgroup (L ≃ₐ[K] L)) [Subgroup.Normal H] :
+    (L ≃ₐ[K] L) ⧸ H ≃* ((fixedField H) ≃ₐ[K] (fixedField H)) :=
+  (QuotientGroup.quotientMulEquivOfEq ((fixingSubgroup_fixedField H).symm.trans
+  (AlgEquiv.restrictNormalHomKer (fixedField H)).symm)).trans <|
+  QuotientGroup.quotientKerEquivOfSurjective (restrictNormalHom (fixedField H)) <|
+  restrictNormalHom_surjective L
+
+open scoped Pointwise
+
+theorem fixingSubgroup_conjugate_of_map (σ : L ≃ₐ[K] L) :
+    (E.map σ).fixingSubgroup = (MulAut.conj σ) • E.fixingSubgroup := by
+  ext τ
+  rw [IntermediateField.fixingSubgroup, mem_fixingSubgroup_iff]
+  have : τ ∈ (MulAut.conj σ) • E.fixingSubgroup ↔ ∀ x : E, σ⁻¹ (τ (σ x)) = x :=
+    Subgroup.mem_pointwise_smul_iff_inv_smul_mem
+  simp only [coe_map, AlgHom.coe_coe, Set.mem_image, SetLike.mem_coe, AlgEquiv.smul_def,
+    forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, this, Subtype.forall]
+  exact ⟨fun h y hy ↦ (h y hy).symm ▸ (σ.left_inv y),
+    fun h y hy ↦ (σ.right_inv (τ (σ y))) ▸ congrArg σ.toFun (h y hy)⟩
+
+/-- Let `E` be an intermediateField of a Galois extension `L / K`. If `E / K` is
+Galois extension, then `E.fixingSubgroup` is a normal subgroup of `Gal(L / K)`. -/
+instance fixingSubgroup_normal_of_isGalois [IsGalois K L] [IsGalois K E] :
+    E.fixingSubgroup.Normal := by
+  apply Subgroup.Normal.of_conjugate_fixed (fun σ ↦ ?_)
+  have : E = ((IntermediateField.map (σ⁻¹ : L ≃ₐ[K] L) E) : IntermediateField K L) :=
+    (IntermediateField.normal_iff_forall_map_eq'.mp inferInstance σ⁻¹).symm
+  nth_rw 1 [this, IsGalois.fixingSubgroup_conjugate_of_map E σ⁻¹, map_inv, smul_inv_smul]
+
+end IsGalois
+
+end
+
 end GaloisCorrespondence
 
 section GaloisEquivalentDefinitions

Mathlib/FieldTheory/IntermediateField/Basic.lean

@@ -551,6 +551,16 @@ theorem mem_lift {F : IntermediateField K L} {E : IntermediateField K F} (x : F)
     x.1 ∈ lift E ↔ x ∈ E :=
   Subtype.val_injective.mem_set_image
 
+/--The algEquiv between an intermediate field and its lift-/
+def lift_algEquiv (E : IntermediateField K L) (F : IntermediateField K E) : ↥F ≃ₐ[K] lift F where
+  toFun x := ⟨x.1.1,(mem_lift x.1).mpr x.2⟩
+  invFun x := ⟨⟨x.1, lift_le F x.2⟩, (mem_lift ⟨x.1, lift_le F x.2⟩).mp x.2⟩
+  left_inv := congrFun rfl
+  right_inv := congrFun rfl
+  map_mul' _ _ := rfl
+  map_add' _ _ := rfl
+  commutes' _ := rfl
+
 section RestrictScalars
 
 variable (K)

Mathlib/FieldTheory/Normal.lean

@@ -283,6 +283,10 @@ theorem AlgEquiv.restrictNormal_trans [Normal F E] :
 def AlgEquiv.restrictNormalHom [Normal F E] : (K₁ ≃ₐ[F] K₁) →* E ≃ₐ[F] E :=
   MonoidHom.mk' (fun χ => χ.restrictNormal E) fun ω χ => χ.restrictNormal_trans ω E
 
+lemma AlgEquiv.restrictNormalHom_apply (L : IntermediateField F K₁) [Normal F L]
+    (σ : (K₁ ≃ₐ[F] K₁)) (x : L) : restrictNormalHom L σ x = σ x :=
+  AlgEquiv.restrictNormal_commutes σ L x
+
 variable (F K₁)
 
 /-- If `K₁/E/F` is a tower of fields with `E/F` normal then `AlgHom.restrictNormal'` is an