feat: Generalize results on Tensor Product and Localization from Ring…

…s to Semirings
leanprover-community · Jan 7, 2024 · f9a53a5 · f9a53a5
1 parent ca6881d
commit f9a53a5
Show file tree

Hide file tree

Showing 4 changed files with 22 additions and 18 deletions.
diff --git a/Mathlib/Algebra/Module/LocalizedModule.lean b/Mathlib/Algebra/Module/LocalizedModule.lean
@@ -540,7 +540,7 @@ section IsLocalizedModule
 
 universe u v
 
-variable {R : Type*} [CommRing R] (S : Submonoid R)
+variable {R : Type*} [CommSemiring R] (S : Submonoid R)
 
 variable {M M' M'' : Type*} [AddCommMonoid M] [AddCommMonoid M'] [AddCommMonoid M'']
 
@@ -1083,7 +1083,7 @@ theorem mkOfAlgebra {R S S' : Type*} [CommRing R] [CommRing S] [CommRing S'] [Al
 end Algebra
 
 variable {A : Type*}
-  [CommRing A] [Algebra R A] [Module A M'] [IsScalarTower R A M'] [IsLocalization S A]
+  [CommSemiring A] [Algebra R A] [Module A M'] [IsScalarTower R A M'] [IsLocalization S A]
 
 
 /-- If `(f : M →ₗ[R] M')` is a localization of modules, then the map

diff --git a/Mathlib/RingTheory/IsTensorProduct.lean b/Mathlib/RingTheory/IsTensorProduct.lean
@@ -38,7 +38,7 @@ open TensorProduct
 
 section IsTensorProduct
 
-variable {R : Type*} [CommRing R]
+variable {R : Type*} [CommSemiring R]
 
 variable {M₁ M₂ M M' : Type*}
 
@@ -140,9 +140,9 @@ section IsBaseChange
 
 variable {R : Type*} {M : Type v₁} {N : Type v₂} (S : Type v₃)
 
-variable [AddCommMonoid M] [AddCommMonoid N] [CommRing R]
+variable [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R]
 
-variable [CommRing S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N]
+variable [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N]
 
 variable (f : M →ₗ[R] N)
 
@@ -325,7 +325,7 @@ theorem IsBaseChange.ofEquiv (e : M ≃ₗ[R] N) : IsBaseChange R e.toLinearMap
   simp
 #align is_base_change.of_equiv IsBaseChange.ofEquiv
 
-variable {T O : Type*} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T]
+variable {T O : Type*} [CommSemiring T] [Algebra R T] [Algebra S T] [IsScalarTower R S T]
 
 variable [AddCommMonoid O] [Module R O] [Module S O] [Module T O] [IsScalarTower S T O]
 
@@ -356,7 +356,7 @@ theorem IsBaseChange.comp {f : M →ₗ[R] N} (hf : IsBaseChange S f) {g : N →
   rfl
 #align is_base_change.comp IsBaseChange.comp
 
-variable {R' S' : Type*} [CommRing R'] [CommRing S']
+variable {R' S' : Type*} [CommSemiring R'] [CommSemiring S']
 
 variable [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S']
 

diff --git a/Mathlib/RingTheory/Localization/Integer.lean b/Mathlib/RingTheory/Localization/Integer.lean
@@ -24,9 +24,9 @@ commutative ring, field of fractions
 -/
 
 
-variable {R : Type*} [CommRing R] {M : Submonoid R} {S : Type*} [CommRing S]
+variable {R : Type*} [CommSemiring R] {M : Submonoid R} {S : Type*} [CommSemiring S]
 
-variable [Algebra R S] {P : Type*} [CommRing P]
+variable [Algebra R S] {P : Type*} [CommSemiring P]
 
 open Function
 
@@ -42,25 +42,25 @@ variable (R)
 /-- Given `a : S`, `S` a localization of `R`, `IsInteger R a` iff `a` is in the image of
 the localization map from `R` to `S`. -/
 def IsInteger (a : S) : Prop :=
-  a ∈ (algebraMap R S).range
+  a ∈ (algebraMap R S).rangeS
 #align is_localization.is_integer IsLocalization.IsInteger
 
 end
 
 theorem isInteger_zero : IsInteger R (0 : S) :=
-  Subring.zero_mem _
+  Subsemiring.zero_mem _
 #align is_localization.is_integer_zero IsLocalization.isInteger_zero
 
 theorem isInteger_one : IsInteger R (1 : S) :=
-  Subring.one_mem _
+  Subsemiring.one_mem _
 #align is_localization.is_integer_one IsLocalization.isInteger_one
 
 theorem isInteger_add {a b : S} (ha : IsInteger R a) (hb : IsInteger R b) : IsInteger R (a + b) :=
-  Subring.add_mem _ ha hb
+  Subsemiring.add_mem _ ha hb
 #align is_localization.is_integer_add IsLocalization.isInteger_add
 
 theorem isInteger_mul {a b : S} (ha : IsInteger R a) (hb : IsInteger R b) : IsInteger R (a * b) :=
-  Subring.mul_mem _ ha hb
+  Subsemiring.mul_mem _ ha hb
 #align is_localization.is_integer_mul IsLocalization.isInteger_mul
 
 theorem isInteger_smul {a : R} {b : S} (hb : IsInteger R b) : IsInteger R (a • b) := by

diff --git a/Mathlib/RingTheory/Localization/Module.lean b/Mathlib/RingTheory/Localization/Module.lean
@@ -31,7 +31,7 @@ open nonZeroDivisors
 
 section Localization
 
-variable {R : Type*} (Rₛ : Type*) [CommRing R] [CommRing Rₛ] [Algebra R Rₛ]
+variable {R : Type*} (Rₛ : Type*) [CommSemiring R] [CommSemiring Rₛ] [Algebra R Rₛ]
 
 variable (S : Submonoid R) [hT : IsLocalization S Rₛ]
 
@@ -55,9 +55,14 @@ theorem LinearIndependent.localization {ι : Type*} {b : ι → M} (hli : Linear
 #align linear_independent.localization LinearIndependent.localization
 
 end AddCommMonoid
+end Localization
 
 section LocalizationLocalization
 
+variable {R : Type*} (Rₛ : Type*) [CommRing R] [CommRing Rₛ] [Algebra R Rₛ]
+
+variable (S : Submonoid R) [hT : IsLocalization S Rₛ]
+
 variable {A : Type*} [CommRing A] [Algebra R A]
 
 variable (Aₛ : Type*) [CommRing Aₛ] [Algebra A Aₛ]
@@ -150,7 +155,6 @@ theorem Basis.localizationLocalization_span {ι : Type*} (b : Basis ι R A) :
 
 end LocalizationLocalization
 
-end Localization
 
 section FractionRing
 
@@ -168,8 +172,8 @@ end FractionRing
 
 section
 
-variable {R : Type*} [CommRing R] (S : Submonoid R)
-variable (A : Type*) [CommRing A] [Algebra R A] [IsLocalization S A]
+variable {R : Type*} [CommSemiring R] (S : Submonoid R)
+variable (A : Type*) [CommSemiring A] [Algebra R A] [IsLocalization S A]
 variable {M N : Type*}
   [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M]
   [AddCommMonoid N] [Module R N] [Module A N] [IsScalarTower R A N]