feat(RingTheory/RamificationInertia/Inertia): inertia degree is invariant under a group action (leanprover-community#40124)

This PR proves that inertia degree is invariant under a group action. We already have this for the old definition `inertiaDeg`, but we will need this new version for `inertiaDeg'` for the upcoming refactor.

Co-authored-by: tb65536 <thomas.l.browning@gmail.com>

Author: tb65536

Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean

@@ -158,12 +158,34 @@ lemma Ideal.surjectiveOnStalks_residueField (I : Ideal R) [I.IsPrime] :
   (RingHom.surjectiveOnStalks_of_surjective Ideal.Quotient.mk_surjective).comp
     (RingHom.surjectiveOnStalks_of_isLocalization I.primeCompl _)
 
-instance (p : Ideal R) [p.IsPrime] (q : Ideal A) [q.IsPrime] [q.LiesOver p]
-    [Algebra (Localization.AtPrime p) (Localization.AtPrime q)]
-    [Localization.AtPrime.IsLiesOverAlgebra p q] :
-    IsLocalHom (algebraMap (Localization.AtPrime p) (Localization.AtPrime q)) := by
-  rw [Localization.AtPrime.IsLiesOverAlgebra.algebraMap_eq]
-  exact Localization.isLocalHom_localRingHom _ _ _ (Ideal.over_def _ _)
+section
+
+open Localization AtPrime
+
+variable (J : Ideal A) (K : Ideal B) [J.IsPrime] [K.IsPrime]
+  [J.LiesOver I] [Algebra (Localization.AtPrime I) (Localization.AtPrime J)] [IsLiesOverAlgebra I J]
+  [K.LiesOver I] [Algebra (Localization.AtPrime I) (Localization.AtPrime K)] [IsLiesOverAlgebra I K]
+
+instance : IsLocalHom (algebraMap (Localization.AtPrime I) (Localization.AtPrime J)) := by
+  rw [IsLiesOverAlgebra.algebraMap_eq]
+  exact isLocalHom_localRingHom _ _ _ (J.over_def I)
+
+/-- An isomorphism of rings induces an isomorphism of residue fields. -/
+noncomputable def Ideal.residueFieldRingEquiv (f : A ≃+* B) (h : J = K.comap f) :
+    J.ResidueField ≃+* K.ResidueField :=
+  IsLocalRing.ResidueField.mapEquiv (localRingEquiv J K f h)
+
+/-- An isomorphism of rings induces an isomorphism of residue fields. -/
+noncomputable abbrev Ideal.residueFieldAlgEquiv (f : A ≃ₐ[R] B) (h : J = K.comap f) :
+    J.ResidueField ≃ₐ[R] K.ResidueField :=
+  IsLocalRing.ResidueField.mapAlgEquiv (localAlgEquiv J K f h)
+
+/-- An isomorphism of rings induces an isomorphism of residue fields. -/
+noncomputable abbrev Ideal.residueFieldAlgEquiv' (f : A ≃ₐ[R] B) (h : J = K.comap f) :
+    J.ResidueField ≃ₐ[I.ResidueField] K.ResidueField :=
+  IsLocalRing.ResidueField.mapAlgEquiv' (localAlgEquiv' I J K f h)
+
+end
 
 instance (p : Ideal R) [p.IsPrime] : Algebra.EssFiniteType R p.ResidueField :=
   .comp _ (Localization.AtPrime p) _

Mathlib/RingTheory/RamificationInertia/Inertia.lean

@@ -105,6 +105,21 @@ theorem inertiaDeg'_tower [r.LiesOver q] :
     apply Module.finrank_mul_finrank
   · rw [inertiaDeg'_of_not_isPrime r R hr, inertiaDeg'_of_not_isPrime r S hr, mul_zero]
 
+variable (R) in
+open Pointwise in
+@[simp]
+theorem inertiaDeg'_smul {G : Type*} [Group G] [MulSemiringAction G S] [SMulCommClass G R S]
+    (g : G) : (g • q).inertiaDeg' R = q.inertiaDeg' R := by
+  by_cases hq : q.IsPrime; swap
+  · rw [inertiaDeg'_of_not_isPrime, inertiaDeg'_of_not_isPrime] <;> simpa
+  · let p := q.under R
+    let f₀ := MulSemiringAction.toAlgAut G R S g
+    let := Localization.AtPrime.algebraOfLiesOver p q
+    let := Localization.AtPrime.algebraOfLiesOver p (g • q)
+    rw [inertiaDeg'_eq p q, inertiaDeg'_eq p (g • q)]
+    let e₂ := Ideal.residueFieldAlgEquiv' p (g • q) q f₀.symm (comap_symm f₀.toRingEquiv).symm
+    exact e₂.toLinearEquiv.finrank_eq
+
 end
 
 end Ideal