From ca817c6a344e3503102613dd96eb346afa3df3bf Mon Sep 17 00:00:00 2001
From: yhtq <1414672068@qq.com>
Date: Tue, 29 Oct 2024 16:45:02 +0800
Subject: [PATCH] Finish IsGalois

---
 .../ToMathlib/IsFractionRing.lean             |  53 ++++++
 GaloisRamification/ToMathlib/IsGalois.lean    | 158 +++++++++++++++++-
 .../ToMathlib/TransAlgStruct.lean             |  48 ++++--
 3 files changed, 240 insertions(+), 19 deletions(-)
 create mode 100644 GaloisRamification/ToMathlib/IsFractionRing.lean

diff --git a/GaloisRamification/ToMathlib/IsFractionRing.lean b/GaloisRamification/ToMathlib/IsFractionRing.lean
new file mode 100644
index 0000000..abcc5d1
--- /dev/null
+++ b/GaloisRamification/ToMathlib/IsFractionRing.lean
@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2024 Zixun Guo. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Zixun Guo
+-/
+import Mathlib.RingTheory.Localization.FractionRing
+import Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
+/-!
+Some extra lemma to IsFractionRing
+-/
+
+namespace IsFractionRing
+/--
+If K, K' are both fraction rings of R, then K ≃ₐ[R] K'
+-/
+noncomputable def algEquiv
+(R K K': Type*)
+[CommRing R] [IsDomain R]
+[Field K'] [Field K]
+[Algebra R K] [IsFractionRing R K]
+[Algebra R K'] [IsFractionRing R K']
+: K ≃ₐ[R] K'
+:= (FractionRing.algEquiv R K).symm.trans (FractionRing.algEquiv R K')
+
+variable
+{R K: Type*} [CommRing R] [IsDomain R]
+[Field K] [Algebra R K] [IsFractionRing R K]
+
+
+theorem lift_unique
+{L: Type*} [Field L]
+{g: R →+* L} (hg: Function.Injective g)
+{f: K →+* L}
+(hf1: ∀ x, f (algebraMap R K x) = g x)
+: IsFractionRing.lift hg = f := IsLocalization.lift_unique _ hf1
+
+theorem lift_unique'
+{L: Type*} [Field L]
+{g: R →+* L} (hg: Function.Injective g)
+{f1 f2: K →+* L}
+(hf1: ∀ x, f1 (algebraMap R K x) = g x)
+(hf2: ∀ x, f2 (algebraMap R K x) = g x)
+: f1 = f2 := Eq.trans (lift_unique hg hf1).symm (lift_unique hg hf2)
+
+theorem lift_unique_scalar_tower
+{L: Type*} [Field L]
+[Algebra R L] (hg: Function.Injective (algebraMap R L))
+[Algebra K L] [IsScalarTower R K L]
+: algebraMap K L = IsFractionRing.lift hg
+:= (lift_unique hg (fun x => (IsScalarTower.algebraMap_apply R K L x).symm)).symm
+
+
+end IsFractionRing
diff --git a/GaloisRamification/ToMathlib/IsGalois.lean b/GaloisRamification/ToMathlib/IsGalois.lean
index 17492ee..68dac2d 100644
--- a/GaloisRamification/ToMathlib/IsGalois.lean
+++ b/GaloisRamification/ToMathlib/IsGalois.lean
@@ -4,19 +4,163 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yongle Hu, Zixun Guo
 -/
 import Mathlib.FieldTheory.Galois.Basic
+import GaloisRamification.ToMathlib.IsFractionRing
+import GaloisRamification.ToMathlib.TransAlgStruct
 
 attribute [local instance] FractionRing.liftAlgebra
 
+/-
+  The aim is to prove a commutative diagram:
+  ----------------
+  |               |
+  \/             \/
+  L  <--- B ---> L'
+  /\      /\     /\
+  |       |      |
+  |       |      |
+  K  <--- A ---> K'
+  /\             /\
+  |               |
+  -----------------
+  in which K <-> K' and L <-> L' come from canonical isomorphisms between two fraction rings of A and B, respectively. The only path to prove is :
+  K -> L -> L' = K -> K' -> L'
+  which induced by the fact that they are both lifting functions of A -> L'
+-/
+#check Equiv.algEquiv
+section
+variable (A B K L K' L' : Type*)
+  [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B] [NoZeroSMulDivisors A B]
+  [Field K] [Field L]
+  [Algebra A K] [IsFractionRing A K]
+  [Algebra B L] [IsFractionRing B L]
+  [Algebra K L] [Algebra A L]
+  [IsScalarTower A B L] [IsScalarTower A K L]
+  [Field K'] [Field L']
+  [Algebra A K'] [IsFractionRing A K']
+  [Algebra B L'] [IsFractionRing B L']
+  [Algebra K' L'] [Algebra A L']
+  [IsScalarTower A B L'] [IsScalarTower A K' L']
+
+private noncomputable def KK': HasRingEquiv K K' := { ringEquiv := IsFractionRing.algEquiv A K K' }
+private noncomputable def LL': HasRingEquiv L L' := { ringEquiv := IsFractionRing.algEquiv B L L' }
+
+private noncomputable def alg_KL' : Algebra K L' := Algebra.algOfAlgOnEquivRing K' L' (e := KK' A K K')
+
+/- following directly from definition, there is a scalar tower K -> K' -> L'
+-/
+private def scalar_tower_K_K'_L':
+  let _ := alg_KL' A K K' L'
+  let _ := KK' A K K'
+  let _ := Algebra.algOfRingEquiv K K'
+  IsScalarTower K K' L' :=
+    let _ := alg_KL' A K K' L'
+    let _ := KK' A K K'
+    let _ := Algebra.algOfRingEquiv K K'
+    Algebra.ofAlgOnEquivRing_scalar_tower _ _
 
 
+private def scalar_tower_K_L_L':
+  let _ := alg_KL' A K K' L'
+  let _ := LL' B L L'
+  let _ := Algebra.algOfRingEquiv L L'
+  IsScalarTower K L L' := by
+    letI _ := alg_KL' A K K' L'
+    letI _ := LL' B L L'
+    letI _ := KK' A K K'
+    letI _ := Algebra.algOfRingEquiv L L'
+    letI _ := Algebra.algOfRingEquiv K K'
+    letI _KK'L' := scalar_tower_K_K'_L' A K K' L'
+    simp at _KK'L'
+    simp only at *
+    apply IsScalarTower.of_algebraMap_eq
+    intro x
+    rw [<-Function.comp_apply (x := x) (g := algebraMap K L) (f := algebraMap L L')]
+    apply congrFun
+    rw [<-RingHom.coe_comp, DFunLike.coe_fn_eq]
+    apply IsFractionRing.lift_unique' (R := A) (g := algebraMap A L')
+    · rw [IsScalarTower.algebraMap_eq A B L', RingHom.coe_comp]
+      apply Function.Injective.comp
+      · exact NoZeroSMulDivisors.algebraMap_injective B L'
+      · exact NoZeroSMulDivisors.algebraMap_injective A B
+    · intro x
+      rw [@IsScalarTower.algebraMap_eq K K' L' _ _ _ _ _ _ _KK'L']
+      simp only [RingHom.coe_comp, Function.comp_apply, Algebra.algOfAlgOnEquivRing_algebraMap_def,
+        smul_eq_mul, mul_one]
+      rw [show (HasRingEquiv.ringEquiv: K -> K') = IsFractionRing.algEquiv A K K' from rfl]
+      rw [AlgEquiv.commutes]
+      exact Eq.symm (IsScalarTower.algebraMap_apply A K' L' x)
+    · intro x
+      rw [IsScalarTower.algebraMap_eq A B L']
+      have : algebraMap B L' = (algebraMap L L').comp (algebraMap B L) := by
+        rw [Algebra.algOfRingEquiv_algebraMap_def']
+        rw [show (HasRingEquiv.ringEquiv: L ≃+* L') = IsFractionRing.algEquiv B L L' from rfl]
+        simp only [AlgEquiv.toRingEquiv_toRingHom]
+        ext r
+        simp only [RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, AlgEquiv.commutes]
+      rw [this]
+      simp only [Algebra.algOfRingEquiv_algebraMap_def', RingHom.coe_comp, RingHom.coe_coe,
+        Function.comp_apply, EmbeddingLike.apply_eq_iff_eq]
+      rw [<-IsScalarTower.algebraMap_apply A K L]
+      rw [<-IsScalarTower.algebraMap_apply A B L]
 
-variable (A K L B : Type*)
+end
+
+
+/- Galois extension is transfered between two pairs of fraction rings
+-/
+theorem IsGalois.of_isGalois_isfractionRing
+  (A B K L K' L' : Type*)
   [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B] [NoZeroSMulDivisors A B]
-  [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsFractionRing B L]
-  [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L]
+  [Field K] [Field L]
+  [Algebra A K] [IsFractionRing A K]
+  [Algebra B L] [IsFractionRing B L]
+  [Algebra K L] [Algebra A L]
+  [IsScalarTower A B L] [IsScalarTower A K L]
+  [Field K'] [Field L']
+  [Algebra A K'] [IsFractionRing A K']
+  [Algebra B L'] [IsFractionRing B L']
+  [Algebra K' L'] [Algebra A L']
+  [IsScalarTower A B L'] [IsScalarTower A K' L']
+  [IsGalois K L] :
+    IsGalois K' L' := by
+      letI _ := alg_KL' A K K' L'
+      letI _ := LL' B L L'
+      letI _ := KK' A K K'
+      letI _ := Algebra.algOfRingEquiv L L'
+      letI _ := Algebra.algOfRingEquiv K K'
+      letI _KK'L' := scalar_tower_K_K'_L' A K K' L'
+      letI _KLL' := scalar_tower_K_L_L' A B  K L K' L'
+      haveI : IsGalois K L' := by
+        apply IsGalois.of_algEquiv (E := L)
+        apply AlgEquiv.ofRingEquiv (f := IsFractionRing.algEquiv B L L')
+        rw [@IsScalarTower.algebraMap_eq K L L' _ _ _ _ _ _ _KLL']
+        simp only [AlgEquiv.coe_ringEquiv, Algebra.algOfRingEquiv_algebraMap_def', RingHom.coe_comp,
+          RingHom.coe_coe, Function.comp_apply]
+        intro x
+        apply congrFun
+        rfl
+      exact @IsGalois.tower_top_of_isGalois K K' L' _ _ _ _ _ _ _KK'L' _
 
-theorem IsGalois.of_isGalois_fractionRing [IsGalois (FractionRing A) (FractionRing B)] :
-    IsGalois K L := sorry
 
-theorem IsGalois.of_isGalois_isFractionRing [IsGalois K L] :
-    IsGalois (FractionRing A) (FractionRing B) := sorry
+theorem IsGalois.isFractionRing_of_isGalois_FractionRing
+(A B K L : Type*)
+  [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B] [NoZeroSMulDivisors A B]
+  [Field K] [Field L]
+  [Algebra A K] [IsFractionRing A K]
+  [Algebra B L] [IsFractionRing B L]
+  [Algebra K L] [Algebra A L]
+  [IsScalarTower A B L] [IsScalarTower A K L]
+  [IsGalois (FractionRing A) (FractionRing B)]
+  : IsGalois K L := IsGalois.of_isGalois_isfractionRing A B (FractionRing A) (FractionRing B) K L
+
+
+theorem IsGalois.FractionRing_of_isGalois_isFractionRing
+(A B K L : Type*)
+  [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B] [NoZeroSMulDivisors A B]
+  [Field K] [Field L]
+  [Algebra A K] [IsFractionRing A K]
+  [Algebra B L] [IsFractionRing B L]
+  [Algebra K L] [Algebra A L]
+  [IsScalarTower A B L] [IsScalarTower A K L]
+  [IsGalois K L]
+  : IsGalois (FractionRing A) (FractionRing B) := IsGalois.of_isGalois_isfractionRing A B K L (FractionRing A) (FractionRing B)
diff --git a/GaloisRamification/ToMathlib/TransAlgStruct.lean b/GaloisRamification/ToMathlib/TransAlgStruct.lean
index a7e1b90..a5beb62 100644
--- a/GaloisRamification/ToMathlib/TransAlgStruct.lean
+++ b/GaloisRamification/ToMathlib/TransAlgStruct.lean
@@ -8,21 +8,25 @@ import Mathlib.Algebra.Algebra.Defs
 import Mathlib.Algebra.Algebra.Equiv
 
 /-!
-# trans Algebra structure through ring equiv
+# transfer Algebra structure through ring equiv
 
-In this file, we intro some definitions and lemma to trans Algebra structure through ring equiv.
+In this file, we intro some definitions and lemma to transfer Algebra structure through ring equiv.
 
 ## Main Results
-* `ofAlgOnEquivRing`: if `R' ≃+* R`, then `Algebra R' B` can induce a canonical `Algebra R B`.
+* `algOfAlgOnEquivRing`: if `R' ≃+* R`, then `Algebra R' B` can induce a canonical `Algebra R B`.
+* `algOfRingEquiv`: if `R' ≃+* R`, then there is a canonical `Algebra R R'` instance.
+* `algOfRingEquivReverse`: if `R' ≃+* R`, then there is a canonical `Algebra R' R` instance.
+* `ofAlgOnEquivRing_scalar_tower`: shows that the Algebra structure generated by `ofAlgOnEquivRing` is compatible with the Algebra structure generated by `ofRingEquiv`
+* `of_equiv_on_equiv_ring`: define a `AlgEquiv` directly from equiv ring
 -/
 
-namespace Algebra
-
 /--
 a class to define the ring equiv used in the context
 -/
 class HasRingEquiv (R R' : Type*) [Add R] [Add R'] [Mul R] [Mul R'] where
   ringEquiv : R ≃+* R'
+namespace Algebra
+
 
 noncomputable def has_ring_equiv_reverse (R R' : Type*) [Add R] [Add R'] [Mul R] [Mul R'] (e: HasRingEquiv R R') : HasRingEquiv R' R where
   ringEquiv := e.ringEquiv.symm
@@ -30,7 +34,7 @@ noncomputable def has_ring_equiv_reverse (R R' : Type*) [Add R] [Add R'] [Mul R]
 theorem has_ring_equiv_reverse_def (R R' : Type*) [Add R] [Add R'] [Mul R] [Mul R'] (e: HasRingEquiv R R')
 : has_ring_equiv_reverse R R' e = ⟨e.ringEquiv.symm⟩ := rfl
 /--
-trans Algebra R' B to Algebra R B if R' ≃+* R
+transfer Algebra R' B to Algebra R B if R' ≃+* R
 -/
 noncomputable def algOfAlgOnEquivRing
 {R: Type*} (R' B : Type*)
@@ -60,10 +64,13 @@ noncomputable def algOfAlgOnEquivRing
       simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, Algebra.smul_mul_assoc, one_mul]
       rfl
 
+@[simp]
 theorem algOfAlgOnEquivRing_smul_def {R: Type*} {R' B : Type*}
 [CommSemiring R] [CommSemiring R'] [Semiring B]
 [Algebra R' B] [e: HasRingEquiv R R']
-(r: R) (b: B): (algOfAlgOnEquivRing R' B).smul r b = e.ringEquiv r • b := rfl
+(r: R) (b: B):
+let _: Algebra R B := algOfAlgOnEquivRing R' B
+r • b = e.ringEquiv r • b := rfl
 
 @[simp]
 theorem algOfAlgOnEquivRing_algebraMap_def {R: Type*} {R' B : Type*}
@@ -74,12 +81,29 @@ theorem algOfAlgOnEquivRing_algebraMap_def {R: Type*} {R' B : Type*}
 /--
 if `R' ≃+* R`, then there is a canonical `Algebra R R'` instance.
 -/
-noncomputable def algOfRingEquiv (R R': Type*) [CommSemiring R] [CommSemiring R'] [HasRingEquiv R R'] : Algebra R R'
+noncomputable def algOfRingEquiv (R R': Type*) [CommSemiring R] [CommSemiring R'] [e: HasRingEquiv R R'] : Algebra R R'
 := algOfAlgOnEquivRing R' R'
 
 noncomputable def algOfRingEquivReverse (R R': Type*) [CommSemiring R] [CommSemiring R'] [e: HasRingEquiv R R'] : Algebra R' R
 := @algOfRingEquiv R' R _ _ (has_ring_equiv_reverse R R' e)
 
+@[simp]
+theorem algOfRingEquiv_smul_def {R R': Type*} [CommSemiring R] [CommSemiring R'] [e: HasRingEquiv R R']
+(r: R) (b: R'):
+  let _: Algebra R R' := algOfRingEquiv R R'
+  r • b = e.ringEquiv r • b := rfl
+
+@[simp]
+theorem algOfRingEquiv_algebraMap_def {R R': Type*} [CommSemiring R] [CommSemiring R'] [e: HasRingEquiv R R']
+(r: R): @algebraMap R R'  _ _ (algOfRingEquiv R R') r = e.ringEquiv r := by
+  simp only [algOfAlgOnEquivRing_algebraMap_def, smul_eq_mul, mul_one]
+
+@[simp]
+theorem algOfRingEquiv_algebraMap_def' {R R': Type*} [CommSemiring R] [CommSemiring R'] [e: HasRingEquiv R R']
+: @algebraMap R R'  _ _ (algOfRingEquiv R R')  = e.ringEquiv := by
+  ext r
+  exact algOfRingEquiv_algebraMap_def r
+
 @[simp]
 theorem algOfRingEquiv_RingHom {R R': Type*} [CommSemiring R] [CommSemiring R'] [e: HasRingEquiv R R'] : (algOfRingEquiv R R').toRingHom = e.ringEquiv
 := by
@@ -101,14 +125,14 @@ def ofAlgOnEquivRing_scalar_tower
 {R: Type*} (R' B : Type*)
 [CommSemiring R] [CommSemiring R'] [Semiring B]
 [Algebra R' B] [e: HasRingEquiv R R']:
-@IsScalarTower R' R B (algOfRingEquivReverse R R').toSMul (algOfAlgOnEquivRing R' B).toSMul _ := by
-  letI smul1_instance := (algOfRingEquivReverse R R').toSMul
+@IsScalarTower R R' B (algOfRingEquiv R R').toSMul _ (algOfAlgOnEquivRing R' B).toSMul  := by
+  letI smul1_instance := (algOfRingEquiv R R').toSMul
   letI smul2_instance := (algOfAlgOnEquivRing R' B: Algebra R B).toSMul
-  let smul1 := fun s (f: R) => e.ringEquiv.symm s • f
+  let smul1 := fun (s: R) (f: R') => e.ringEquiv s • f
   let smul2 := fun s (f: B) => e.ringEquiv s • f
   apply IsScalarTower.mk
   intro r x y
-  show smul2 (smul1 r x) y = r • (smul2 x y)
+  show (smul1 r x) • y = smul2 r (x • y)
   unfold_let smul1 smul2
   simp only [smul_eq_mul, map_mul, RingEquiv.apply_symm_apply, mul_smul]
 end Algebra