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,90 @@ 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
+
+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
+    intro σ x ⟨a, ha, hax⟩ τ
+    rw [← hax]
+    calc _ = (σ * σ⁻¹ * τ.1 * σ) a := by rw [mul_inv_cancel]; rfl
+      _ = _ := by nth_rw 2 [← ha ⟨_ , (Subgroup.Normal.conj_mem hn τ.1 τ.2 σ⁻¹)⟩]; rfl
+
+/-- 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] :
+    ((fixedField H) ≃ₐ[K] (fixedField H)) ≃* (L ≃ₐ[K] L) ⧸ H := by
+  apply MulEquiv.symm <| (QuotientGroup.quotientMulEquivOfEq
+    ((fixingSubgroup_fixedField H).symm.trans _)).trans <|
+    QuotientGroup.quotientKerEquivOfSurjective (restrictNormalHom (fixedField H)) <|
+      restrictNormalHom_surjective L
+  ext σ
+  apply (((mem_fixingSubgroup_iff (L ≃ₐ[K] L)).trans ⟨fun h ⟨x, hx⟩ ↦ Subtype.val_inj.mp <|
+    (restrictNormal_commutes σ (fixedField H) ⟨x, hx⟩).trans (h x hx) , _⟩).trans
+      AlgEquiv.ext_iff.symm)
+  intro h x hx
+  have hs : ((restrictNormalHom (fixedField H)) σ) ⟨x, hx⟩ = σ • x :=
+    restrictNormal_commutes σ (fixedField H) ⟨x, hx⟩
+  rw [← hs]
+  exact Subtype.val_inj.mpr (h ⟨x, hx⟩)
+
+open scoped Pointwise
+
+theorem fixingSubgroup_conjugate_of_map (σ : L ≃ₐ[K] L) :
+    E.fixingSubgroup = (MulAut.conj σ⁻¹) • ((IntermediateField.map σ E).fixingSubgroup) := by
+  ext τ
+  have h1 : τ ∈ (MulAut.conj σ⁻¹ • (IntermediateField.map σ E).fixingSubgroup :
+    Subgroup (L ≃ₐ[K] L)) ↔ ∀ x : ((IntermediateField.map σ E) : IntermediateField K L),
+    σ (τ (σ⁻¹ x)) = x := by
+    rw [Subgroup.mem_pointwise_smul_iff_inv_smul_mem, map_inv, inv_inv, MulAut.smul_def,
+      MulAut.conj_apply]
+    exact Iff.rfl
+  have h2 : τ ∈ E.fixingSubgroup ↔ ∀ x : E, τ x = x := Iff.rfl
+  have h3 : ∀ x : L, (x ∈ ((IntermediateField.map σ E) : IntermediateField K L) ↔
+      ∃ y : E, x = σ y) :=
+    fun x ↦ ⟨fun ⟨y, hy, heq⟩ ↦ ⟨⟨y, hy⟩, heq.symm⟩, fun ⟨⟨y, hy⟩, heq⟩ ↦ ⟨y, hy, heq.symm⟩⟩
+  rw [h1, h2]
+  exact ⟨
+    fun h ↦ (fun x ↦ (by
+      obtain ⟨y, hy⟩ := (h3 x).mp x.2
+      rw [hy, show σ⁻¹ (σ y) = y from σ.left_inv y, h y])),
+    fun h ↦ (fun x ↦ (by
+      have : σ (τ (σ⁻¹ (σ x))) = σ x := h ⟨σ x, (h3 (σ x)).mpr ⟨x, rfl⟩⟩
+      rw [show σ⁻¹ (σ x) = x from σ.left_inv x, EmbeddingLike.apply_eq_iff_eq] at this
+      exact this))⟩
+
+/-- 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
+  intro σ
+  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 σ⁻¹, inv_inv]
+
+end IsGalois
+
+end
+
 end GaloisCorrespondence
 
 section GaloisEquivalentDefinitions

Mathlib/FieldTheory/IntermediateField/Basic.lean

@@ -551,6 +551,18 @@ 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] (IntermediateField.lift F) where
+  toFun := fun x => ⟨x.1.1,(mem_lift x.1).mpr x.2⟩
+  invFun := fun x => ⟨⟨x.1, IntermediateField.lift_le F x.2⟩,
+    (mem_lift ⟨x.1, IntermediateField.lift_le F x.2⟩).mp x.2⟩
+  left_inv := congrFun rfl
+  right_inv := congrFun rfl
+  map_mul' := fun _ _ => rfl
+  map_add' := fun _ _ => rfl
+  commutes' := fun _ => rfl
+
 section RestrictScalars
 
 variable (K)