add

Author: tb65536

Mathlib/RingTheory/Invariant/Basic.lean

@@ -357,6 +357,12 @@ theorem IsFractionRing.stabilizerHom_apply_apply_mk (σ : MulAction.stabilizer G
       algebraMap _ L (Ideal.Quotient.mk Q (σ.val • x)) := by
   simp [IsFractionRing.stabilizerHom, MulAction.subgroup_smul_def]
 
+omit [Finite G] [Q.IsPrime] [Algebra.IsInvariant A B G] in
+theorem IsFractionRing.ker_stabilizerHom :
+    (stabilizerHom G P Q K L).ker = (Q.inertia G).subgroupOf (MulAction.stabilizer G Q) := by
+  rw [stabilizerHom, MonoidHom.ker_comp_of_injective, Ideal.Quotient.ker_stabilizerHom]
+  apply fieldEquivOfAlgEquivHom_injective
+
 /-- This theorem will be made redundant by `IsFractionRing.stabilizerHom_surjective`. -/
 private theorem fixed_of_fixed2 (f : Gal(L/K)) (x : L)
     (hx : ∀ g : MulAction.stabilizer G Q, IsFractionRing.stabilizerHom G P Q K L g x = x) :
@@ -400,6 +406,18 @@ theorem Ideal.Quotient.stabilizerHom_surjective :
   exact key.of_comp_left (IsFractionRing.fieldEquivOfAlgEquivHom_injective (A ⧸ P) (B ⧸ Q)
     (FractionRing (A ⧸ P)) (FractionRing (B ⧸ Q)))
 
+/--
+The isomorphism between `stabilizer G Q ⧸ inertia G Q` and the Galois group of the residue fields.
+-/
+noncomputable def IsFractionRing.stabilizerQuotientInertiaEquiv :
+    MulAction.stabilizer G Q ⧸ (Q.inertia G).subgroupOf (MulAction.stabilizer G Q) ≃* Gal(L/K) :=
+  QuotientGroup.liftEquiv (N := (Q.inertia G).subgroupOf (MulAction.stabilizer G Q))
+    (stabilizerHom_surjective G P Q K L) (ker_stabilizerHom G P Q K L).symm
+
+@[simp]
+theorem IsFractionRing.stabilizerQuotientInertiaEquiv_mk (g : MulAction.stabilizer G Q) :
+    stabilizerQuotientInertiaEquiv G P Q K L g = stabilizerHom G P Q K L g := rfl
+
 /--
 The isomorphism between `stabilizer G Q ⧸ inertia G Q` and the Galois group of the residue fields
 extension `B ⧸ Q` over `A ⧸ P`.
@@ -410,6 +428,7 @@ noncomputable def Ideal.Quotient.stabilizerQuotientInertiaEquiv :
   QuotientGroup.liftEquiv (N := (Q.inertia G).subgroupOf (MulAction.stabilizer G Q))
     (stabilizerHom_surjective G P Q) (ker_stabilizerHom Q P G).symm
 
+@[simp]
 theorem Ideal.Quotient.stabilizerQuotientInertiaEquiv_mk (g : MulAction.stabilizer G Q) :
     stabilizerQuotientInertiaEquiv G P Q g = stabilizerHom Q P G g := rfl