From 6e16239a8c888e17bbac8a762cd2721da35377e4 Mon Sep 17 00:00:00 2001
From: Sean Gonzales <seang696@gmail.com>
Date: Mon, 27 Nov 2023 08:45:36 -0800
Subject: [PATCH] Updated normal correspondence code to Lean 4

---
 src/field_theory/normal_correspondence.lean | 45 ++++++++++++++++-----
 1 file changed, 36 insertions(+), 9 deletions(-)

diff --git a/src/field_theory/normal_correspondence.lean b/src/field_theory/normal_correspondence.lean
index 4964c0e52efb3..c9254870be34a 100644
--- a/src/field_theory/normal_correspondence.lean
+++ b/src/field_theory/normal_correspondence.lean
@@ -1,6 +1,7 @@
 import field_theory.galois
+import field_theory.normal_closure
 
-lemma normal_iff_stabilizing {F L : Type*}
+lemma normal_sbgp_iff_stabilizing {F L : Type*}
   [field F] [field L] [algebra F L] [is_galois F L]
   [finite_dimensional F L] (K : intermediate_field F L) :
   K.fixing_subgroup.normal ↔ ∀ (g : L ≃ₐ[F] L) (x : L), x ∈ K → g • x ∈ K :=
@@ -12,7 +13,6 @@ begin
     rw ← hk_fixing,
     rw intermediate_field.fixed_field,
     rw fixed_points.intermediate_field,
-    dsimp,
     rintro ⟨ϕ, hϕ⟩,
     change ϕ (g x) = g x,
     suffices: g⁻¹ (ϕ (g x)) = x,
@@ -51,29 +51,56 @@ begin
   },
   {
     intros hK g x hxk,
-    have gres := g ∘ K.val,
+    let gres := g.comp K.val,
+    exact hK gres ⟨x, hxk⟩,
   },
 end
 
-lemma stabilizing_iff_normal_ext {F L : Type*}
+lemma res_stabilizing_iff_normal_closure_contained {F L : Type*}
   [field F] [field L] [algebra F L] [is_galois F L]
   [finite_dimensional F L] (K : intermediate_field F L) :
-  (∀ (g : L ≃ₐ[F] L) (x : L), x ∈ K → g • x ∈ K) ↔ normal F K :=
+  (∀ (g : K →ₐ[F] L) (x : K), g x ∈ K) ↔ K.normal_closure ≤ K :=
+begin
+  rw intermediate_field.normal_closure_le_iff,
+  apply forall_congr,
+  intro a,
+  have := @set.range_subset_iff L K a K,
+  exact this.symm,
+end
+
+lemma normal_closure_contained_iff_normal {F L : Type*}
+  [field F] [field L] [algebra F L] [is_galois F L]
+  [finite_dimensional F L] (K : intermediate_field F L) :
+  K.normal_closure ≤ K ↔ normal F K :=
 begin
   split,
   {
-    sorry,
+    intro hncont,
+    rw ← le_antisymm hncont (intermediate_field.le_normal_closure K),
+    apply_instance,
   },
   {
-    -- intros hsplit g,
-    sorry,
+    introI hknormal,
+    rw intermediate_field.normal_closure_of_normal K,
+    exact le_rfl,
   },
 end
 
+lemma stabilizing_iff_normal_ext {F L : Type*}
+  [field F] [field L] [algebra F L] [is_galois F L]
+  [finite_dimensional F L] (K : intermediate_field F L) :
+  (∀ (g : L ≃ₐ[F] L) (x : L), x ∈ K → g • x ∈ K) ↔ normal F K :=
+begin
+  rw equiv.forall_congr_left' (alg_equiv_equiv_alg_hom F L).to_equiv,
+  change (∀ (g : L →ₐ[F] L) x, x ∈ K → g x ∈ K) ↔ _,
+  rw [stabilizing_iff_res_stabilizing, res_stabilizing_iff_normal_closure_contained,
+    normal_closure_contained_iff_normal],
+end
+
 theorem normal_correspondence (F L : Type*)
   [field F] [field L] [algebra F L] [is_galois F L]
   [finite_dimensional F L] (K : intermediate_field F L) :
   normal F K ↔ K.fixing_subgroup.normal :=
 begin
-  rw [normal_iff_stabilizing, stabilizing_iff_normal_ext],
+  rw [normal_sbgp_iff_stabilizing, stabilizing_iff_normal_ext],
 end