refactor(ring_theory/ideals): make local_ring a prop class (#3171)

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

Author: kbuzzard

src/ring_theory/ideals.lean

@@ -36,6 +36,7 @@ theorem eq_top_iff_one : I = ⊤ ↔ (1:α) ∈ I :=
 theorem ne_top_iff_one : I ≠ ⊤ ↔ (1:α) ∉ I :=
 not_congr I.eq_top_iff_one
 
+/-- The ideal generated by a subset of a ring -/
 def span (s : set α) : ideal α := submodule.span α s
 
 lemma subset_span {s : set α} : s ⊆ span s := submodule.subset_span
@@ -73,6 +74,7 @@ lemma span_singleton_eq_bot {x} : span ({x} : set α) = ⊥ ↔ x = 0 := submodu
 lemma span_singleton_eq_top {x} : span ({x} : set α) = ⊤ ↔ is_unit x :=
 by rw [is_unit_iff_dvd_one, ← span_singleton_le_span_singleton, span_singleton_one, eq_top_iff]
 
+/-- An ideal `P` of a ring `R` is prime if `P ≠ R` and `xy ∈ P → x ∈ P ∨ y ∈ P` -/
 @[class] def is_prime (I : ideal α) : Prop :=
 I ≠ ⊤ ∧ ∀ {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I
 
@@ -98,6 +100,7 @@ theorem span_singleton_prime {p : α} (hp : p ≠ 0) :
   is_prime (span ({p} : set α)) ↔ prime p :=
 by simp [is_prime, prime, span_singleton_eq_top, hp, mem_span_singleton]
 
+/-- An ideal is maximal if it is maximal in the collection of proper ideals. -/
 @[class] def is_maximal (I : ideal α) : Prop :=
 I ≠ ⊤ ∧ ∀ J, I < J → J = ⊤
 
@@ -165,12 +168,17 @@ lt_of_le_not_le (ideal.span_le.2 $ singleton_subset_iff.2 $
 h₂ $ is_unit_of_dvd_one _ $ (mul_dvd_mul_iff_left h₁).1 $
 by rwa [mul_one, ← ideal.span_singleton_le_span_singleton]
 
+/-- The quotient `R/I` of a ring `R` by an ideal `I`. -/
 def quotient (I : ideal α) := I.quotient
 
 namespace quotient
 variables {I} {x y : α}
+
+/-- The map from a ring `R` to a quotient ring `R/I`. -/
 def mk (I : ideal α) (a : α) : I.quotient := submodule.quotient.mk a
 
+instance : inhabited (quotient I) := ⟨mk I 37⟩
+
 protected theorem eq : mk I x = mk I y ↔ x - y ∈ I := submodule.quotient.eq I
 
 instance (I : ideal α) : has_one I.quotient := ⟨mk I 1⟩
@@ -209,6 +217,7 @@ def mk_hom (I : ideal α) : α →+* I.quotient := ⟨mk I, rfl, λ _ _, rfl, rf
 
 lemma mk_eq_mk_hom (I : ideal α) (x : α) : ideal.quotient.mk I x = ideal.quotient.mk_hom I x := rfl
 
+/-- The image of an ideal J under the quotient map `R → R/I`. -/
 def map_mk (I J : ideal α) : ideal I.quotient :=
 { carrier := mk I '' J,
   zero_mem' := ⟨0, J.zero_mem, rfl⟩,
@@ -353,12 +362,15 @@ end
 
 section prio
 set_option default_priority 100 -- see Note [default priority]
-class local_ring (α : Type u) extends comm_ring α, nonzero α :=
+/-- A commutative ring is local if it has a unique maximal ideal. Note that
+  `local_ring` is a predicate. -/
+class local_ring (α : Type u) [comm_ring α] extends nonzero α : Prop :=
 (is_local : ∀ (a : α), (is_unit a) ∨ (is_unit (1 - a)))
 end prio
 
 namespace local_ring
-variable [local_ring α]
+
+variables [comm_ring α] [local_ring α]
 
 lemma is_unit_or_is_unit_one_sub_self (a : α) :
   (is_unit a) ∨ (is_unit (1 - a)) :=
@@ -393,13 +405,13 @@ end
 variable (α)
 
 /-- The ideal of elements that are not units. -/
-def nonunits_ideal : ideal α :=
+def maximal_ideal : ideal α :=
 { carrier := nonunits α,
   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 nonunits_ideal.is_maximal : (nonunits_ideal α).is_maximal :=
+instance maximal_ideal.is_maximal : (maximal_ideal α).is_maximal :=
 begin
   rw ideal.is_maximal_iff,
   split,
@@ -412,40 +424,28 @@ end
 
 lemma max_ideal_unique :
   ∃! I : ideal α, I.is_maximal :=
-⟨nonunits_ideal α, nonunits_ideal.is_maximal α,
-  λ I hI, hI.eq_of_le (nonunits_ideal.is_maximal α).1 $
+⟨maximal_ideal α, maximal_ideal.is_maximal α,
+  λ I hI, hI.eq_of_le (maximal_ideal.is_maximal α).1 $
   λ x hx, hI.1 ∘ I.eq_top_of_is_unit_mem hx⟩
 
 variable {α}
 
-@[simp] lemma mem_nonunits_ideal (x) :
-  x ∈ nonunits_ideal α ↔ x ∈ nonunits α := iff.rfl
+@[simp] lemma mem_maximal_ideal (x) :
+  x ∈ maximal_ideal α ↔ x ∈ nonunits α := iff.rfl
 
 end local_ring
 
-def is_local_ring (α : Type u) [comm_ring α] : Prop :=
-((0:α) ≠ 1) ∧ ∀ (a : α), (is_unit a) ∨ (is_unit (1 - a))
-
-def local_of_is_local_ring [comm_ring α] (h : is_local_ring α) : local_ring α :=
-{ zero_ne_one := h.1,
-  is_local := h.2,
-  .. ‹comm_ring α› }
-
-def local_of_unit_or_unit_one_sub [comm_ring α] (hnze : (0:α) ≠ 1)
-  (h : ∀ x : α, is_unit x ∨ is_unit (1 - x)) : local_ring α :=
-local_of_is_local_ring ⟨hnze, h⟩
-
-def local_of_nonunits_ideal [comm_ring α] (hnze : (0:α) ≠ 1)
+lemma local_of_nonunits_ideal [comm_ring α] (hnze : (0:α) ≠ 1)
   (h : ∀ x y ∈ nonunits α, x + y ∈ nonunits α) : local_ring α :=
-local_of_is_local_ring ⟨hnze,
-λ x, or_iff_not_imp_left.mpr $ λ hx,
+{ zero_ne_one := 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⟩
+end}
 
-def local_of_unique_max_ideal [comm_ring α] (h : ∃! I : ideal α, I.is_maximal) :
+lemma local_of_unique_max_ideal [comm_ring α] (h : ∃! I : ideal α, I.is_maximal) :
   local_ring α :=
 local_of_nonunits_ideal
 (let ⟨I, Imax, _⟩ := h in (λ (H : 0 = 1), Imax.1 $ I.eq_top_iff_one.2 $ H ▸ I.zero_mem))
@@ -459,6 +459,9 @@ Imax.1 $ I.eq_top_of_is_unit_mem (I.add_mem xmemI ymemI) H
 
 section prio
 set_option default_priority 100 -- see Note [default priority]
+/-- A local ring homomorphism is a homomorphism between local rings
+  such that the image of the maximal ideal of the source is contained within
+  the maximal ideal of the target. -/
 class is_local_ring_hom [semiring α] [semiring β] (f : α →+* β) : Prop :=
 (map_nonunit : ∀ a, is_unit (f a) → is_unit a)
 end prio
@@ -469,33 +472,37 @@ is_local_ring_hom.map_nonunit a h
 
 section
 open local_ring
-variables [local_ring α] [local_ring β]
+variables [comm_ring α] [local_ring α] [comm_ring β] [local_ring β]
 variables (f : α →+* β) [is_local_ring_hom f]
 
-lemma map_nonunit (a) (h : a ∈ nonunits_ideal α) : f a ∈ nonunits_ideal β :=
+lemma map_nonunit (a) (h : a ∈ maximal_ideal α) : f a ∈ maximal_ideal β :=
 λ H, h $ is_unit_of_map_unit f a H
 
 end
 
 namespace local_ring
-variables [local_ring α] [local_ring β]
+variables [comm_ring α] [local_ring α] [comm_ring β] [local_ring β]
 
 variable (α)
-def residue_field := (nonunits_ideal α).quotient
+/-- The residue field of a local ring is the quotient of the ring by its maximal ideal. -/
+def residue_field := (maximal_ideal α).quotient
 
 noncomputable instance residue_field.field : field (residue_field α) :=
-ideal.quotient.field (nonunits_ideal α)
+ideal.quotient.field (maximal_ideal α)
+
+noncomputable instance : inhabited (residue_field α) := ⟨37⟩
 
-/-- The quotient map from a local ring to it's residue field. -/
+/-- The quotient map from a local ring to its residue field. -/
 def residue : α →+* (residue_field α) :=
 ideal.quotient.mk_hom _
 
 namespace residue_field
 
 variables {α β}
+/-- The map on residue fields induced by a local homomorphism between local rings -/
 noncomputable def map (f : α →+* β) [is_local_ring_hom f] :
   residue_field α →+* residue_field β :=
-ideal.quotient.lift (nonunits_ideal α) ((ideal.quotient.mk_hom _).comp f) $
+ideal.quotient.lift (maximal_ideal α) ((ideal.quotient.mk_hom _).comp f) $
 λ a ha,
 begin
   erw ideal.quotient.eq_zero_iff_mem,

src/ring_theory/power_series.lean

@@ -424,7 +424,7 @@ end map
 section trunc
 variables [comm_semiring α] (n : σ →₀ ℕ)
 
--- Auxiliary definition for the truncation function.
+/-- Auxiliary definition for the truncation function. -/
 def trunc_fun (φ : mv_power_series σ α) : mv_polynomial σ α :=
 { support := (n.antidiagonal.support.image prod.fst).filter (λ m, coeff α m φ ≠ 0),
   to_fun := λ m, if m ≤ n then coeff α m φ else 0,
@@ -600,15 +600,13 @@ section comm_ring
 variable [comm_ring α]
 
 /-- Multivariate formal power series over a local ring form a local ring.-/
-lemma is_local_ring (h : is_local_ring α) : is_local_ring (mv_power_series σ α) :=
-begin
-  split,
-  { have H : (0:α) ≠ 1 := ‹is_local_ring α›.1, contrapose! H,
+instance is_local_ring [local_ring α] : local_ring (mv_power_series σ α) :=
+{ zero_ne_one := by { have H : (0:α) ≠ 1 := ‹local_ring α›.zero_ne_one, contrapose! H,
     simpa using congr_arg (constant_coeff σ α) H },
-  { intro φ, rcases ‹is_local_ring α›.2 (constant_coeff σ α φ) with ⟨u,h⟩|⟨u,h⟩; [left, right];
+  is_local := by { intro φ, rcases local_ring.is_local (constant_coeff σ α φ) with ⟨u,h⟩|⟨u,h⟩;
+    [left, right];
     { refine is_unit_of_mul_eq_one _ _ (mul_inv_of_unit _ u _),
-      simpa using h.symm } }
-end
+      simpa using h.symm } } }
 
 -- TODO(jmc): once adic topology lands, show that this is complete
 
@@ -632,11 +630,13 @@ end, congr_arg X⟩
 end nonzero
 
 section local_ring
-variables {β : Type*} [local_ring α] [local_ring β] (f : α →+* β) [is_local_ring_hom f]
+variables {β : Type*} [comm_ring α] [comm_ring β] (f : α →+* β)
+  [is_local_ring_hom f]
 
-instance : local_ring (mv_power_series σ α) :=
-local_of_is_local_ring $ is_local_ring ⟨zero_ne_one, local_ring.is_local⟩
+-- Thanks to the linter for informing us that  this instance does
+-- not actually need α and β to be local rings!
 
+/-- The map `A[[X]] → B[[X]]` induced by a local ring hom `A → B` is local -/
 instance map.is_local_ring_hom : is_local_ring_hom (map σ f) :=
 ⟨begin
   rintros φ ⟨ψ, h⟩,
@@ -648,11 +648,18 @@ instance map.is_local_ring_hom : is_local_ring_hom (map σ f) :=
   exact is_unit_of_mul_eq_one φ (inv_of_unit φ c) (mul_inv_of_unit φ c hc.symm)
 end⟩
 
+variables [local_ring α] [local_ring β]
+
+instance : local_ring (mv_power_series σ α) :=
+{ zero_ne_one := zero_ne_one,
+  is_local := local_ring.is_local }
+
 end local_ring
 
 section field
 variables [field α]
 
+/-- The inverse `1/f` of a multivariable power series `f` over a field -/
 protected def inv (φ : mv_power_series σ α) : mv_power_series σ α :=
 inv.aux (constant_coeff σ α φ)⁻¹ φ
 
@@ -1051,6 +1058,7 @@ end comm_semiring
 section ring
 variables [ring α]
 
+/-- Auxiliary function used for computing inverse of a power series -/
 protected def inv.aux : α → power_series α → power_series α :=
 mv_power_series.inv.aux
 
@@ -1164,29 +1172,23 @@ end
 end integral_domain
 
 section local_ring
-variables [comm_ring α]
+variables {β : Type*} [comm_ring α] [comm_ring β]
+  (f : α →+* β) [is_local_ring_hom f]
 
-lemma is_local_ring (h : is_local_ring α) :
-  is_local_ring (power_series α) :=
-mv_power_series.is_local_ring h
-
-end local_ring
+instance map.is_local_ring_hom : is_local_ring_hom (map f) :=
+mv_power_series.map.is_local_ring_hom f
 
-section local_ring
-variables {β : Type*} [local_ring α] [local_ring β] (f : α →+* β) [is_local_ring_hom f]
+variables [local_ring α] [local_ring β]
 
 instance : local_ring (power_series α) :=
 mv_power_series.local_ring
 
-instance map.is_local_ring_hom :
-  is_local_ring_hom (map f) :=
-mv_power_series.map.is_local_ring_hom f
-
 end local_ring
 
 section field
 variables [field α]
 
+/-- The inverse 1/f of a power series f defined over a field -/
 protected def inv : power_series α → power_series α :=
 mv_power_series.inv