feat: generalize Ideal.spanNorm to allow non free extensions

Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean

@@ -261,4 +261,9 @@ instance integralClosure.isDedekindDomain_fractionRing [IsDedekindDomain A] :
     IsDedekindDomain (integralClosure A L) :=
   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) _ _
+
 end IsIntegralClosure

Mathlib/RingTheory/DedekindDomain/PID.lean

@@ -183,7 +183,7 @@ theorem IsPrincipalIdealRing.of_finite_primes [IsDedekindDomain R]
 
 variable [IsDedekindDomain R]
 variable (S : Type*) [CommRing S]
-variable [Algebra R S] [Module.Free R S] [Module.Finite R S]
+variable [Algebra R S] [NoZeroSMulDivisors R S] [Module.Finite R S]
 variable (p : Ideal R) (hp0 : p ≠ ⊥) [IsPrime p]
 variable {Sₚ : Type*} [CommRing Sₚ] [Algebra S Sₚ]
 variable [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ]

Mathlib/RingTheory/Ideal/Norm/RelNorm.lean

@@ -6,6 +6,7 @@ Authors: Anne Baanen, Alex J. Best
 import Mathlib.LinearAlgebra.FreeModule.PID
 import Mathlib.RingTheory.DedekindDomain.PID
 import Mathlib.RingTheory.Localization.NormTrace
+import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
 
 /-!
 
@@ -34,44 +35,53 @@ namespace Ideal
 
 open Submodule
 
-variable (R : Type*) [CommRing R] {S : Type*} [CommRing S] [Algebra R S]
+attribute [local instance] FractionRing.liftAlgebra
 
-/-- `Ideal.spanNorm R (I : Ideal S)` is the ideal generated by mapping `Algebra.norm R` over `I`.
+variable (R S : Type*) [CommRing R] [IsDomain R] {S : Type*} [CommRing S] [IsDomain S]
+variable [IsIntegrallyClosed R] [IsIntegrallyClosed S] [Algebra R S] [Module.Finite R S]
+variable [NoZeroSMulDivisors R S] [Algebra.IsSeparable (FractionRing R) (FractionRing S)]
+
+/-- `Ideal.spanNorm R (I : Ideal S)` is the ideal generated by mapping `Algebra.intNorm R S`
+over `I`.
 
 See also `Ideal.relNorm`.
 -/
 def spanNorm (I : Ideal S) : Ideal R :=
-  Ideal.span (Algebra.norm R '' (I : Set S))
+  Ideal.span (Algebra.intNorm R S '' (I : Set S))
 
 @[simp]
-theorem spanNorm_bot [Nontrivial S] [Module.Free R S] [Module.Finite R S] :
+theorem spanNorm_bot :
     spanNorm R (⊥ : Ideal S) = ⊥ := span_eq_bot.mpr fun x hx => by simpa using hx
 
 variable {R}
 
 @[simp]
-theorem spanNorm_eq_bot_iff [IsDomain R] [IsDomain S] [Module.Free R S] [Module.Finite R S]
-    {I : Ideal S} : spanNorm R I = ⊥ ↔ I = ⊥ := by
-  simp only [spanNorm, Ideal.span_eq_bot, Set.mem_image, SetLike.mem_coe, forall_exists_index,
-    and_imp, forall_apply_eq_imp_iff₂,
-    Algebra.norm_eq_zero_iff_of_basis (Module.Free.chooseBasis R S), @eq_bot_iff _ _ _ I,
-    SetLike.le_def]
+theorem spanNorm_eq_bot_iff {I : Ideal S} : spanNorm R I = ⊥ ↔ I = ⊥ := by
+  simp only [spanNorm, span_eq_bot, Set.mem_image, SetLike.mem_coe, forall_exists_index, and_imp,
+    forall_apply_eq_imp_iff₂, Algebra.intNorm_eq_zero, @eq_bot_iff _ _ _ I, SetLike.le_def]
   rfl
 
 variable (R)
 
-theorem norm_mem_spanNorm {I : Ideal S} (x : S) (hx : x ∈ I) : Algebra.norm R x ∈ I.spanNorm R :=
+theorem intNorm_mem_spanNorm {I : Ideal S} {x : S} (hx : x ∈ I) :
+    Algebra.intNorm R S x ∈ I.spanNorm R :=
   subset_span (Set.mem_image_of_mem _ hx)
 
+theorem norm_mem_spanNorm [Module.Free R S] {I : Ideal S} (x : S) (hx : x ∈ I) :
+    Algebra.norm R x ∈ I.spanNorm R := by
+  refine subset_span ⟨x, hx, ?_⟩
+  rw [Algebra.intNorm_eq_norm]
+
 @[simp]
-theorem spanNorm_singleton {r : S} : spanNorm R (span ({r} : Set S)) = span {Algebra.norm R r} :=
+theorem spanNorm_singleton {r : S} :
+    spanNorm R (span ({r} : Set S)) = span {Algebra.intNorm R S r} :=
   le_antisymm
     (span_le.mpr fun x hx =>
       mem_span_singleton.mpr
         (by
           obtain ⟨x, hx', rfl⟩ := (Set.mem_image _ _ _).mp hx
           exact map_dvd _ (mem_span_singleton.mp hx')))
-    ((span_singleton_le_iff_mem _).mpr (norm_mem_spanNorm _ _ (mem_span_singleton_self _)))
+    ((span_singleton_le_iff_mem _).mpr (intNorm_mem_spanNorm _ (mem_span_singleton_self _)))
 
 @[simp]
 theorem spanNorm_top : spanNorm R (⊤ : Ideal S) = ⊤ := by
@@ -80,8 +90,8 @@ theorem spanNorm_top : spanNorm R (⊤ : Ideal S) = ⊤ := by
   rw [← Ideal.span_singleton_one, spanNorm_singleton]
   simp
 
-theorem map_spanNorm (I : Ideal S) {T : Type*} [CommRing T] (f : R →+* T) :
-    map f (spanNorm R I) = span (f ∘ Algebra.norm R '' (I : Set S)) := by
+theorem map_spanIntNorm (I : Ideal S) {T : Type*} [CommRing T] (f : R →+* T) :
+    map f (spanNorm R I) = span (f ∘ Algebra.intNorm R S '' (I : Set S)) := by
   rw [spanNorm, map_span, Set.image_image]
   -- Porting note: `Function.comp` reducibility
   rfl
@@ -90,31 +100,63 @@ theorem map_spanNorm (I : Ideal S) {T : Type*} [CommRing T] (f : R →+* T) :
 theorem spanNorm_mono {I J : Ideal S} (h : I ≤ J) : spanNorm R I ≤ spanNorm R J :=
   Ideal.span_mono (Set.monotone_image h)
 
-theorem spanNorm_localization (I : Ideal S) [Module.Finite R S] [Module.Free R S] (M : Submonoid R)
+theorem spanIntNorm_localization (I : Ideal S) (M : Submonoid R) (hM : M ≤ R⁰)
     {Rₘ : Type*} (Sₘ : Type*) [CommRing Rₘ] [Algebra R Rₘ] [CommRing Sₘ] [Algebra S Sₘ]
     [Algebra Rₘ Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ]
-    [IsLocalization M Rₘ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] :
+    [IsLocalization M Rₘ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ]
+    [IsIntegrallyClosed Rₘ] [IsDomain Rₘ] [IsDomain Sₘ] [NoZeroSMulDivisors Rₘ Sₘ]
+    [Module.Finite Rₘ Sₘ] [IsIntegrallyClosed Sₘ]
+    [Algebra.IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)] :
     spanNorm Rₘ (I.map (algebraMap S Sₘ)) = (spanNorm R I).map (algebraMap R Rₘ) := by
-  cases subsingleton_or_nontrivial R
-  · haveI := IsLocalization.unique R Rₘ M
-    simp [eq_iff_true_of_subsingleton]
-  let b := Module.Free.chooseBasis R S
-  rw [map_spanNorm]
+  let K := FractionRing R
+  let f : Rₘ →+* K := IsLocalization.map _ (T := R⁰) (RingHom.id R) hM
+  let L := FractionRing S
+  let g : Sₘ →+* L := IsLocalization.map _ (M := Algebra.algebraMapSubmonoid S M) (T := S⁰)
+      (RingHom.id S) (Submonoid.map_le_of_le_comap _ <| hM.trans
+      (nonZeroDivisors_le_comap_nonZeroDivisors_of_injective _
+        (NoZeroSMulDivisors.algebraMap_injective _ _)))
+  algebraize [f, g, (algebraMap K L).comp f]
+  have : IsScalarTower R Rₘ K := IsScalarTower.of_algebraMap_eq'
+    (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq])
+  let _ := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
+  have : IsScalarTower S Sₘ L := IsScalarTower.of_algebraMap_eq'
+    (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq])
+  have : IsScalarTower Rₘ Sₘ L := by
+    apply IsScalarTower.of_algebraMap_eq'
+    apply IsLocalization.ringHom_ext M
+    rw [RingHom.algebraMap_toAlgebra, RingHom.algebraMap_toAlgebra (R := Sₘ), RingHom.comp_assoc,
+      RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R S Sₘ,
+      IsLocalization.map_comp, RingHom.comp_id, ← RingHom.comp_assoc, IsLocalization.map_comp,
+      RingHom.comp_id, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
+  let _ := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization
+    (Algebra.algebraMapSubmonoid S M) Sₘ L
+  have : IsIntegralClosure Sₘ Rₘ L :=
+    IsIntegralClosure.of_isIntegrallyClosed _ _ _
+  rw [map_spanIntNorm]
   refine span_eq_span (Set.image_subset_iff.mpr ?_) (Set.image_subset_iff.mpr ?_)
-  · rintro a' ha'
-    simp only [Set.mem_preimage, submodule_span_eq, ← map_spanNorm, SetLike.mem_coe,
+  · intro a' ha'
+    simp only [Set.mem_preimage, submodule_span_eq, ← map_spanIntNorm, SetLike.mem_coe,
       IsLocalization.mem_map_algebraMap_iff (Algebra.algebraMapSubmonoid S M) Sₘ,
       IsLocalization.mem_map_algebraMap_iff M Rₘ, Prod.exists] at ha' ⊢
     obtain ⟨⟨a, ha⟩, ⟨_, ⟨s, hs, rfl⟩⟩, has⟩ := ha'
-    refine ⟨⟨Algebra.norm R a, norm_mem_spanNorm _ _ ha⟩,
-      ⟨s ^ Fintype.card (Module.Free.ChooseBasisIndex R S), pow_mem hs _⟩, ?_⟩
+    refine ⟨⟨Algebra.intNorm R S a, intNorm_mem_spanNorm _ ha⟩,
+      ⟨s ^ Module.finrank K L, pow_mem hs _⟩, ?_⟩
     simp only [Submodule.coe_mk, Subtype.coe_mk, map_pow] at has ⊢
-    apply_fun Algebra.norm Rₘ at has
-    rwa [_root_.map_mul, ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R Rₘ,
-      Algebra.norm_algebraMap_of_basis (b.localizationLocalization Rₘ M Sₘ),
-      Algebra.norm_localization R M a] at has
+    apply_fun algebraMap _ L at has
+    apply_fun Algebra.norm K at has
+    simp only [_root_.map_mul, IsScalarTower.algebraMap_apply R Rₘ Sₘ] at has
+    rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply,
+      ← IsScalarTower.algebraMap_apply,
+      IsScalarTower.algebraMap_apply R K L,
+      Algebra.norm_algebraMap] at has
+    apply IsFractionRing.injective Rₘ K
+    simp only [_root_.map_mul, map_pow]
+    have : FiniteDimensional K L := Module.Finite_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.norm_localization (Sₘ := Sₘ) R M a]
+    rw [Set.mem_preimage, Function.comp_apply, Algebra.intNorm_eq_of_isLocalization
+      (A := R) (B := S) M (Aₘ := Rₘ) (Bₘ := Sₘ)]
     exact subset_span (Set.mem_image_of_mem _ (mem_map_of_mem _ ha))
 
 theorem spanNorm_mul_spanNorm_le (I J : Ideal S) :
@@ -127,60 +169,73 @@ theorem spanNorm_mul_spanNorm_le (I J : Ideal S) :
 /-- This condition `eq_bot_or_top` is equivalent to being a field.
 However, `Ideal.spanNorm_mul_of_field` is harder to apply since we'd need to upgrade a `CommRing R`
 instance to a `Field R` instance. -/
-theorem spanNorm_mul_of_bot_or_top [IsDomain R] [IsDomain S] [Module.Free R S] [Module.Finite R S]
-    (eq_bot_or_top : ∀ I : Ideal R, I = ⊥ ∨ I = ⊤) (I J : Ideal S) :
+theorem spanNorm_mul_of_bot_or_top (eq_bot_or_top : ∀ I : Ideal R, I = ⊥ ∨ I = ⊤) (I J : Ideal S) :
     spanNorm R (I * J) = spanNorm R I * spanNorm R J := by
   refine le_antisymm ?_ (spanNorm_mul_spanNorm_le R _ _)
-  cases' eq_bot_or_top (spanNorm R I) with hI hI
+  rcases eq_bot_or_top (spanNorm R I) with hI | hI
   · rw [hI, spanNorm_eq_bot_iff.mp hI, bot_mul, spanNorm_bot]
     exact bot_le
   rw [hI, Ideal.top_mul]
-  cases' eq_bot_or_top (spanNorm R J) with hJ hJ
+  rcases eq_bot_or_top (spanNorm R J) with hJ | hJ
   · rw [hJ, spanNorm_eq_bot_iff.mp hJ, mul_bot, spanNorm_bot]
   rw [hJ]
   exact le_top
 
-@[simp]
-theorem spanNorm_mul_of_field {K : Type*} [Field K] [Algebra K S] [IsDomain S] [Module.Finite K S]
-    (I J : Ideal S) : spanNorm K (I * J) = spanNorm K I * spanNorm K J :=
-  spanNorm_mul_of_bot_or_top K eq_bot_or_top I J
-
-variable [IsDomain R] [IsDomain S] [IsDedekindDomain R] [IsDedekindDomain S]
-variable [Module.Finite R S] [Module.Free R S]
+variable [IsDedekindDomain R] [IsDedekindDomain S]
 
 /-- Multiplicativity of `Ideal.spanNorm`. simp-normal form is `map_mul (Ideal.relNorm R)`. -/
 theorem spanNorm_mul (I J : Ideal S) : spanNorm R (I * J) = spanNorm R I * spanNorm R J := by
   nontriviality R
   cases subsingleton_or_nontrivial S
-  · have : ∀ I : Ideal S, I = ⊤ := fun I => Subsingleton.elim I ⊤
+  · have : ∀ I : Ideal S, I = ⊤ := fun I ↦ Subsingleton.elim I ⊤
     simp [this I, this J, this (I * J)]
-  refine eq_of_localization_maximal ?_
-  intro P hP
+  refine eq_of_localization_maximal (fun P hP ↦ ?_)
   by_cases hP0 : P = ⊥
   · subst hP0
     rw [spanNorm_mul_of_bot_or_top]
     intro I
-    refine or_iff_not_imp_right.mpr fun hI => ?_
-    exact (hP.eq_of_le hI bot_le).symm
+    exact or_iff_not_imp_right.mpr fun hI ↦ (hP.eq_of_le hI bot_le).symm
   let P' := Algebra.algebraMapSubmonoid S P.primeCompl
-  letI : Algebra (Localization.AtPrime P) (Localization P') := localizationAlgebra P.primeCompl S
-  haveI : IsScalarTower R (Localization.AtPrime P) (Localization P') :=
+  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 _ (NoZeroSMulDivisors.algebraMap_injective _ _)
       P.primeCompl_le_nonZeroDivisors
-  haveI : IsDomain (Localization P') := IsLocalization.isDomain_localization h
-  haveI : IsDedekindDomain (Localization P') := IsLocalization.isDedekindDomain S h _
-  letI := Classical.decEq (Ideal (Localization P'))
-  haveI : IsPrincipalIdealRing (Localization P') :=
+  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
-  rw [Ideal.map_mul, ← spanNorm_localization R I P.primeCompl (Localization P'),
-    ← spanNorm_localization R J P.primeCompl (Localization P'),
-    ← spanNorm_localization R (I * J) P.primeCompl (Localization P'), Ideal.map_mul,
-    ← (I.map _).span_singleton_generator, ← (J.map _).span_singleton_generator,
+  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]
+    simp only [IsScalarTower.algebraMap_apply R Rₚ (FractionRing R), AlgEquiv.coe_ringEquiv,
+      AlgEquiv.commutes, IsScalarTower.algebraMap_apply R S L,
+      IsScalarTower.algebraMap_apply S Sₚ L]
+    simp only [← IsScalarTower.algebraMap_apply]
+    rw [IsScalarTower.algebraMap_apply R Rₚ (FractionRing Rₚ),
+      ← IsScalarTower.algebraMap_apply Rₚ, ← 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]
+  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, _root_.map_mul]
+      spanNorm_singleton, span_singleton_mul_span_singleton, _root_.map_mul]
 
 /-- The relative norm `Ideal.relNorm R (I : Ideal S)`, where `R` and `S` are Dedekind domains,
 and `S` is an extension of `R` that is finite and free as a module. -/
@@ -190,7 +245,8 @@ def relNorm : Ideal S →*₀ Ideal R where
   map_one' := by dsimp only; rw [one_eq_top, spanNorm_top R, one_eq_top]
   map_mul' := spanNorm_mul R
 
-theorem relNorm_apply (I : Ideal S) : relNorm R I = span (Algebra.norm R '' (I : Set S) : Set R) :=
+theorem relNorm_apply (I : Ideal S) :
+    relNorm R I = span (Algebra.intNorm R S '' (I : Set S) : Set R) :=
   rfl
 
 @[simp]
@@ -212,16 +268,17 @@ theorem relNorm_eq_bot_iff {I : Ideal S} : relNorm R I = ⊥ ↔ I = ⊥ :=
 
 variable (R)
 
-theorem norm_mem_relNorm (I : Ideal S) {x : S} (hx : x ∈ I) : Algebra.norm R x ∈ relNorm R I :=
+theorem norm_mem_relNorm [Module.Free R S] (I : Ideal S) {x : S} (hx : x ∈ I) :
+    Algebra.norm R x ∈ relNorm R I :=
   norm_mem_spanNorm R x hx
 
 @[simp]
-theorem relNorm_singleton (r : S) : relNorm R (span ({r} : Set S)) = span {Algebra.norm R r} :=
+theorem relNorm_singleton (r : S) : relNorm R (span ({r} : Set S)) = span {Algebra.intNorm R S r} :=
   spanNorm_singleton R
 
 theorem map_relNorm (I : Ideal S) {T : Type*} [CommRing T] (f : R →+* T) :
-    map f (relNorm R I) = span (f ∘ Algebra.norm R '' (I : Set S)) :=
-  map_spanNorm R I f
+    map f (relNorm R I) = span (f ∘ Algebra.intNorm R S '' (I : Set S)) :=
+  map_spanIntNorm R I f
 
 @[mono]
 theorem relNorm_mono {I J : Ideal S} (h : I ≤ J) : relNorm R I ≤ relNorm R J :=

Mathlib/RingTheory/Localization/Ideal.lean

@@ -6,6 +6,7 @@ Authors: Kenny Lau, Mario Carneiro, Johan Commelin, Amelia Livingston, Anne Baan
 import Mathlib.GroupTheory.MonoidLocalization.Away
 import Mathlib.RingTheory.Ideal.Quotient.Operations
 import Mathlib.RingTheory.Localization.Defs
+import Mathlib.Algebra.Algebra.Tower
 
 /-!
 # Ideals in localizations of commutative rings
@@ -242,6 +243,32 @@ theorem ideal_eq_iInf_comap_map_away {S : Finset R} (hS : Ideal.span (α := R) S
     rw [pow_add, mul_assoc, ← mul_comm x, e]
     exact I.mul_mem_left _ y.2
 
+variable (R) in
+lemma _root_.NoZeroSMulDivisors_of_isLocalization (Rₚ Sₚ : Type*) [CommRing Rₚ] [CommRing Sₚ]
+    [Algebra R Rₚ] [Algebra R Sₚ] [Algebra S Sₚ] [Algebra Rₚ Sₚ] [IsScalarTower R S Sₚ]
+    [IsScalarTower R Rₚ Sₚ] {M : Submonoid R} (hM : M ≤ R⁰) [IsLocalization M Rₚ]
+    [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ] [NoZeroSMulDivisors R S] [IsDomain S] :
+    NoZeroSMulDivisors Rₚ Sₚ := by
+  have e : Algebra.algebraMapSubmonoid S M ≤ S⁰ :=
+    Submonoid.map_le_of_le_comap _ <| hM.trans
+      (nonZeroDivisors_le_comap_nonZeroDivisors_of_injective _
+        (NoZeroSMulDivisors.algebraMap_injective _ _))
+  have : IsDomain Sₚ := IsLocalization.isDomain_of_le_nonZeroDivisors S e
+  have : algebraMap Rₚ Sₚ = IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ
+    (algebraMap R S) (Submonoid.le_comap_map M) := by
+    apply IsLocalization.ringHom_ext M
+    simp only [IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
+  rw [NoZeroSMulDivisors.iff_algebraMap_injective, RingHom.injective_iff_ker_eq_bot,
+    RingHom.ker_eq_bot_iff_eq_zero]
+  intro x hx
+  obtain ⟨x, s, rfl⟩ := IsLocalization.mk'_surjective M x
+  simp only [RingHom.algebraMap_toAlgebra, IsLocalization.map_mk', IsLocalization.mk'_eq_zero_iff,
+    Subtype.exists, exists_prop, this] at hx ⊢
+  obtain ⟨_, ⟨a, ha, rfl⟩, H⟩ := hx
+  simp only [← _root_.map_mul,
+    (injective_iff_map_eq_zero' _).mp (NoZeroSMulDivisors.algebraMap_injective R S)] at H
+  exact ⟨a, ha, H⟩
+
 end CommRing
 
 end IsLocalization