From 33761143f65b0779ff8d132272031a0e4c3f58d0 Mon Sep 17 00:00:00 2001 From: tb65536 Date: Fri, 22 May 2026 17:05:59 +0100 Subject: [PATCH 1/4] add --- .../Localization/AtPrime/Basic.lean | 50 +++++++++++++++++-- 1 file changed, 45 insertions(+), 5 deletions(-) diff --git a/Mathlib/RingTheory/Localization/AtPrime/Basic.lean b/Mathlib/RingTheory/Localization/AtPrime/Basic.lean index bf561bdba02b0e..a640d223b9b2ca 100644 --- a/Mathlib/RingTheory/Localization/AtPrime/Basic.lean +++ b/Mathlib/RingTheory/Localization/AtPrime/Basic.lean @@ -296,8 +296,10 @@ noncomputable def localRingEquiv (J : Ideal P) [J.IsPrime] (f : R ≃+* P) (hIJ right_inv x := by simp [localRingHom, map_map] variable {S} in -/-- For an algebra hom `f : S →ₐ[R] P` and a prime ideal `J` in `P`, the induced ring hom from the -localization of `R` at `J ∩ S` to the localization of `P` at `J`. -/ +/-- For an `R`-algebra homomorphism `f : S →ₐ[R] P` and prime ideals `I = f⁻¹(J)`, the induced +`R`-algebra homomorphism from the localization of `S` at `I` to the localization of `P` at `J`. + +See `localAlgHom'` for a variant where the base ring `R` is also localized. -/ noncomputable def localAlgHom [Algebra R P] (I : Ideal S) [I.IsPrime] (J : Ideal P) [J.IsPrime] (f : S →ₐ[R] P) (hIJ : I = J.comap f) : Localization.AtPrime I →ₐ[R] Localization.AtPrime J where @@ -312,7 +314,9 @@ variable {S} in localAlgHom I J f hIJ x = localRingHom I J f.toRingHom hIJ x := rfl variable {S} in -/-- Isomorphic algebras have isomorphic localizations. -/ +/-- Isomorphic algebras have isomorphic localizations. + +See `localAlgEquiv'` for a variant where the base ring is also localized. -/ @[simps] noncomputable def localAlgEquiv [Algebra R P] (I : Ideal S) [I.IsPrime] (J : Ideal P) [J.IsPrime] (f : S ≃ₐ[R] P) (hIJ : I = J.comap f) : @@ -349,8 +353,8 @@ namespace AtPrime section -variable {A B C : Type*} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra A C] - [Algebra R A] [Algebra R B] [IsScalarTower R A B] [Algebra B C] [IsScalarTower A B C] +variable {A B C : Type*} [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B] [Algebra A B] + [IsScalarTower R A B] [CommSemiring C] [Algebra A C] [Algebra B C] [IsScalarTower A B C] /-- If `P` lies over `p`, then `Localization.AtPrime P` is an algebra over `Localization.AtPrime p`. This is not an instance for performance reasons and to avoid diamonds in the situation where the top @@ -414,6 +418,42 @@ theorem mapPiEvalRingHom_algebraMap_apply {r : Π i, R i} : end AtPrime +section localAlg + +open AtPrime + +variable {S} [Algebra R P] (J : Ideal S) (K : Ideal P) [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] + +/-- For an `R`-algebra homomorphism `f : S →ₐ[R] P` and prime ideals `J = f⁻¹(K)` lying over `I`, +the induced algebra homomorphism from the localization of `S` at `J` to the localization of `P` at +`K` over the localization of `R` at `I`. + +See `localAlgHom` for a variant where the base ring `R` is not localized. -/ +noncomputable def localAlgHom' (f : S →ₐ[R] P) (h : J = K.comap f) : + Localization.AtPrime J →ₐ[Localization.AtPrime I] Localization.AtPrime K where + __ := localAlgHom J K f h + commutes' := by + let RI := Localization.AtPrime I + let f := (localAlgHom J K f h).comp (IsScalarTower.toAlgHom R RI _) + let g := IsScalarTower.toAlgHom R RI (Localization.AtPrime K) + have : f.toRingHom.comp (algebraMap R RI) = g.toRingHom.comp (algebraMap R RI) := by simp + suffices f = g by rwa [DFunLike.ext_iff] at this + apply Localization.algHom_ext + rwa [DFunLike.ext_iff] at this ⊢ + +/-- Isomorphic algebras have isomorphic localizations. + +See `localAlgEquiv` for a variant where the base ring is not localized. -/ +@[simps] +noncomputable def localAlgEquiv' (f : S ≃ₐ[R] P) (h : J = K.comap f) : + Localization.AtPrime J ≃ₐ[Localization.AtPrime I] Localization.AtPrime K where + __ := localAlgHom' I J K f.toAlgHom h + __ := localAlgEquiv J K f h + +end localAlg + end Localization section From 1e683d778c069d1b642c660ea9335e24cea63749 Mon Sep 17 00:00:00 2001 From: tb65536 Date: Fri, 29 May 2026 09:15:24 -0700 Subject: [PATCH 2/4] add --- .../Localization/AtPrime/Basic.lean | 20 ++++++------------- Mathlib/RingTheory/Localization/Basic.lean | 4 ++-- 2 files changed, 8 insertions(+), 16 deletions(-) diff --git a/Mathlib/RingTheory/Localization/AtPrime/Basic.lean b/Mathlib/RingTheory/Localization/AtPrime/Basic.lean index 3932fdd4027fe8..429a6fba691abb 100644 --- a/Mathlib/RingTheory/Localization/AtPrime/Basic.lean +++ b/Mathlib/RingTheory/Localization/AtPrime/Basic.lean @@ -431,26 +431,18 @@ the induced algebra homomorphism from the localization of `S` at `J` to the loca `K` over the localization of `R` at `I`. See `localAlgHom` for a variant where the base ring `R` is not localized. -/ +@[simps!] noncomputable def localAlgHom' (f : S →ₐ[R] P) (h : J = K.comap f) : - Localization.AtPrime J →ₐ[Localization.AtPrime I] Localization.AtPrime K where - __ := localAlgHom J K f h - commutes' := by - let RI := Localization.AtPrime I - let f := (localAlgHom J K f h).comp (IsScalarTower.toAlgHom R RI _) - let g := IsScalarTower.toAlgHom R RI (Localization.AtPrime K) - have : f.toRingHom.comp (algebraMap R RI) = g.toRingHom.comp (algebraMap R RI) := by simp - suffices f = g by rwa [DFunLike.ext_iff] at this - apply Localization.algHom_ext - rwa [DFunLike.ext_iff] at this ⊢ + Localization.AtPrime J →ₐ[Localization.AtPrime I] Localization.AtPrime K := + (localAlgHom J K f h).extendScalarsOfIsLocalization (Localization.AtPrime I) I.primeCompl /-- Isomorphic algebras have isomorphic localizations. See `localAlgEquiv` for a variant where the base ring is not localized. -/ -@[simps] +@[simps!] noncomputable def localAlgEquiv' (f : S ≃ₐ[R] P) (h : J = K.comap f) : - Localization.AtPrime J ≃ₐ[Localization.AtPrime I] Localization.AtPrime K where - __ := localAlgHom' I J K f.toAlgHom h - __ := localAlgEquiv J K f h + Localization.AtPrime J ≃ₐ[Localization.AtPrime I] Localization.AtPrime K := + (localAlgEquiv J K f h).extendScalarsOfIsLocalization (Localization.AtPrime I) I.primeCompl end localAlg diff --git a/Mathlib/RingTheory/Localization/Basic.lean b/Mathlib/RingTheory/Localization/Basic.lean index df9047149e41b3..9badde254b6b5b 100644 --- a/Mathlib/RingTheory/Localization/Basic.lean +++ b/Mathlib/RingTheory/Localization/Basic.lean @@ -687,8 +687,8 @@ theorem IsLocalization.algHom_ext {R A L B : Type*} section extend -variable {R A B : Type*} [CommRing R] [CommRing A] [CommRing B] - (S : Type*) [CommRing S] [Algebra R S] (M : Submonoid R) [IsLocalization M S] +variable {R A B : Type*} [CommSemiring R] [Semiring A] [Semiring B] + (S : Type*) [CommSemiring S] [Algebra R S] (M : Submonoid R) [IsLocalization M S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Algebra R B] [Algebra S B] [IsScalarTower R S B] From 5c20c2b0cfcb851ad828132525345cbcb4acbdcb Mon Sep 17 00:00:00 2001 From: tb65536 Date: Mon, 1 Jun 2026 12:33:02 -0700 Subject: [PATCH 3/4] add --- .../LocalRing/ResidueField/Ideal.lean | 34 +++++++++++++++---- .../RamificationInertia/Inertia.lean | 15 ++++++++ 2 files changed, 43 insertions(+), 6 deletions(-) diff --git a/Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean b/Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean index fd4f6027c0ad69..f10063a2788c23 100644 --- a/Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean +++ b/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 def 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 def 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) _ diff --git a/Mathlib/RingTheory/RamificationInertia/Inertia.lean b/Mathlib/RingTheory/RamificationInertia/Inertia.lean index 1832e595f5e45e..b36614f2b52344 100644 --- a/Mathlib/RingTheory/RamificationInertia/Inertia.lean +++ b/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 From 9a8635f65b944875b111a1582c838497fff02706 Mon Sep 17 00:00:00 2001 From: tb65536 Date: Sun, 7 Jun 2026 07:08:27 -0700 Subject: [PATCH 4/4] fix --- Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean b/Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean index f10063a2788c23..e8d783fe6e83ee 100644 --- a/Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean +++ b/Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean @@ -176,12 +176,12 @@ noncomputable def Ideal.residueFieldRingEquiv (f : A ≃+* B) (h : J = K.comap f IsLocalRing.ResidueField.mapEquiv (localRingEquiv J K f h) /-- An isomorphism of rings induces an isomorphism of residue fields. -/ -noncomputable def Ideal.residueFieldAlgEquiv (f : A ≃ₐ[R] B) (h : J = K.comap f) : +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 def Ideal.residueFieldAlgEquiv' (f : A ≃ₐ[R] B) (h : J = K.comap f) : +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)