Merge remote-tracking branch 'upstream/master' into HomeomorphClass

Mathlib.lean

@@ -507,8 +507,11 @@ import Mathlib.Algebra.Module.LinearMap.Polynomial
 import Mathlib.Algebra.Module.LinearMap.Prod
 import Mathlib.Algebra.Module.LinearMap.Rat
 import Mathlib.Algebra.Module.LinearMap.Star
-import Mathlib.Algebra.Module.LocalizedModule
-import Mathlib.Algebra.Module.LocalizedModuleIntegers
+import Mathlib.Algebra.Module.LocalizedModule.Basic
+import Mathlib.Algebra.Module.LocalizedModule.Exact
+import Mathlib.Algebra.Module.LocalizedModule.Int
+import Mathlib.Algebra.Module.LocalizedModule.IsLocalization
+import Mathlib.Algebra.Module.LocalizedModule.Submodule
 import Mathlib.Algebra.Module.MinimalAxioms
 import Mathlib.Algebra.Module.Opposite
 import Mathlib.Algebra.Module.PID
@@ -532,7 +535,6 @@ import Mathlib.Algebra.Module.Submodule.IterateMapComap
 import Mathlib.Algebra.Module.Submodule.Ker
 import Mathlib.Algebra.Module.Submodule.Lattice
 import Mathlib.Algebra.Module.Submodule.LinearMap
-import Mathlib.Algebra.Module.Submodule.Localization
 import Mathlib.Algebra.Module.Submodule.Map
 import Mathlib.Algebra.Module.Submodule.Order
 import Mathlib.Algebra.Module.Submodule.Pointwise
@@ -1393,6 +1395,8 @@ import Mathlib.Analysis.ODE.PicardLindelof
 import Mathlib.Analysis.Oscillation
 import Mathlib.Analysis.PSeries
 import Mathlib.Analysis.PSeriesComplex
+import Mathlib.Analysis.Polynomial.Basic
+import Mathlib.Analysis.Polynomial.CauchyBound
 import Mathlib.Analysis.Quaternion
 import Mathlib.Analysis.RCLike.Basic
 import Mathlib.Analysis.RCLike.Inner
@@ -1438,7 +1442,6 @@ import Mathlib.Analysis.SpecialFunctions.NonIntegrable
 import Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
 import Mathlib.Analysis.SpecialFunctions.PolarCoord
 import Mathlib.Analysis.SpecialFunctions.PolynomialExp
-import Mathlib.Analysis.SpecialFunctions.Polynomials
 import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
 import Mathlib.Analysis.SpecialFunctions.Pow.Complex
 import Mathlib.Analysis.SpecialFunctions.Pow.Continuity
@@ -4280,6 +4283,7 @@ import Mathlib.RingTheory.RingHomProperties
 import Mathlib.RingTheory.RingInvo
 import Mathlib.RingTheory.RootsOfUnity.Basic
 import Mathlib.RingTheory.RootsOfUnity.Complex
+import Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
 import Mathlib.RingTheory.RootsOfUnity.Lemmas
 import Mathlib.RingTheory.RootsOfUnity.Minpoly
 import Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Mathlib/Algebra/BigOperators/Pi.lean

@@ -145,3 +145,39 @@ theorem snd_prod : (∏ c ∈ s, f c).2 = ∏ c ∈ s, (f c).2 :=
   map_prod (MonoidHom.snd α β) f s
 
 end Prod
+
+section MulEquiv
+
+/-- The canonical isomorphism between the monoid of homomorphisms from a finite product of
+commutative monoids to another commutative monoid and the product of the homomorphism monoids. -/
+@[to_additive "The canonical isomorphism between the additive monoid of homomorphisms from
+a finite product of additive commutative monoids to another additive commutative monoid and
+the product of the homomorphism monoids."]
+def Pi.monoidHomMulEquiv {ι : Type*} [Fintype ι] [DecidableEq ι] (M : ι → Type*)
+    [(i : ι) → CommMonoid (M i)] (M' : Type*) [CommMonoid M'] :
+    (((i : ι) → M i) →* M') ≃* ((i : ι) → (M i →* M')) where
+      toFun φ i := φ.comp <| MonoidHom.mulSingle M i
+      invFun φ := ∏ (i : ι), (φ i).comp (Pi.evalMonoidHom M i)
+      left_inv φ := by
+        ext
+        simp only [MonoidHom.finset_prod_apply, MonoidHom.coe_comp, Function.comp_apply,
+          evalMonoidHom_apply, MonoidHom.mulSingle_apply, ← map_prod]
+        refine congrArg _ <| funext fun _ ↦ ?_
+        rw [Fintype.prod_apply]
+        exact Fintype.prod_pi_mulSingle ..
+      right_inv φ := by
+        ext i m
+        simp only [MonoidHom.coe_comp, Function.comp_apply, MonoidHom.mulSingle_apply,
+          MonoidHom.finset_prod_apply, evalMonoidHom_apply, ]
+        let φ' i : M i → M' := ⇑(φ i)
+        conv =>
+          enter [1, 2, j]
+          rw [show φ j = φ' j from rfl, Pi.apply_mulSingle φ' (fun i ↦ map_one (φ i))]
+        rw [show φ' i = φ i from rfl]
+        exact Fintype.prod_pi_mulSingle' ..
+      map_mul' φ ψ := by
+        ext
+        simp only [MonoidHom.coe_comp, Function.comp_apply, MonoidHom.mulSingle_apply,
+          MonoidHom.mul_apply, mul_apply]
+
+end MulEquiv

Mathlib/Algebra/GeomSum.lean

@@ -163,6 +163,22 @@ theorem geom_sum₂_mul [CommRing α] (x y : α) (n : ℕ) :
     (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n :=
   (Commute.all x y).geom_sum₂_mul n
 
+theorem geom_sum₂_mul_of_ge [CommSemiring α] [PartialOrder α] [AddLeftReflectLE α] [AddLeftMono α]
+    [ExistsAddOfLE α] [Sub α] [OrderedSub α] {x y : α} (hxy : y ≤ x) (n : ℕ) :
+    (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n := by
+  apply eq_tsub_of_add_eq
+  simpa only [tsub_add_cancel_of_le hxy] using geom_sum₂_mul_add (x - y) y n
+
+theorem geom_sum₂_mul_of_le [CommSemiring α] [PartialOrder α] [AddLeftReflectLE α] [AddLeftMono α]
+    [ExistsAddOfLE α] [Sub α] [OrderedSub α] {x y : α} (hxy : x ≤ y) (n : ℕ) :
+    (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (y - x) = y ^ n - x ^ n := by
+  rw [← Finset.sum_range_reflect]
+  convert geom_sum₂_mul_of_ge hxy n using 3
+  simp_all only [Finset.mem_range]
+  rw [mul_comm]
+  congr
+  omega
+
 theorem Commute.sub_dvd_pow_sub_pow [Ring α] {x y : α} (h : Commute x y) (n : ℕ) :
     x - y ∣ x ^ n - y ^ n :=
   Dvd.intro _ <| h.mul_geom_sum₂ _
@@ -211,6 +227,16 @@ theorem geom_sum_mul [Ring α] (x : α) (n : ℕ) : (∑ i ∈ range n, x ^ i) *
   rw [one_pow, geom_sum₂_with_one] at this
   exact this
 
+theorem geom_sum_mul_of_one_le [CommSemiring α] [PartialOrder α] [AddLeftReflectLE α]
+    [AddLeftMono α] [ExistsAddOfLE α] [Sub α] [OrderedSub α] {x : α} (hx : 1 ≤ x) (n : ℕ) :
+    (∑ i ∈ range n, x ^ i) * (x - 1) = x ^ n - 1 := by
+  simpa using geom_sum₂_mul_of_ge hx n
+
+theorem geom_sum_mul_of_le_one [CommSemiring α] [PartialOrder α] [AddLeftReflectLE α]
+    [AddLeftMono α] [ExistsAddOfLE α] [Sub α] [OrderedSub α] {x : α} (hx : x ≤ 1) (n : ℕ) :
+    (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n := by
+  simpa using geom_sum₂_mul_of_le hx n
+
 theorem mul_geom_sum [Ring α] (x : α) (n : ℕ) : ((x - 1) * ∑ i ∈ range n, x ^ i) = x ^ n - 1 :=
   op_injective <| by simpa using geom_sum_mul (op x) n
 
@@ -245,11 +271,31 @@ theorem geom₂_sum [Field α] {x y : α} (h : x ≠ y) (n : ℕ) :
     ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y) :=
   (Commute.all x y).geom_sum₂ h n
 
+theorem geom₂_sum_of_gt {α : Type*} [CanonicallyLinearOrderedSemifield α] [Sub α] [OrderedSub α]
+    {x y : α} (h : y < x) (n : ℕ) :
+    ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y) :=
+  eq_div_of_mul_eq (tsub_pos_of_lt h).ne' (geom_sum₂_mul_of_ge h.le n)
+
+theorem geom₂_sum_of_lt {α : Type*} [CanonicallyLinearOrderedSemifield α] [Sub α] [OrderedSub α]
+    {x y : α} (h : x < y) (n : ℕ) :
+    ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (y ^ n - x ^ n) / (y - x) :=
+  eq_div_of_mul_eq (tsub_pos_of_lt h).ne' (geom_sum₂_mul_of_le h.le n)
+
 theorem geom_sum_eq [DivisionRing α] {x : α} (h : x ≠ 1) (n : ℕ) :
     ∑ i ∈ range n, x ^ i = (x ^ n - 1) / (x - 1) := by
   have : x - 1 ≠ 0 := by simp_all [sub_eq_iff_eq_add]
   rw [← geom_sum_mul, mul_div_cancel_right₀ _ this]
 
+lemma geom_sum_of_one_lt {x : α} [CanonicallyLinearOrderedSemifield α] [Sub α] [OrderedSub α]
+    (h : 1 < x) (n : ℕ) :
+    ∑ i ∈ Finset.range n, x ^ i = (x ^ n - 1) / (x - 1) :=
+  eq_div_of_mul_eq (tsub_pos_of_lt h).ne' (geom_sum_mul_of_one_le h.le n)
+
+lemma geom_sum_of_lt_one {x : α} [CanonicallyLinearOrderedSemifield α] [Sub α] [OrderedSub α]
+    (h : x < 1) (n : ℕ) :
+    ∑ i ∈ Finset.range n, x ^ i = (1 - x ^ n) / (1 - x) :=
+  eq_div_of_mul_eq (tsub_pos_of_lt h).ne' (geom_sum_mul_of_le_one h.le n)
+
 protected theorem Commute.mul_geom_sum₂_Ico [Ring α] {x y : α} (h : Commute x y) {m n : ℕ}
     (hmn : m ≤ n) :
     ((x - y) * ∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i)) = x ^ n - x ^ m * y ^ (n - m) := by

Mathlib/Algebra/Group/TypeTags.lean

@@ -554,3 +554,21 @@ is often used for composition, without affecting the behavior of the function it
 instance Multiplicative.coeToFun {α : Type*} {β : α → Sort*} [CoeFun α β] :
     CoeFun (Multiplicative α) fun a => β (toAdd a) :=
   ⟨fun a => CoeFun.coe (toAdd a)⟩
+
+lemma Pi.mulSingle_multiplicativeOfAdd_eq {ι : Type*} [DecidableEq ι] {M : ι → Type*}
+    [(i : ι) → AddMonoid (M i)] (i : ι) (a : M i) (j : ι) :
+    Pi.mulSingle (f := fun i ↦ Multiplicative (M i)) i (Multiplicative.ofAdd a) j =
+      Multiplicative.ofAdd ((Pi.single i a) j) := by
+  rcases eq_or_ne j i with rfl | h
+  · simp only [mulSingle_eq_same, single_eq_same]
+  · simp only [mulSingle, ne_eq, h, not_false_eq_true, Function.update_noteq, one_apply, single,
+      zero_apply, ofAdd_zero]
+
+lemma Pi.single_additiveOfMul_eq {ι : Type*} [DecidableEq ι] {M : ι → Type*}
+    [(i : ι) → Monoid (M i)] (i : ι) (a : M i) (j : ι) :
+    Pi.single (f := fun i ↦ Additive (M i)) i (Additive.ofMul a) j =
+      Additive.ofMul ((Pi.mulSingle i a) j) := by
+  rcases eq_or_ne j i with rfl | h
+  · simp only [mulSingle_eq_same, single_eq_same]
+  · simp only [single, ne_eq, h, not_false_eq_true, Function.update_noteq, zero_apply, mulSingle,
+      one_apply, ofMul_one]

Mathlib/Algebra/Module/LocalizedModule.lean → Mathlib/Algebra/Module/LocalizedModule/Basic.lean

@@ -3,8 +3,6 @@ Copyright (c) 2022 Jujian Zhang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang, Jujian Zhang
 -/
-import Mathlib.Algebra.Algebra.Bilinear
-import Mathlib.Algebra.Exact
 import Mathlib.Algebra.Algebra.Tower
 import Mathlib.RingTheory.Localization.Defs
 
@@ -586,34 +584,6 @@ lemma isLocalizedModule_id (R') [CommSemiring R'] [Algebra R R'] [IsLocalization
   surj' m := ⟨(m, 1), one_smul _ _⟩
   exists_of_eq h := ⟨1, congr_arg _ h⟩
 
-variable {S} in
-theorem isLocalizedModule_iff_isLocalization {A Aₛ} [CommSemiring A] [Algebra R A] [CommSemiring Aₛ]
-    [Algebra A Aₛ] [Algebra R Aₛ] [IsScalarTower R A Aₛ] :
-    IsLocalizedModule S (IsScalarTower.toAlgHom R A Aₛ).toLinearMap ↔
-      IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ := by
-  rw [isLocalizedModule_iff, isLocalization_iff]
-  refine and_congr ?_ (and_congr (forall_congr' fun _ ↦ ?_) (forall₂_congr fun _ _ ↦ ?_))
-  · simp_rw [← (Algebra.lmul R Aₛ).commutes, Algebra.lmul_isUnit_iff, Subtype.forall,
-      Algebra.algebraMapSubmonoid, ← SetLike.mem_coe, Submonoid.coe_map,
-      Set.forall_mem_image, ← IsScalarTower.algebraMap_apply]
-  · simp_rw [Prod.exists, Subtype.exists, Algebra.algebraMapSubmonoid]
-    simp [← IsScalarTower.algebraMap_apply, Submonoid.mk_smul, Algebra.smul_def, mul_comm]
-  · congr!; simp_rw [Subtype.exists, Algebra.algebraMapSubmonoid]; simp [Algebra.smul_def]
-
-instance {A Aₛ} [CommSemiring A] [Algebra R A][CommSemiring Aₛ] [Algebra A Aₛ] [Algebra R Aₛ]
-    [IsScalarTower R A Aₛ] [h : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ] :
-    IsLocalizedModule S (IsScalarTower.toAlgHom R A Aₛ).toLinearMap :=
-  isLocalizedModule_iff_isLocalization.mpr h
-
-lemma isLocalizedModule_iff_isLocalization' (R') [CommSemiring R'] [Algebra R R'] :
-    IsLocalizedModule S (Algebra.ofId R R').toLinearMap ↔ IsLocalization S R' := by
-  convert isLocalizedModule_iff_isLocalization (S := S) (A := R) (Aₛ := R')
-  exact (Submonoid.map_id S).symm
-
-instance {A} [CommRing A] [Algebra R A] [IsLocalization S A] :
-    IsLocalizedModule S (Algebra.linearMap R A) :=
-  (isLocalizedModule_iff_isLocalization' S _).mpr inferInstance
-
 namespace LocalizedModule
 
 /--
@@ -1176,36 +1146,6 @@ lemma map_iso_commute (g : M₀ →ₗ[R] M₁) : (map S f₀ f₁) g ∘ₗ (is
 
 end IsLocalizedModule
 
-namespace LocalizedModule
-
-open IsLocalizedModule LocalizedModule Function Submonoid
-
-variable {M₀ M₀'} [AddCommMonoid M₀] [Module R M₀]
-variable {M₁ M₁'} [AddCommMonoid M₁] [Module R M₁]
-variable {M₂ M₂'} [AddCommMonoid M₂] [Module R M₂]
-
-/-- Localization of modules is an exact functor, proven here for `LocalizedModule`.
-See `IsLocalizedModule.map_exact` for the more general version. -/
-lemma map_exact (g : M₀ →ₗ[R] M₁) (h : M₁ →ₗ[R] M₂) (ex : Exact g h) :
-    Exact (map S (mkLinearMap S M₀) (mkLinearMap S M₁) g)
-    (map S (mkLinearMap S M₁) (mkLinearMap S M₂) h) :=
-  fun y ↦ Iff.intro
-    (induction_on
-      (fun m s hy ↦ by
-        rw [map_LocalizedModules, ← zero_mk 1, mk_eq, one_smul, smul_zero] at hy
-        obtain ⟨a, aS, ha⟩ := Subtype.exists.1 hy
-        rw [smul_zero, mk_smul, ← LinearMap.map_smul, ex (a • m)] at ha
-        rcases ha with ⟨x, hx⟩
-        use mk x (⟨a, aS⟩ * s)
-        rw [map_LocalizedModules, hx, ← mk_cancel_common_left ⟨a, aS⟩ s m, mk_smul])
-      y)
-    fun ⟨x, hx⟩ ↦ by
-      revert hx
-      refine induction_on (fun m s hx ↦ ?_) x
-      rw [← hx, map_LocalizedModules, map_LocalizedModules, (ex (g m)).2 ⟨m, rfl⟩, zero_mk]
-
-end LocalizedModule
-
 namespace IsLocalizedModule
 
 variable {M₀ M₀'} [AddCommMonoid M₀] [AddCommMonoid M₀'] [Module R M₀] [Module R M₀']
@@ -1215,12 +1155,6 @@ variable (f₁ : M₁ →ₗ[R] M₁') [IsLocalizedModule S f₁]
 variable {M₂ M₂'} [AddCommMonoid M₂] [AddCommMonoid M₂'] [Module R M₂] [Module R M₂']
 variable (f₂ : M₂ →ₗ[R] M₂') [IsLocalizedModule S f₂]
 
-/-- Localization of modules is an exact functor. -/
-theorem map_exact (g : M₀ →ₗ[R] M₁) (h : M₁ →ₗ[R] M₂) (ex : Function.Exact g h) :
-    Function.Exact (map S f₀ f₁ g) (map S f₁ f₂ h) :=
-  Function.Exact.of_ladder_linearEquiv_of_exact
-    (map_iso_commute S f₀ f₁ g) (map_iso_commute S f₁ f₂ h) (LocalizedModule.map_exact S g h ex)
-
 /-- Localization of composition is the composition of localization -/
 theorem map_comp' (g : M₀ →ₗ[R] M₁) (h : M₁ →ₗ[R] M₂) :
     map S f₀ f₂ (h ∘ₗ g) = map S f₁ f₂ h ∘ₗ map S f₀ f₁ g := by

Mathlib/Algebra/Module/LocalizedModule/Exact.lean

@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2022 Jujian Zhang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang, Jujian Zhang
+-/
+import Mathlib.Algebra.Exact
+import Mathlib.Algebra.Module.LocalizedModule.Basic
+
+/-!
+# Localization of modules is an exact functor
+
+## Main definitions
+
+- `LocalizedModule.map_exact`: Localization of modules is an exact functor.
+- `IsLocalizedModule.map_exact`: A variant expressed in terms of `IsLocalizedModule`.
+
+-/
+
+section
+
+open IsLocalizedModule Function Submonoid
+
+variable {R : Type*} [CommSemiring R] (S : Submonoid R)
+variable {M₀ M₀'} [AddCommMonoid M₀] [AddCommMonoid M₀'] [Module R M₀] [Module R M₀']
+variable (f₀ : M₀ →ₗ[R] M₀') [IsLocalizedModule S f₀]
+variable {M₁ M₁'} [AddCommMonoid M₁] [AddCommMonoid M₁'] [Module R M₁] [Module R M₁']
+variable (f₁ : M₁ →ₗ[R] M₁') [IsLocalizedModule S f₁]
+variable {M₂ M₂'} [AddCommMonoid M₂] [AddCommMonoid M₂'] [Module R M₂] [Module R M₂']
+variable (f₂ : M₂ →ₗ[R] M₂') [IsLocalizedModule S f₂]
+
+/-- Localization of modules is an exact functor, proven here for `LocalizedModule`.
+See `IsLocalizedModule.map_exact` for the more general version. -/
+lemma LocalizedModule.map_exact (g : M₀ →ₗ[R] M₁) (h : M₁ →ₗ[R] M₂) (ex : Exact g h) :
+    Exact (map S (mkLinearMap S M₀) (mkLinearMap S M₁) g)
+    (map S (mkLinearMap S M₁) (mkLinearMap S M₂) h) :=
+  fun y ↦ Iff.intro
+    (induction_on
+      (fun m s hy ↦ by
+        rw [map_LocalizedModules, ← zero_mk 1, mk_eq, one_smul, smul_zero] at hy
+        obtain ⟨a, aS, ha⟩ := Subtype.exists.1 hy
+        rw [smul_zero, mk_smul, ← LinearMap.map_smul, ex (a • m)] at ha
+        rcases ha with ⟨x, hx⟩
+        use mk x (⟨a, aS⟩ * s)
+        rw [map_LocalizedModules, hx, ← mk_cancel_common_left ⟨a, aS⟩ s m, mk_smul])
+      y)
+    fun ⟨x, hx⟩ ↦ by
+      revert hx
+      refine induction_on (fun m s hx ↦ ?_) x
+      rw [← hx, map_LocalizedModules, map_LocalizedModules, (ex (g m)).2 ⟨m, rfl⟩, zero_mk]
+
+/-- Localization of modules is an exact functor. -/
+theorem IsLocalizedModule.map_exact (g : M₀ →ₗ[R] M₁) (h : M₁ →ₗ[R] M₂) (ex : Function.Exact g h) :
+    Function.Exact (map S f₀ f₁ g) (map S f₁ f₂ h) :=
+  Function.Exact.of_ladder_linearEquiv_of_exact
+    (map_iso_commute S f₀ f₁ g) (map_iso_commute S f₁ f₂ h) (LocalizedModule.map_exact S g h ex)
+
+end

Mathlib/Algebra/Module/LocalizedModuleIntegers.lean → Mathlib/Algebra/Module/LocalizedModule/Int.lean

@@ -3,7 +3,7 @@ Copyright (c) 2024 Christian Merten. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Christian Merten
 -/
-import Mathlib.Algebra.Module.LocalizedModule
+import Mathlib.Algebra.Module.LocalizedModule.Basic
 import Mathlib.Algebra.Module.Submodule.Pointwise
 
 /-!

Mathlib/Algebra/Module/LocalizedModule/IsLocalization.lean

@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2022 Jujian Zhang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang, Jujian Zhang
+-/
+import Mathlib.Algebra.Algebra.Bilinear
+import Mathlib.Algebra.Module.LocalizedModule.Basic
+
+/-!
+# Equivalence between `IsLocalizedModule` and `IsLocalization`
+-/
+
+section IsLocalizedModule
+
+variable {R : Type*} [CommSemiring R] (S : Submonoid R)
+
+variable {S} in
+theorem isLocalizedModule_iff_isLocalization {A Aₛ} [CommSemiring A] [Algebra R A] [CommSemiring Aₛ]
+    [Algebra A Aₛ] [Algebra R Aₛ] [IsScalarTower R A Aₛ] :
+    IsLocalizedModule S (IsScalarTower.toAlgHom R A Aₛ).toLinearMap ↔
+      IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ := by
+  rw [isLocalizedModule_iff, isLocalization_iff]
+  refine and_congr ?_ (and_congr (forall_congr' fun _ ↦ ?_) (forall₂_congr fun _ _ ↦ ?_))
+  · simp_rw [← (Algebra.lmul R Aₛ).commutes, Algebra.lmul_isUnit_iff, Subtype.forall,
+      Algebra.algebraMapSubmonoid, ← SetLike.mem_coe, Submonoid.coe_map,
+      Set.forall_mem_image, ← IsScalarTower.algebraMap_apply]
+  · simp_rw [Prod.exists, Subtype.exists, Algebra.algebraMapSubmonoid]
+    simp [← IsScalarTower.algebraMap_apply, Submonoid.mk_smul, Algebra.smul_def, mul_comm]
+  · congr!; simp_rw [Subtype.exists, Algebra.algebraMapSubmonoid]; simp [Algebra.smul_def]
+
+instance {A Aₛ} [CommSemiring A] [Algebra R A][CommSemiring Aₛ] [Algebra A Aₛ] [Algebra R Aₛ]
+    [IsScalarTower R A Aₛ] [h : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ] :
+    IsLocalizedModule S (IsScalarTower.toAlgHom R A Aₛ).toLinearMap :=
+  isLocalizedModule_iff_isLocalization.mpr h
+
+lemma isLocalizedModule_iff_isLocalization' (R') [CommSemiring R'] [Algebra R R'] :
+    IsLocalizedModule S (Algebra.ofId R R').toLinearMap ↔ IsLocalization S R' := by
+  convert isLocalizedModule_iff_isLocalization (S := S) (A := R) (Aₛ := R')
+  exact (Submonoid.map_id S).symm
+
+instance {A} [CommRing A] [Algebra R A] [IsLocalization S A] :
+    IsLocalizedModule S (Algebra.linearMap R A) :=
+  (isLocalizedModule_iff_isLocalization' S _).mpr inferInstance
+
+end IsLocalizedModule

Mathlib/Algebra/Module/Submodule/Localization.lean → Mathlib/Algebra/Module/LocalizedModule/Submodule.lean

@@ -3,7 +3,7 @@ Copyright (c) 2024 Andrew Yang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
-import Mathlib.Algebra.Module.LocalizedModule
+import Mathlib.Algebra.Module.LocalizedModule.Basic
 import Mathlib.LinearAlgebra.Quotient.Basic
 import Mathlib.RingTheory.Localization.Module