feat: add Mathlib.RingTheory.DedekindDomain.Instances (#26070)

We add a new file `Mathlib.RingTheory.DedekindDomain.Instances` containing various instances that are useful to work with the localization a prime of an extension of Dedekind domains. As a practical example we golf a tedious proof in `Mathlib.RingTheory.Ideal/Norm.RelNorm`.

Author: riccardobrasca

Mathlib.lean

@@ -5196,6 +5196,7 @@ import Mathlib.RingTheory.DedekindDomain.Dvr
 import Mathlib.RingTheory.DedekindDomain.Factorization
 import Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
 import Mathlib.RingTheory.DedekindDomain.Ideal
+import Mathlib.RingTheory.DedekindDomain.Instances
 import Mathlib.RingTheory.DedekindDomain.IntegralClosure
 import Mathlib.RingTheory.DedekindDomain.PID
 import Mathlib.RingTheory.DedekindDomain.SInteger

Mathlib/RingTheory/DedekindDomain/Different.lean

@@ -472,7 +472,7 @@ theorem differentIdeal_ne_bot [Module.Finite A B]
   let L := FractionRing B
   have : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L :=
     IsIntegralClosure.isLocalization _ K _ _
-  have : FiniteDimensional K L := Module.Finite_of_isLocalization A B _ _ A⁰
+  have : FiniteDimensional K L := .of_isLocalization A B A⁰
   rw [ne_eq, ← FractionalIdeal.coeIdeal_inj (K := L), coeIdeal_differentIdeal (K := K)]
   simp
 
@@ -649,8 +649,7 @@ lemma pow_sub_one_dvd_differentIdeal [Algebra.IsSeparable (FractionRing A) (Frac
     (hP : P ^ e ∣ p.map (algebraMap A B)) : P ^ (e - 1) ∣ differentIdeal A B := by
   have : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B) :=
     IsIntegralClosure.isLocalization _ (FractionRing A) _ _
-  have : FiniteDimensional (FractionRing A) (FractionRing B) :=
-    Module.Finite_of_isLocalization A B _ _ A⁰
+  have : FiniteDimensional (FractionRing A) (FractionRing B) := .of_isLocalization A B A⁰
   by_cases he : e = 0
   · rw [he, pow_zero]; exact one_dvd _
   exact pow_sub_one_dvd_differentIdeal_aux A (FractionRing A) (FractionRing B) _ he hp hP
@@ -675,7 +674,7 @@ theorem not_dvd_differentIdeal_of_intTrace_not_mem
   let L := FractionRing B
   have : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L :=
     IsIntegralClosure.isLocalization _ K _ _
-  have : FiniteDimensional K L := Module.Finite_of_isLocalization A B _ _ A⁰
+  have : FiniteDimensional K L := .of_isLocalization A B A⁰
   rw [Ideal.dvd_iff_le]
   intro H
   replace H := (mul_le_mul_right' H Q).trans_eq hP
@@ -766,8 +765,7 @@ lemma dvd_differentIdeal_of_not_isSeparable
   let L := FractionRing B
   have : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L :=
     IsIntegralClosure.isLocalization _ K _ _
-  have : FiniteDimensional K L :=
-    Module.Finite_of_isLocalization A B _ _ A⁰
+  have : FiniteDimensional K L := .of_isLocalization A B A⁰
   have hp' := (Ideal.map_eq_bot_iff_of_injective
     (FaithfulSMul.algebraMap_injective A B)).not.mpr hp
   have habot : a ≠ ⊥ := fun ha' ↦ hp' (by simpa [ha'] using ha)
@@ -826,7 +824,7 @@ theorem not_dvd_differentIdeal_iff
     simp only [Submodule.zero_eq_bot, differentIdeal_ne_bot, not_false_eq_true, true_iff]
     let K := FractionRing A
     let L := FractionRing B
-    have : FiniteDimensional K L := Module.Finite_of_isLocalization A B _ _ A⁰
+    have : FiniteDimensional K L := .of_isLocalization A B A⁰
     have : IsLocalization B⁰ (Localization.AtPrime (⊥ : Ideal B)) := by
       convert (inferInstanceAs
         (IsLocalization (⊥ : Ideal B).primeCompl (Localization.AtPrime (⊥ : Ideal B))))

Mathlib/RingTheory/DedekindDomain/Instances.lean

@@ -0,0 +1,138 @@
+/-
+Copyright (c) 2025 Riccardo Brasca. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Riccardo Brasca
+-/
+
+import Mathlib.Algebra.Lie.OfAssociative
+import Mathlib.Order.CompletePartialOrder
+import Mathlib.RingTheory.DedekindDomain.PID
+import Mathlib.FieldTheory.Separable
+
+/-!
+# Instances for Dedekind domains
+This file contains various instances to work with localization of a ring extension.
+
+A very common situation in number theory is to have an extension of (say) Dedekind domains `R` and
+`S`, and to prove a property of this extension it is useful to consider the localization `Rₚ` of `R`
+at `P`, a prime ideal of `R`. One also works with the corresponding localization `Sₚ` of `S` and the
+fraction fields `K` and `L` of `R` and `S`. In this situation there are many compatible algebra
+structures and various properties of the rings involved. This file contains a collection of such
+instances.
+
+## Implementation details
+In general one wants all the results below for any algebra satisfying `IsLocalization`, but those
+cannot be instances (since Lean has no way of guessing the submonoid). Having the instances in the
+special case of *the* localization at a prime ideal is useful in working with Dedekind domains.
+
+-/
+
+open nonZeroDivisors IsLocalization Algebra IsFractionRing IsScalarTower
+
+attribute [local instance] FractionRing.liftAlgebra
+
+variable {R : Type*} (S : Type*) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S]
+
+local notation3 "K" => FractionRing R
+local notation3 "L" => FractionRing S
+section
+
+theorem algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul {A : Type*} (B : Type*)
+    [CommSemiring A] [CommSemiring B] [Algebra A B] [NoZeroDivisors B] [FaithfulSMul A B]
+    {S : Submonoid A} (hS : S ≤ A⁰) : algebraMapSubmonoid B S ≤ B⁰ :=
+  map_le_nonZeroDivisors_of_injective _ (FaithfulSMul.algebraMap_injective A B) hS
+
+variable (Rₘ Sₘ : Type*) [CommRing Rₘ] [CommRing Sₘ] [Algebra R Rₘ] [NoZeroSMulDivisors R S]
+    [Algebra.IsSeparable (FractionRing R) (FractionRing S)] {M : Submonoid R} [IsLocalization M Rₘ]
+    [Algebra Rₘ Sₘ] [Algebra S Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ]
+    [IsScalarTower R S Sₘ] [IsLocalization (algebraMapSubmonoid S M) Sₘ]
+    [Algebra (FractionRing Rₘ) (FractionRing Sₘ)]
+    [IsScalarTower Rₘ (FractionRing Rₘ) (FractionRing Sₘ)]
+
+include R S in
+theorem FractionRing.isSeparable_of_isLocalization (hM : M ≤ R⁰) :
+    Algebra.IsSeparable (FractionRing Rₘ) (FractionRing Sₘ) := by
+  let M' := algebraMapSubmonoid S M
+  have hM' : algebraMapSubmonoid S M ≤ S⁰ := algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul
+    _ hM
+  let f₁ : Rₘ →+* K := map _ (T := R⁰) (RingHom.id R) hM
+  let f₂ : Sₘ →+* L := map _ (T := S⁰) (RingHom.id S) hM'
+  algebraize [f₁, f₂]
+  have := localization_isScalarTower_of_submonoid_le Rₘ K _ _ hM
+  have := localization_isScalarTower_of_submonoid_le Sₘ L _ _ hM'
+  have := isFractionRing_of_isDomain_of_isLocalization M Rₘ K
+  have := isFractionRing_of_isDomain_of_isLocalization M' Sₘ L
+  have : IsDomain Rₘ := isDomain_of_le_nonZeroDivisors _ hM
+  apply Algebra.IsSeparable.of_equiv_equiv (FractionRing.algEquiv Rₘ K).symm.toRingEquiv
+    (FractionRing.algEquiv Sₘ L).symm.toRingEquiv
+  apply ringHom_ext R⁰
+  ext
+  simp only [AlgEquiv.toRingEquiv_eq_coe, RingHom.coe_comp,
+      RingHom.coe_coe, Function.comp_apply, ← algebraMap_apply]
+  rw [algebraMap_apply R Rₘ (FractionRing R), AlgEquiv.coe_ringEquiv, AlgEquiv.commutes,
+    algebraMap_apply R S L, algebraMap_apply S Sₘ L, AlgEquiv.coe_ringEquiv, AlgEquiv.commutes]
+  simp only [← algebraMap_apply]
+  rw [algebraMap_apply R Rₘ (FractionRing Rₘ), ← algebraMap_apply Rₘ, ← algebraMap_apply]
+
+end
+
+variable {P : Ideal R} [P.IsPrime]
+
+local notation3 "P'" => algebraMapSubmonoid S P.primeCompl
+local notation3 "Rₚ" => Localization.AtPrime P
+local notation3 "Sₚ" => Localization P'
+
+variable [FaithfulSMul R S]
+
+noncomputable instance : Algebra Sₚ L :=
+  (map _ (T := S⁰) (RingHom.id S)
+    (algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul _
+      P.primeCompl_le_nonZeroDivisors)).toAlgebra
+
+instance : IsScalarTower S Sₚ L :=
+  localization_isScalarTower_of_submonoid_le _ _ _ _
+    (algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul _
+      P.primeCompl_le_nonZeroDivisors)
+
+instance : IsFractionRing Rₚ K :=
+  isFractionRing_of_isDomain_of_isLocalization P.primeCompl _ _
+
+instance : IsFractionRing Sₚ L :=
+  isFractionRing_of_isDomain_of_isLocalization P' _ _
+
+noncomputable instance : Algebra Rₚ L :=
+  (lift (M := P.primeCompl) (g := algebraMap R L) <|
+    fun ⟨x, hx⟩ ↦ by simpa using fun h ↦ hx <| by simp [h]).toAlgebra
+
+-- Make sure there are no diamonds in the case `R = S`.
+example : instAlgebraLocalizationAtPrime P = instAlgebraAtPrimeFractionRing (S := R) := by
+  with_reducible_and_instances rfl
+
+instance : IsScalarTower Rₚ K L :=
+  of_algebraMap_eq' (ringHom_ext P.primeCompl
+    (RingHom.ext fun x ↦ by simp [RingHom.algebraMap_toAlgebra]))
+
+instance : IsScalarTower R Rₚ K :=
+  of_algebraMap_eq' (RingHom.ext fun x ↦ by simp [RingHom.algebraMap_toAlgebra])
+
+instance : IsScalarTower Rₚ Sₚ L := by
+  refine IsScalarTower.of_algebraMap_eq' <| IsLocalization.ringHom_ext P.primeCompl ?_
+  rw [RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq R Rₚ Sₚ, IsScalarTower.algebraMap_eq R S Sₚ,
+    ← RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq S Sₚ L, IsScalarTower.algebraMap_eq Rₚ K L,
+    RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq,
+    ← IsScalarTower.algebraMap_eq]
+
+instance [IsDedekindDomain S] : IsDedekindDomain Sₚ :=
+  isDedekindDomain S
+    (algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul _ P.primeCompl_le_nonZeroDivisors) _
+
+instance [IsDedekindDomain R] [IsDedekindDomain S] [Module.Finite R S] [hP : NeZero P] :
+    IsPrincipalIdealRing Sₚ :=
+  IsDedekindDomain.isPrincipalIdealRing_localization_over_prime S P (fun h ↦ hP.1 h)
+
+instance [Algebra.IsSeparable K L] :
+    -- Without the following line there is a timeout
+    letI : Algebra Rₚ (FractionRing Sₚ) := OreLocalization.instAlgebra
+    Algebra.IsSeparable (FractionRing Rₚ) (FractionRing Sₚ) :=
+  let _ : Algebra Rₚ (FractionRing Sₚ) := OreLocalization.instAlgebra
+  FractionRing.isSeparable_of_isLocalization S _ _ P.primeCompl_le_nonZeroDivisors

Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean

@@ -9,6 +9,7 @@ import Mathlib.LinearAlgebra.BilinearForm.DualLattice
 import Mathlib.RingTheory.DedekindDomain.Basic
 import Mathlib.RingTheory.Localization.Module
 import Mathlib.RingTheory.Trace.Basic
+import Mathlib.RingTheory.RingHom.Finite
 
 /-!
 # Integral closure of Dedekind domains
@@ -247,8 +248,8 @@ instance integralClosure.isDedekindDomain_fractionRing [IsDedekindDomain A] :
   integralClosure.isDedekindDomain A (FractionRing A) L
 
 attribute [local instance] FractionRing.liftAlgebra in
-instance [NoZeroSMulDivisors A C] [Module.Finite A C] [IsIntegrallyClosed C] :
-    IsLocalization (Algebra.algebraMapSubmonoid C A⁰) (FractionRing C) :=
-  IsIntegralClosure.isLocalization _ (FractionRing A) _ _
+instance [Module.Finite A C] [NoZeroSMulDivisors A C] :
+    FiniteDimensional (FractionRing A) (FractionRing C) :=
+  .of_isLocalization A C A⁰
 
 end IsIntegralClosure

Mathlib/RingTheory/Ideal/Norm/RelNorm.lean

@@ -5,6 +5,7 @@ Authors: Anne Baanen, Alex J. Best
 -/
 import Mathlib.LinearAlgebra.FreeModule.PID
 import Mathlib.RingTheory.DedekindDomain.PID
+import Mathlib.RingTheory.DedekindDomain.Instances
 import Mathlib.RingTheory.Localization.NormTrace
 import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
 
@@ -145,12 +146,11 @@ theorem spanIntNorm_localization (I : Ideal S) (M : Submonoid R) (hM : M ≤ R
       Algebra.norm_algebraMap] at has
     apply IsFractionRing.injective Rₘ K
     simp only [map_mul, map_pow]
-    have : FiniteDimensional K L := Module.Finite_of_isLocalization R S _ _ R⁰
+    have : FiniteDimensional K L := .of_isLocalization R S R⁰
     rwa [Algebra.algebraMap_intNorm (L := L), ← IsScalarTower.algebraMap_apply,
       ← IsScalarTower.algebraMap_apply, Algebra.algebraMap_intNorm (L := L)]
   · intro a ha
-    rw [Set.mem_preimage, Function.comp_apply, Algebra.intNorm_eq_of_isLocalization
-      (A := R) (B := S) M (Aₘ := Rₘ) (Bₘ := Sₘ)]
+    rw [Set.mem_preimage, Function.comp_apply, Algebra.intNorm_eq_of_isLocalization M (Bₘ := Sₘ)]
     exact subset_span (Set.mem_image_of_mem _ (mem_map_of_mem _ ha))
 
 theorem spanNorm_mul_spanNorm_le (I J : Ideal S) :
@@ -191,42 +191,10 @@ theorem spanNorm_mul (I J : Ideal S) : spanNorm R (I * J) = spanNorm R I * spanN
     rw [spanNorm_mul_of_bot_or_top]
     intro I
     exact or_iff_not_imp_right.mpr fun hI ↦ (hP.eq_of_le hI bot_le).symm
+  have : NeZero P := ⟨hP0⟩
   let P' := Algebra.algebraMapSubmonoid S P.primeCompl
-  let Rₚ := Localization.AtPrime P
-  let Sₚ := Localization P'
-  let _ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
-  have : IsScalarTower R Rₚ Sₚ :=
-    IsScalarTower.of_algebraMap_eq (fun x =>
-      (IsLocalization.map_eq (T := P') (Q := Localization P') P.primeCompl.le_comap_map x).symm)
-  have h : P' ≤ S⁰ :=
-    map_le_nonZeroDivisors_of_injective _ (FaithfulSMul.algebraMap_injective _ _)
-      P.primeCompl_le_nonZeroDivisors
-  have : IsDomain Sₚ := IsLocalization.isDomain_localization h
-  have : IsDedekindDomain Sₚ := IsLocalization.isDedekindDomain S h _
-  have : IsPrincipalIdealRing Sₚ :=
-    IsDedekindDomain.isPrincipalIdealRing_localization_over_prime S P hP0
-  have := NoZeroSMulDivisors_of_isLocalization R S Rₚ Sₚ P.primeCompl_le_nonZeroDivisors
-  have := Module.Finite_of_isLocalization R S Rₚ Sₚ P.primeCompl
-  let L := FractionRing S
-  let g : Sₚ →+* L := IsLocalization.map _ (M := P') (T := S⁰) (RingHom.id S) h
-  algebraize [g]
-  have : IsScalarTower S Sₚ (FractionRing S) := IsScalarTower.of_algebraMap_eq'
-    (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHom.comp_id])
-  have := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization P' Sₚ (FractionRing S)
-  have : Algebra.IsSeparable (FractionRing Rₚ) (FractionRing Sₚ) := by
-    apply Algebra.IsSeparable.of_equiv_equiv
-      (FractionRing.algEquiv Rₚ (FractionRing R)).symm.toRingEquiv
-      (FractionRing.algEquiv Sₚ (FractionRing S)).symm.toRingEquiv
-    apply IsLocalization.ringHom_ext R⁰
-    ext
-    simp only [AlgEquiv.toRingEquiv_eq_coe, RingHom.coe_comp,
-      RingHom.coe_coe, Function.comp_apply, ← IsScalarTower.algebraMap_apply]
-    rw [IsScalarTower.algebraMap_apply R Rₚ (FractionRing R), AlgEquiv.coe_ringEquiv,
-      AlgEquiv.commutes, IsScalarTower.algebraMap_apply R S L,
-      IsScalarTower.algebraMap_apply S Sₚ L, AlgEquiv.coe_ringEquiv, AlgEquiv.commutes]
-    simp only [← IsScalarTower.algebraMap_apply]
-  simp only [Ideal.map_mul, ← spanIntNorm_localization (R := R) (S := S)
-    (Rₘ := Localization.AtPrime P) (Sₘ := Localization P') _ _ P.primeCompl_le_nonZeroDivisors]
+  simp only [Ideal.map_mul, ← spanIntNorm_localization (R := R) (Sₘ := Localization P')
+    _ _ P.primeCompl_le_nonZeroDivisors]
   rw [← (I.map _).span_singleton_generator, ← (J.map _).span_singleton_generator,
     span_singleton_mul_span_singleton, spanNorm_singleton, spanNorm_singleton,
     spanNorm_singleton, span_singleton_mul_span_singleton, map_mul]