feat(ring_theory/localization): generalize lemmas from comm_ring to…

… `comm_semiring` (#13994)

This PR does not add new stuffs, but removes several subtractions from the proofs.

src/ring_theory/localization/at_prime.lean

@@ -28,8 +28,8 @@ See `src/ring_theory/localization/basic.lean` for a design overview.
 localization, ring localization, commutative ring localization, characteristic predicate,
 commutative ring, field of fractions
 -/
-variables {R : Type*} [comm_ring R] (M : submonoid R) (S : Type*) [comm_ring S]
-variables [algebra R S] {P : Type*} [comm_ring P]
+variables {R : Type*} [comm_semiring R] (M : submonoid R) (S : Type*) [comm_semiring S]
+variables [algebra R S] {P : Type*} [comm_semiring P]
 
 section at_prime
 
@@ -58,37 +58,41 @@ protected abbreviation localization.at_prime := localization I.prime_compl
 
 namespace is_localization
 
+lemma at_prime.nontrivial [is_localization.at_prime S I] : nontrivial S :=
+nontrivial_of_ne (0 : S) 1 $ λ hze,
+begin
+  rw [←(algebra_map R S).map_one, ←(algebra_map R S).map_zero] at hze,
+  obtain ⟨t, ht⟩ := (eq_iff_exists I.prime_compl S).1 hze,
+  have htz : (t : R) = 0, by simpa using ht.symm,
+  exact t.2 (htz.symm ▸ I.zero_mem : ↑t ∈ I)
+end
+
+local attribute [instance] at_prime.nontrivial
+
 theorem at_prime.local_ring [is_localization.at_prime S I] : local_ring S :=
-@local_ring.of_nonunits_add _ _ (nontrivial_of_ne (0 : S) 1
-  (λ hze, begin
-      rw [←(algebra_map R S).map_one, ←(algebra_map R S).map_zero] at hze,
-      obtain ⟨t, ht⟩ := (eq_iff_exists I.prime_compl S).1 hze,
-      exact ((show (t : R) ∉ I, from t.2) (have htz : (t : R) = 0, by simpa using ht.symm,
-        htz.symm ▸ I.zero_mem))
-    end))
-  (begin
-    intros x y hx hy hu,
-    cases is_unit_iff_exists_inv.1 hu with z hxyz,
-    have : ∀ {r : R} {s : I.prime_compl}, mk' S r s ∈ nonunits S → r ∈ I, from
-      λ (r : R) (s : I.prime_compl), not_imp_comm.1
-        (λ nr, is_unit_iff_exists_inv.2 ⟨mk' S ↑s (⟨r, nr⟩ : I.prime_compl),
-          mk'_mul_mk'_eq_one' _ _ nr⟩),
-    rcases mk'_surjective I.prime_compl x with ⟨rx, sx, hrx⟩,
-    rcases mk'_surjective I.prime_compl y with ⟨ry, sy, hry⟩,
-    rcases mk'_surjective I.prime_compl z with ⟨rz, sz, hrz⟩,
-    rw [←hrx, ←hry, ←hrz, ←mk'_add, ←mk'_mul,
-        ←mk'_self S I.prime_compl.one_mem] at hxyz,
-    rw ←hrx at hx, rw ←hry at hy,
-    obtain ⟨t, ht⟩ := is_localization.eq.1 hxyz,
-    simp only [mul_one, one_mul, submonoid.coe_mul, subtype.coe_mk] at ht,
-    rw [←sub_eq_zero, ←sub_mul] at ht,
-    have hr := (hp.mem_or_mem_of_mul_eq_zero ht).resolve_right t.2,
-    rw sub_eq_add_neg at hr,
-    have := I.neg_mem_iff.1 ((ideal.add_mem_iff_right _ _).1 hr),
-    { exact not_or (mt hp.mem_or_mem (not_or sx.2 sy.2)) sz.2 (hp.mem_or_mem this)},
-    { exact I.mul_mem_right _ (I.add_mem (I.mul_mem_right _ (this hx))
-                                         (I.mul_mem_right _ (this hy)))}
-  end)
+local_ring.of_nonunits_add
+begin
+  intros x y hx hy hu,
+  cases is_unit_iff_exists_inv.1 hu with z hxyz,
+  have : ∀ {r : R} {s : I.prime_compl}, mk' S r s ∈ nonunits S → r ∈ I, from
+    λ (r : R) (s : I.prime_compl), not_imp_comm.1
+      (λ nr, is_unit_iff_exists_inv.2 ⟨mk' S ↑s (⟨r, nr⟩ : I.prime_compl),
+        mk'_mul_mk'_eq_one' _ _ nr⟩),
+  rcases mk'_surjective I.prime_compl x with ⟨rx, sx, hrx⟩,
+  rcases mk'_surjective I.prime_compl y with ⟨ry, sy, hry⟩,
+  rcases mk'_surjective I.prime_compl z with ⟨rz, sz, hrz⟩,
+  rw [←hrx, ←hry, ←hrz, ←mk'_add, ←mk'_mul,
+      ←mk'_self S I.prime_compl.one_mem] at hxyz,
+  rw ←hrx at hx, rw ←hry at hy,
+  obtain ⟨t, ht⟩ := is_localization.eq.1 hxyz,
+  simp only [mul_one, one_mul, submonoid.coe_mul, subtype.coe_mk] at ht,
+  suffices : ↑sx * ↑sy * ↑sz * ↑t ∈ I, from
+    not_or (mt hp.mem_or_mem $ not_or sx.2 sy.2) sz.2
+      (hp.mem_or_mem $ (hp.mem_or_mem this).resolve_right t.2),
+  rw [←ht, mul_assoc],
+  exact I.mul_mem_right _ (I.add_mem (I.mul_mem_right _ $ this hx)
+                                     (I.mul_mem_right _ $ this hy))
+end
 
 end is_localization
 
@@ -130,7 +134,7 @@ lemma is_unit_to_map_iff (x : R) :
 lemma to_map_mem_maximal_iff (x : R) (h : _root_.local_ring S := local_ring S I) :
   algebra_map R S x ∈ local_ring.maximal_ideal S ↔ x ∈ I :=
 not_iff_not.mp $ by
-simpa only [@local_ring.mem_maximal_ideal S, mem_nonunits_iff, not_not]
+simpa only [local_ring.mem_maximal_ideal, mem_nonunits_iff, not_not]
   using is_unit_to_map_iff S I x
 
 lemma is_unit_mk'_iff (x : R) (y : I.prime_compl) :
@@ -141,7 +145,7 @@ lemma is_unit_mk'_iff (x : R) (y : I.prime_compl) :
 lemma mk'_mem_maximal_iff (x : R) (y : I.prime_compl) (h : _root_.local_ring S := local_ring S I) :
   mk' S x y ∈ local_ring.maximal_ideal S ↔ x ∈ I :=
 not_iff_not.mp $ by
-simpa only [@local_ring.mem_maximal_ideal S, mem_nonunits_iff, not_not]
+simpa only [local_ring.mem_maximal_ideal, mem_nonunits_iff, not_not]
   using is_unit_mk'_iff S I x y
 
 end at_prime
@@ -227,7 +231,7 @@ map_unique _ _ hj
   local_ring_hom I I (ring_hom.id R) (ideal.comap_id I).symm = ring_hom.id _ :=
 local_ring_hom_unique _ _ _ _ (λ x, rfl)
 
-@[simp] lemma local_ring_hom_comp {S : Type*} [comm_ring S]
+@[simp] lemma local_ring_hom_comp {S : Type*} [comm_semiring S]
   (J : ideal S) [hJ : J.is_prime] (K : ideal P) [hK : K.is_prime]
   (f : R →+* S) (hIJ : I = J.comap f) (g : S →+* P) (hJK : J = K.comap g) :
   local_ring_hom I K (g.comp f) (by rw [hIJ, hJK, ideal.comap_comap f g]) =

src/ring_theory/localization/away.lean

@@ -21,8 +21,8 @@ See `src/ring_theory/localization/basic.lean` for a design overview.
 localization, ring localization, commutative ring localization, characteristic predicate,
 commutative ring, field of fractions
 -/
-variables {R : Type*} [comm_ring R] (M : submonoid R) {S : Type*} [comm_ring S]
-variables [algebra R S] {P : Type*} [comm_ring P]
+variables {R : Type*} [comm_semiring R] (M : submonoid R) {S : Type*} [comm_semiring S]
+variables [algebra R S] {P : Type*} [comm_semiring P]
 
 
 namespace is_localization
@@ -33,7 +33,7 @@ variables (x : R)
 
 /-- Given `x : R`, the typeclass `is_localization.away x S` states that `S` is
 isomorphic to the localization of `R` at the submonoid generated by `x`. -/
-abbreviation away (S : Type*) [comm_ring S] [algebra R S] :=
+abbreviation away (S : Type*) [comm_semiring S] [algebra R S] :=
 is_localization (submonoid.powers x) S
 
 namespace away
@@ -46,7 +46,7 @@ mk' S (1 : R) ⟨x, submonoid.mem_powers _⟩
 
 variables {g : R →+* P}
 
-/-- Given `x : R`, a localization map `F : R →+* S` away from `x`, and a map of `comm_ring`s
+/-- Given `x : R`, a localization map `F : R →+* S` away from `x`, and a map of `comm_semiring`s
 `g : R →+* P` such that `g x` is invertible, the homomorphism induced from `S` to `P` sending
 `z : S` to `g y * (g x)⁻ⁿ`, where `y : R, n : ℕ` are such that `z = F y * (F x)⁻ⁿ`. -/
 noncomputable def lift (hg : is_unit (g x)) : S →+* P :=
@@ -71,7 +71,7 @@ lift x $ show is_unit ((algebra_map R P) x), from
 is_unit_of_mul_eq_one ((algebra_map R P) x) (mk' P y ⟨x * y, submonoid.mem_powers _⟩) $
 by rw [mul_mk'_eq_mk'_of_mul, mk'_self]
 
-variables (S) (Q : Type*) [comm_ring Q] [algebra P Q]
+variables (S) (Q : Type*) [comm_semiring Q] [algebra P Q]
 
 /-- Given a map `f : R →+* S` and an element `r : R`, we may construct a map `Rᵣ →+* Sᵣ`. -/
 noncomputable

src/ring_theory/localization/ideal.lean

@@ -17,14 +17,13 @@ See `src/ring_theory/localization/basic.lean` for a design overview.
 localization, ring localization, commutative ring localization, characteristic predicate,
 commutative ring, field of fractions
 -/
-variables {R : Type*} [comm_ring R] (M : submonoid R) (S : Type*) [comm_ring S]
-variables [algebra R S] {P : Type*} [comm_ring P]
+
 namespace is_localization
-variables [is_localization M S]
 
-section ideals
+section comm_semiring
+variables {R : Type*} [comm_semiring R] (M : submonoid R) (S : Type*) [comm_semiring S]
+variables [algebra R S] [is_localization M S]
 
-variables (M) (S)
 include M
 
 /-- Explicit characterization of the ideal given by `ideal.map (algebra_map R S) I`.
@@ -80,22 +79,11 @@ theorem comap_map_of_is_prime_disjoint (I : ideal R) (hI : I.is_prime)
   ideal.comap (algebra_map R S) (ideal.map (algebra_map R S) I) = I :=
 begin
   refine le_antisymm (λ a ha, _) ideal.le_comap_map,
-  rw [ideal.mem_comap, mem_map_algebra_map_iff M S] at ha,
-  obtain ⟨⟨b, s⟩, h⟩ := ha,
-  have : (algebra_map R S) (a * ↑s - b) = 0 := by simpa [sub_eq_zero] using h,
-  rw [← (algebra_map R S).map_zero, eq_iff_exists M S] at this,
-  obtain ⟨c, hc⟩ := this,
-  have : a * s ∈ I,
-  { rw zero_mul at hc,
-    let this : (a * ↑s - ↑b) * ↑c ∈ I := hc.symm ▸ I.zero_mem,
-    cases hI.mem_or_mem this with h1 h2,
-    { simpa using I.add_mem h1 b.2 },
-    { exfalso,
-      refine hM ⟨c.2, h2⟩ } },
-  cases hI.mem_or_mem this with h1 h2,
-  { exact h1 },
-  { exfalso,
-    refine hM ⟨s.2, h2⟩ }
+  obtain ⟨⟨b, s⟩, h⟩ := (mem_map_algebra_map_iff M S).1 (ideal.mem_comap.1 ha),
+  replace h : algebra_map R S (a * s) = algebra_map R S b := by simpa only [←map_mul] using h,
+  obtain ⟨c, hc⟩ := (eq_iff_exists M S).1 h,
+  have : a * (s * c) ∈ I := by { rw [←mul_assoc, hc], exact I.mul_mem_right c b.2 },
+  exact (hI.mem_or_mem this).resolve_right (λ hsc, hM ⟨(s * c).2, hsc⟩)
 end
 
 /-- If `S` is the localization of `R` at a submonoid, the ordering of ideals of `S` is
@@ -159,6 +147,14 @@ def order_iso_of_prime :
   map_rel_iff' := λ I I', ⟨λ h, (show I.val ≤ I'.val,
     from (map_comap M S I.val) ▸ (map_comap M S I'.val) ▸ (ideal.map_mono h)), λ h x hx, h hx⟩ }
 
+end comm_semiring
+
+section comm_ring
+variables {R : Type*} [comm_ring R] (M : submonoid R) (S : Type*) [comm_ring S]
+variables [algebra R S] [is_localization M S]
+
+include M
+
 /-- `quotient_map` applied to maximal ideals of a localization is `surjective`.
   The quotient by a maximal ideal is a field, so inverses to elements already exist,
   and the localization necessarily maps the equivalence class of the inverse in the localization -/
@@ -193,6 +189,6 @@ begin
       (by rw [← ring_hom.map_mul, ← mk'_eq_mul_mk'_one, mk'_self, ring_hom.map_one]))) }
 end
 
-end ideals
+end comm_ring
 
 end is_localization