[Merged by Bors] - chore(ring_theory/ideal/local_ring): generalize to semirings

src/ring_theory/graded_algebra/homogeneous_localization.lean

@@ -470,28 +470,30 @@ end, λ ⟨⟨_, b, eq1, eq2⟩, rfl⟩, begin
   exact ⟨⟨f.val, b.val, eq1, eq2⟩, rfl⟩
 end⟩
 
+instance : nontrivial (homogeneous_localization 𝒜 x) :=
+⟨⟨0, 1, λ r, by simpa [ext_iff_val, zero_val, one_val, zero_ne_one] using r⟩⟩
+
 instance : local_ring (homogeneous_localization 𝒜 x) :=
-{ exists_pair_ne := ⟨0, 1, λ r, by simpa [ext_iff_val, zero_val, one_val, zero_ne_one] using r⟩,
-  is_local := λ a, begin
-    simp only [← is_unit_iff_is_unit_val, sub_val, one_val],
-    induction a using quotient.induction_on',
-    simp only [homogeneous_localization.val_mk', ← subtype.val_eq_coe],
-    by_cases mem1 : a.num.1 ∈ x,
-    { right,
-      have : a.denom.1 - a.num.1 ∈ x.prime_compl := λ h, a.denom_not_mem
-        ((sub_add_cancel a.denom.val a.num.val) ▸ ideal.add_mem _ h mem1 : a.denom.1 ∈ x),
-      apply is_unit_of_mul_eq_one _ (localization.mk a.denom.1 ⟨a.denom.1 - a.num.1, this⟩),
-      simp only [sub_mul, localization.mk_mul, one_mul, localization.sub_mk, ← subtype.val_eq_coe,
-        submonoid.coe_mul],
-      convert localization.mk_self _,
-      simp only [← subtype.val_eq_coe, submonoid.coe_mul],
-      ring, },
-    { left,
-      change _ ∈ x.prime_compl at mem1,
-      apply is_unit_of_mul_eq_one _ (localization.mk a.denom.1 ⟨a.num.1, mem1⟩),
-      rw [localization.mk_mul],
-      convert localization.mk_self _,
-      simpa only [mul_comm], },
-end }
+local_of_is_unit_or_is_unit_one_sub_self $ λ a, begin
+  simp only [← is_unit_iff_is_unit_val, sub_val, one_val],
+  induction a using quotient.induction_on',
+  simp only [homogeneous_localization.val_mk', ← subtype.val_eq_coe],
+  by_cases mem1 : a.num.1 ∈ x,
+  { right,
+    have : a.denom.1 - a.num.1 ∈ x.prime_compl := λ h, a.denom_not_mem
+      ((sub_add_cancel a.denom.val a.num.val) ▸ ideal.add_mem _ h mem1 : a.denom.1 ∈ x),
+    apply is_unit_of_mul_eq_one _ (localization.mk a.denom.1 ⟨a.denom.1 - a.num.1, this⟩),
+    simp only [sub_mul, localization.mk_mul, one_mul, localization.sub_mk, ← subtype.val_eq_coe,
+      submonoid.coe_mul],
+    convert localization.mk_self _,
+    simp only [← subtype.val_eq_coe, submonoid.coe_mul],
+    ring, },
+  { left,
+    change _ ∈ x.prime_compl at mem1,
+    apply is_unit_of_mul_eq_one _ (localization.mk a.denom.1 ⟨a.num.1, mem1⟩),
+    rw [localization.mk_mul],
+    convert localization.mk_self _,
+    simpa only [mul_comm], },
+end
 
 end homogeneous_localization

src/ring_theory/ideal/local_ring.lean

@@ -16,11 +16,11 @@ Define local rings as commutative rings having a unique maximal ideal.
 
 ## Main definitions
 
-* `local_ring`: A predicate on commutative rings, stating that every element `a` is either a unit
-  or `1 - a` is a unit. This is shown to be equivalent to the condition that there exists a unique
+* `local_ring`: A predicate on commutative semirings, stating that the set of nonunits is closed
+  under the addition. This is shown to be equivalent to the condition that there exists a unique
   maximal ideal.
-* `local_ring.maximal_ideal`: The unique maximal ideal for a local rings. Its carrier set is the set
-  of non units.
+* `local_ring.maximal_ideal`: The unique maximal ideal for a local rings. Its carrier set is the
+  set of non units.
 * `is_local_ring_hom`: A predicate on semiring homomorphisms, requiring that it maps nonunits
   to nonunits. For local rings, this means that the image of the unique maximal ideal is again
   contained in the unique maximal ideal.
@@ -32,53 +32,43 @@ universes u v w
 
 /-- A commutative ring is local if it has a unique maximal ideal. Note that
   `local_ring` is a predicate. -/
-class local_ring (R : Type u) [comm_ring R] extends nontrivial R : Prop :=
-(is_local : ∀ (a : R), (is_unit a) ∨ (is_unit (1 - a)))
+class local_ring (R : Type u) [comm_semiring R] extends nontrivial R : Prop :=
+(nonunits_add : ∀ {a b : R}, a ∈ nonunits R → b ∈ nonunits R → a + b ∈ nonunits R)
 
 namespace local_ring
 
-variables {R : Type u} [comm_ring R] [local_ring R]
+variables {R : Type u}
 
-lemma is_unit_or_is_unit_one_sub_self (a : R) :
+lemma is_unit_or_is_unit_one_sub_self [comm_ring R] [local_ring R] (a : R) :
   (is_unit a) ∨ (is_unit (1 - a)) :=
-is_local a
+or_iff_not_imp_left.mpr $ λ ha,
+begin
+  by_contra ha',
+  apply nonunits_add ha ha',
+  simp [-sub_eq_add_neg, add_sub_cancel'_right]
+end
 
-lemma is_unit_of_mem_nonunits_one_sub_self (a : R) (h : (1 - a) ∈ nonunits R) :
+lemma is_unit_of_mem_nonunits_one_sub_self [comm_ring R] [local_ring R]
+  (a : R) (h : (1 - a) ∈ nonunits R) :
   is_unit a :=
-or_iff_not_imp_right.1 (is_local a) h
+or_iff_not_imp_right.1 (is_unit_or_is_unit_one_sub_self a) h
 
-lemma is_unit_one_sub_self_of_mem_nonunits (a : R) (h : a ∈ nonunits R) :
+lemma is_unit_one_sub_self_of_mem_nonunits [comm_ring R] [local_ring R]
+  (a : R) (h : a ∈ nonunits R) :
   is_unit (1 - a) :=
-or_iff_not_imp_left.1 (is_local a) h
-
-lemma nonunits_add {x y} (hx : x ∈ nonunits R) (hy : y ∈ nonunits R) :
-  x + y ∈ nonunits R :=
-begin
-  rintros ⟨u, hu⟩,
-  apply hy,
-  suffices : is_unit ((↑u⁻¹ : R) * y),
-  { rcases this with ⟨s, hs⟩,
-    use u * s,
-    convert congr_arg (λ z, (u : R) * z) hs,
-    rw ← mul_assoc, simp },
-  rw show (↑u⁻¹ * y) = (1 - ↑u⁻¹ * x),
-  { rw eq_sub_iff_add_eq,
-    replace hu := congr_arg (λ z, (↑u⁻¹ : R) * z) hu.symm,
-    simpa [mul_add, add_comm] using hu },
-  apply is_unit_one_sub_self_of_mem_nonunits,
-  exact mul_mem_nonunits_right hx
-end
+or_iff_not_imp_left.1 (is_unit_or_is_unit_one_sub_self a) h
 
 variable (R)
 
 /-- The ideal of elements that are not units. -/
-def maximal_ideal : ideal R :=
+def maximal_ideal [comm_semiring R] [local_ring R] : ideal R :=
 { carrier := nonunits R,
   zero_mem' := zero_mem_nonunits.2 $ zero_ne_one,
   add_mem' := λ x y hx hy, nonunits_add hx hy,
   smul_mem' := λ a x, mul_mem_nonunits_right }
 
-instance maximal_ideal.is_maximal : (maximal_ideal R).is_maximal :=
+instance maximal_ideal.is_maximal [comm_semiring R] [local_ring R] :
+  (maximal_ideal R).is_maximal :=
 begin
   rw ideal.is_maximal_iff,
   split,
@@ -89,41 +79,58 @@ begin
     simpa using I.mul_mem_left ↑u⁻¹ H }
 end
 
-lemma maximal_ideal_unique :
+lemma maximal_ideal_unique [comm_semiring R] [local_ring R] :
   ∃! I : ideal R, I.is_maximal :=
 ⟨maximal_ideal R, maximal_ideal.is_maximal R,
   λ I hI, hI.eq_of_le (maximal_ideal.is_maximal R).1.1 $
   λ x hx, hI.1.1 ∘ I.eq_top_of_is_unit_mem hx⟩
 
 variable {R}
 
-lemma eq_maximal_ideal {I : ideal R} (hI : I.is_maximal) : I = maximal_ideal R :=
+lemma eq_maximal_ideal [comm_semiring R] [local_ring R] {I : ideal R} (hI : I.is_maximal) :
+  I = maximal_ideal R :=
 unique_of_exists_unique (maximal_ideal_unique R) hI $ maximal_ideal.is_maximal R
 
-lemma le_maximal_ideal {J : ideal R} (hJ : J ≠ ⊤) : J ≤ maximal_ideal R :=
+lemma le_maximal_ideal [comm_semiring R] [local_ring R] {J : ideal R} (hJ : J ≠ ⊤) :
+  J ≤ maximal_ideal R :=
 begin
   rcases ideal.exists_le_maximal J hJ with ⟨M, hM1, hM2⟩,
   rwa ←eq_maximal_ideal hM1
 end
 
-@[simp] lemma mem_maximal_ideal (x) :
+@[simp] lemma mem_maximal_ideal [comm_semiring R] [local_ring R] (x) :
   x ∈ maximal_ideal R ↔ x ∈ nonunits R := iff.rfl
 
 end local_ring
 
 variables {R : Type u} {S : Type v} {T : Type w}
 
-lemma local_of_nonunits_ideal [comm_ring R] (hnze : (0:R) ≠ 1)
+lemma local_of_nonunits_ideal [comm_semiring R] (hnze : (0:R) ≠ 1)
   (h : ∀ x y ∈ nonunits R, x + y ∈ nonunits R) : local_ring R :=
 { exists_pair_ne := ⟨0, 1, hnze⟩,
-  is_local := λ x, or_iff_not_imp_left.mpr $ λ hx,
-  begin
-    by_contra H,
-    apply h _ hx _ H,
-    simp [-sub_eq_add_neg, add_sub_cancel'_right]
-  end }
+  nonunits_add := λ x y hx hy, h x hx y hy }
+
+lemma local_of_is_unit_or_is_unit_one_sub_self [comm_ring R] [nontrivial R]
+  (h : ∀ a : R, is_unit a ∨ is_unit (1 - a)) : local_ring R :=
+local_ring.mk
+begin
+  intros x y hx hy,
+  rintros ⟨u, hu⟩,
+  apply hy,
+  suffices : is_unit ((↑u⁻¹ : R) * y),
+  { rcases this with ⟨s, hs⟩,
+    use u * s,
+    convert congr_arg (λ z, (u : R) * z) hs,
+    rw ← mul_assoc, simp },
+  rw show (↑u⁻¹ * y) = (1 - ↑u⁻¹ * x),
+  { rw eq_sub_iff_add_eq,
+    replace hu := congr_arg (λ z, (↑u⁻¹ : R) * z) hu.symm,
+    simpa [mul_add, add_comm] using hu },
+  apply or_iff_not_imp_left.1 (h _),
+  exact mul_mem_nonunits_right hx
+end
 
-lemma local_of_unique_max_ideal [comm_ring R] (h : ∃! I : ideal R, I.is_maximal) :
+lemma local_of_unique_max_ideal [comm_semiring R] (h : ∃! I : ideal R, I.is_maximal) :
   local_ring R :=
 local_of_nonunits_ideal
 (let ⟨I, Imax, _⟩ := h in (λ (H : 0 = 1), Imax.1.1 $ I.eq_top_iff_one.2 $ H ▸ I.zero_mem))
@@ -135,7 +142,7 @@ have xmemI : x ∈ I, from ((Iuniq Ix Ixmax) ▸ Hx),
 have ymemI : y ∈ I, from ((Iuniq Iy Iymax) ▸ Hy),
 Imax.1.1 $ I.eq_top_of_is_unit_mem (I.add_mem xmemI ymemI) H
 
-lemma local_of_unique_nonzero_prime (R : Type u) [comm_ring R]
+lemma local_of_unique_nonzero_prime (R : Type u) [comm_semiring R]
   (h : ∃! P : ideal R, P ≠ ⊥ ∧ ideal.is_prime P) : local_ring R :=
 local_of_unique_max_ideal begin
   rcases h with ⟨P, ⟨hPnonzero, hPnot_top, _⟩, hPunique⟩,
@@ -149,15 +156,14 @@ end
 lemma local_of_surjective [comm_ring R] [local_ring R] [comm_ring S] [nontrivial S]
   (f : R →+* S) (hf : function.surjective f) :
   local_ring S :=
-{ is_local :=
-  begin
-    intros b,
-    obtain ⟨a, rfl⟩ := hf b,
-    apply (local_ring.is_unit_or_is_unit_one_sub_self a).imp f.is_unit_map _,
-    rw [← f.map_one, ← f.map_sub],
-    apply f.is_unit_map,
-  end,
-  .. ‹nontrivial S› }
+local_of_is_unit_or_is_unit_one_sub_self
+begin
+  intros b,
+  obtain ⟨a, rfl⟩ := hf b,
+  apply (local_ring.is_unit_or_is_unit_one_sub_self a).imp f.is_unit_map _,
+  rw [← f.map_one, ← f.map_sub],
+  apply f.is_unit_map,
+end
 
 /-- A local ring homomorphism is a homomorphism between local rings
   such that the image of the maximal ideal of the source is contained within
@@ -173,6 +179,11 @@ instance is_local_ring_hom_id (R : Type*) [semiring R] : is_local_ring_hom (ring
   is_unit (f a) ↔ is_unit a :=
 ⟨is_local_ring_hom.map_nonunit a, f.is_unit_map⟩
 
+@[simp] lemma mem_nonunits_map_iff [semiring R] [semiring S] (f : R →+* S)
+  [is_local_ring_hom f] (a) :
+  f a ∈ nonunits S ↔ a ∈ nonunits R :=
+⟨λ h ha, h $ (is_unit_map_iff f a).mpr ha, λ h ha, h $ (is_unit_map_iff f a).mp ha⟩
+
 instance is_local_ring_hom_comp [semiring R] [semiring S] [semiring T]
   (g : S →+* T) (f : R →+* S) [is_local_ring_hom g] [is_local_ring_hom f] :
   is_local_ring_hom (g.comp f) :=
@@ -189,9 +200,9 @@ lemma _root_.ring_hom.domain_local_ring {R S : Type*} [comm_ring R] [comm_ring S
 begin
   haveI : nontrivial R := pullback_nonzero f f.map_zero f.map_one,
   constructor,
-  intro x,
-  rw [← is_unit_map_iff f, ← is_unit_map_iff f, f.map_sub, f.map_one],
-  exact _root_.local_ring.is_local (f x)
+  intros a b,
+  simp_rw [←mem_nonunits_map_iff f, f.map_add],
+  exact local_ring.nonunits_add
 end
 
 lemma is_local_ring_hom_of_comp {R S T: Type*} [comm_ring R] [comm_ring S] [comm_ring T]
@@ -210,7 +221,7 @@ instance is_local_ring_hom_equiv [semiring R] [semiring S] (f : R ≃+* S) :
   (a) (h : is_unit (f a)) : is_unit a :=
 is_local_ring_hom.map_nonunit a h
 
-theorem of_irreducible_map [semiring R] [semiring S] (f : R →+* S) [h : is_local_ring_hom f] {x : R}
+theorem of_irreducible_map [semiring R] [semiring S] (f : R →+* S) [h : is_local_ring_hom f] {x}
   (hfx : irreducible (f x)) : irreducible x :=
 ⟨λ h, hfx.not_unit $ is_unit.map f h, λ p q hx, let ⟨H⟩ := h in
 or.imp (H p) (H q) $ hfx.is_unit_or_is_unit $ f.map_mul p q ▸ congr_arg f hx⟩
@@ -234,7 +245,7 @@ end
 
 section
 open local_ring
-variables [comm_ring R] [local_ring R] [comm_ring S] [local_ring S]
+variables [comm_semiring R] [local_ring R] [comm_semiring S] [local_ring S]
 variables (f : R →+* S) [is_local_ring_hom f]
 
 lemma map_nonunit (a : R) (h : a ∈ maximal_ideal R) : f a ∈ maximal_ideal S :=
@@ -243,7 +254,8 @@ lemma map_nonunit (a : R) (h : a ∈ maximal_ideal R) : f a ∈ maximal_ideal S
 end
 
 namespace local_ring
-variables [comm_ring R] [local_ring R] [comm_ring S] [local_ring S]
+section
+variables [comm_semiring R] [local_ring R] [comm_semiring S] [local_ring S]
 
 /--
 A ring homomorphism between local rings is a local ring hom iff it reflects units,
@@ -267,7 +279,10 @@ begin
   tfae_finish,
 end
 
-variable (R)
+end
+
+section
+variables (R) [comm_ring R] [local_ring R]
 /-- The residue field of a local ring is the quotient of the ring by its maximal ideal. -/
 def residue_field := R ⧸ maximal_ideal R
 
@@ -280,12 +295,15 @@ noncomputable instance : inhabited (residue_field R) := ⟨37⟩
 def residue : R →+* (residue_field R) :=
 ideal.quotient.mk _
 
-noncomputable instance residue_field.algebra : algebra R (residue_field R) := (residue R).to_algebra
+noncomputable
+instance residue_field.algebra : algebra R (residue_field R) := (residue R).to_algebra
+
+end
 
 namespace residue_field
 
 
-variables {R S}
+variables {R S} [comm_ring R] [local_ring R] [comm_ring S] [local_ring S]
 /-- The map on residue fields induced by a local homomorphism between local rings -/
 noncomputable def map (f : R →+* S) [is_local_ring_hom f] :
   residue_field R →+* residue_field S :=
@@ -298,7 +316,7 @@ end
 
 end residue_field
 
-variables {R}
+variables {R} [comm_ring R] [local_ring R]
 
 lemma ker_eq_maximal_ideal {K : Type*} [field K]
   (φ : R →+* K) (hφ : function.surjective φ) : φ.ker = maximal_ideal R :=
@@ -313,9 +331,9 @@ open_locale classical
 
 @[priority 100] -- see Note [lower instance priority]
 instance : local_ring R :=
-{ is_local := λ a,
+local_of_is_unit_or_is_unit_one_sub_self $ λ a,
   if h : a = 0
   then or.inr (by rw [h, sub_zero]; exact is_unit_one)
-  else or.inl $ is_unit.mk0 a h }
+  else or.inl $ is_unit.mk0 a h
 
 end field

src/ring_theory/power_series/basic.lean

@@ -649,10 +649,12 @@ variable [comm_ring R]
 
 /-- Multivariate formal power series over a local ring form a local ring. -/
 instance [local_ring R] : local_ring (mv_power_series σ R) :=
-{ is_local := by { intro φ, rcases local_ring.is_local (constant_coeff σ R φ) with ⟨u,h⟩|⟨u,h⟩;
+local_of_is_unit_or_is_unit_one_sub_self $ by
+{ intro φ,
+  rcases local_ring.is_unit_or_is_unit_one_sub_self (constant_coeff σ R φ) with ⟨u,h⟩|⟨u,h⟩;
     [left, right];
     { refine is_unit_of_mul_eq_one _ _ (mul_inv_of_unit _ u _),
-      simpa using h.symm } } }
+      simpa using h.symm } }
 
 -- TODO(jmc): once adic topology lands, show that this is complete