refactor(ring_theory): remove unbundled leftovers in ideal.quotient (#3467)

This PR aims to smooth some corners in the `ideal.quotient` namespace left by the move to bundled `ring_hom`s. The main irritation is the ambiguity between different ways to map `x : R` to the quotient ring: `quot.mk`, `quotient.mk`, `quotient.mk'`, `submodule.quotient.mk`, `ideal.quotient.mk` and `ideal.quotient.mk_hom`, which caused a lot of duplication and more awkward proofs.

The specific changes are:

 * delete function `ideal_quotient.mk`
 * rename ring hom `ideal.quotient.mk_hom` to `ideal.quotient.mk`
 * make new `ideal_quotient.mk` the `simp` normal form
 * delete obsolete `mk_eq_mk_hom`
 * delete obsolete `mk_...` `simp` lemmas (use `ring_hom.map_...` instead)
 * delete `quotient.map_mk` which was unused and had no lemmas (`ideal.map quotient.mk` is used elsewhere)

Author: Vierkantor

src/algebra/direct_limit.lean

@@ -287,7 +287,7 @@ comm_ring.to_ring _
 
 /-- The canonical map from a component to the direct limit. -/
 def of (i) (x : G i) : direct_limit G f :=
-ideal.quotient.mk _ $ of ⟨i, x⟩
+ideal.quotient.mk _ (of (⟨i, x⟩ : Σ i, G i))
 
 variables {G f}
 

src/number_theory/basic.lean

@@ -20,11 +20,11 @@ begin
   rw [nat.pow_succ, pow_mul, pow_mul, ← geom_sum₂_mul, pow_succ],
   refine mul_dvd_mul _ ih,
   let I : ideal R := span {p},
-  let f : R →+* ideal.quotient I := mk_hom I,
+  let f : R →+* ideal.quotient I := mk I,
   have hp : (p : ideal.quotient I) = 0,
-  { rw [← f.map_nat_cast, ← mk_eq_mk_hom, eq_zero_iff_mem, mem_span_singleton] },
-  rw [← mem_span_singleton, ← ideal.quotient.eq, mk_eq_mk_hom, mk_eq_mk_hom] at h,
-  rw [← mem_span_singleton, ← eq_zero_iff_mem, mk_eq_mk_hom, ring_hom.map_geom_series₂,
+  { rw [← f.map_nat_cast, eq_zero_iff_mem, mem_span_singleton] },
+  rw [← mem_span_singleton, ← ideal.quotient.eq] at h,
+  rw [← mem_span_singleton, ← eq_zero_iff_mem, ring_hom.map_geom_series₂,
       ring_hom.map_pow, ring_hom.map_pow, h, geom_series₂_self, hp, zero_mul],
 end
 

src/ring_theory/adjoin_root.lean

@@ -56,7 +56,7 @@ instance : inhabited (adjoin_root f) := ⟨0⟩
 instance : decidable_eq (adjoin_root f) := classical.dec_eq _
 
 /-- Ring homomorphism from `R[x]` to `adjoin_root f` sending `X` to the `root`. -/
-def mk : polynomial R →+* adjoin_root f := ideal.quotient.mk_hom _
+def mk : polynomial R →+* adjoin_root f := ideal.quotient.mk _
 
 @[elab_as_eliminator]
 theorem induction_on {C : adjoin_root f → Prop} (x : adjoin_root f)

src/ring_theory/eisenstein_criterion.lean

@@ -23,11 +23,10 @@ namespace eisenstein_criterion_aux
 
 lemma map_eq_C_mul_X_pow_of_forall_coeff_mem {f : polynomial R} {P : ideal R}
   (hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P) (hf0 : f ≠ 0) :
-  map (mk_hom P) f = C ((mk_hom P) f.leading_coeff) * X ^ f.nat_degree :=
+  map (mk P) f = C ((mk P) f.leading_coeff) * X ^ f.nat_degree :=
 polynomial.ext (λ n, begin
   rcases lt_trichotomy ↑n (degree f) with h | h | h,
-  { erw [coeff_map, ← mk_eq_mk_hom, eq_zero_iff_mem.2 (hfP n h),
-      coeff_C_mul, coeff_X_pow, if_neg, mul_zero],
+  { erw [coeff_map, eq_zero_iff_mem.2 (hfP n h), coeff_C_mul, coeff_X_pow, if_neg, mul_zero],
     rintro rfl, exact not_lt_of_ge degree_le_nat_degree h },
   { have : nat_degree f = n, from nat_degree_eq_of_degree_eq_some h.symm,
     rw [coeff_C_mul, coeff_X_pow, if_pos this.symm, mul_one, leading_coeff, this, coeff_map] },
@@ -39,17 +38,17 @@ end)
 
 lemma le_nat_degree_of_map_eq_mul_X_pow {n : ℕ}
   {P : ideal R} (hP : P.is_prime) {q : polynomial R} {c : polynomial P.quotient}
-  (hq : map (mk_hom P) q = c * X ^ n) (hc0 : c.degree = 0) : n ≤ q.nat_degree :=
+  (hq : map (mk P) q = c * X ^ n) (hc0 : c.degree = 0) : n ≤ q.nat_degree :=
 with_bot.coe_le_coe.1
-  (calc ↑n = degree (q.map (mk_hom P)) :
+  (calc ↑n = degree (q.map (mk P)) :
       by rw [hq, degree_mul, hc0, zero_add, degree_pow, degree_X, nsmul_one, nat.cast_with_bot]
       ... ≤ degree q : degree_map_le _
       ... ≤ nat_degree q : degree_le_nat_degree)
 
 lemma eval_zero_mem_ideal_of_eq_mul_X_pow {n : ℕ} {P : ideal R}
   {q : polynomial R} {c : polynomial P.quotient}
-  (hq : map (mk_hom P) q = c * X ^ n) (hn0 : 0 < n) : eval 0 q ∈ P :=
-by rw [← coeff_zero_eq_eval_zero, ← eq_zero_iff_mem, mk_eq_mk_hom, ← coeff_map,
+  (hq : map (mk P) q = c * X ^ n) (hn0 : 0 < n) : eval 0 q ∈ P :=
+by rw [← coeff_zero_eq_eval_zero, ← eq_zero_iff_mem, ← coeff_map,
     coeff_zero_eq_eval_zero, hq, eval_mul, eval_pow, eval_X, zero_pow hn0, mul_zero]
 
 lemma is_unit_of_nat_degree_eq_zero_of_forall_dvd_is_unit {p q : polynomial R}
@@ -76,7 +75,7 @@ theorem irreducible_of_eisenstein_criterion {f : polynomial R} {P : ideal R} (hP
   (hfd0 : 0 < degree f) (h0 : f.coeff 0 ∉ P^2)
   (hu : ∀ x : R, C x ∣ f → is_unit x) : irreducible f :=
 have hf0 : f ≠ 0, from λ _, by simp only [*, not_true, submodule.zero_mem, coeff_zero] at *,
-have hf : f.map (mk_hom P) = C (mk_hom P (leading_coeff f)) * X ^ nat_degree f,
+have hf : f.map (mk P) = C (mk P (leading_coeff f)) * X ^ nat_degree f,
   from map_eq_C_mul_X_pow_of_forall_coeff_mem hfP hf0,
 have hfd0 : 0 < f.nat_degree, from with_bot.coe_lt_coe.1
   (lt_of_lt_of_le hfd0 degree_le_nat_degree),
@@ -94,8 +93,8 @@ begin
     exact ideal.mul_mem_mul
       (eval_zero_mem_ideal_of_eq_mul_X_pow hp hm0)
       (eval_zero_mem_ideal_of_eq_mul_X_pow hq hn0) },
-  have hpql0 : (mk_hom P) (p * q).leading_coeff ≠ 0,
-  { rwa [← mk_eq_mk_hom, ne.def, eq_zero_iff_mem] },
+  have hpql0 : (mk P) (p * q).leading_coeff ≠ 0,
+  { rwa [ne.def, eq_zero_iff_mem] },
   have hp0 : p ≠ 0, from λ h, by simp only [*, zero_mul, eq_self_iff_true, not_true, ne.def] at *,
   have hq0 : q ≠ 0, from λ h, by simp only [*, eq_self_iff_true, not_true, ne.def, mul_zero] at *,
   have hbc0 : degree b = 0 ∧ degree c = 0,

src/ring_theory/ideal_operations.lean

@@ -180,9 +180,9 @@ begin
     { split_ifs with h, { apply hg1 }, rw sub_self, exact (f i).zero_mem },
     { intros hjs hji, rw dif_pos, { apply hg2 }, exact ⟨hjs, hji⟩ } },
   rcases this with ⟨g, hgi, hgj⟩, use (∏ x in s.erase i, g x), split,
-  { rw [← quotient.eq, quotient.mk_one, quotient.mk_prod],
-    apply finset.prod_eq_one, intros, rw [← quotient.mk_one, quotient.eq], apply hgi },
-  intros j hjs hji, rw [← quotient.eq_zero_iff_mem, quotient.mk_prod],
+  { rw [← quotient.eq, ring_hom.map_one, ring_hom.map_prod],
+    apply finset.prod_eq_one, intros, rw [← ring_hom.map_one, quotient.eq], apply hgi },
+  intros j hjs hji, rw [← quotient.eq_zero_iff_mem, ring_hom.map_prod],
   refine finset.prod_eq_zero (finset.mem_erase_of_ne_of_mem hji hjs) _,
   rw quotient.eq_zero_iff_mem, exact hgj j hjs hji
 end
@@ -199,20 +199,20 @@ begin
   rcases this with ⟨φ, hφ1, hφ2⟩,
   use ∑ i, g i * φ i,
   intros i,
-  rw [← quotient.eq, quotient.mk_sum],
+  rw [← quotient.eq, ring_hom.map_sum],
   refine eq.trans (finset.sum_eq_single i _ _) _,
   { intros j _ hji, rw quotient.eq_zero_iff_mem, exact (f i).mul_mem_left (hφ2 j i hji) },
   { intros hi, exact (hi $ finset.mem_univ i).elim },
-  specialize hφ1 i, rw [← quotient.eq, quotient.mk_one] at hφ1,
-  rw [quotient.mk_mul, hφ1, mul_one]
+  specialize hφ1 i, rw [← quotient.eq, ring_hom.map_one] at hφ1,
+  rw [ring_hom.map_mul, hφ1, mul_one]
 end
 
 def quotient_inf_to_pi_quotient (f : ι → ideal R) :
   (⨅ i, f i).quotient →+* Π i, (f i).quotient :=
 begin
   refine quotient.lift (⨅ i, f i) _ _,
   { convert @@pi.ring_hom (λ i, quotient (f i)) (λ i, ring.to_semiring) ring.to_semiring
-      (λ i, quotient.mk_hom (f i)) },
+      (λ i, quotient.mk (f i)) },
   { intros r hr,
     rw submodule.mem_infi at hr,
     ext i,
@@ -552,7 +552,7 @@ le_antisymm (λ r ⟨n, hfrnk⟩, ⟨n, show f (r ^ n) ∈ K,
 (λ r ⟨n, hfrnk⟩, ⟨n, f.map_pow r n ▸ hfrnk⟩)
 
 @[simp] lemma map_quotient_self :
-  map (quotient.mk_hom I) I = ⊥ :=
+  map (quotient.mk I) I = ⊥ :=
 eq_bot_iff.2 $ ideal.map_le_iff_le_comap.2 $ λ x hx,
 (submodule.mem_bot I.quotient).2 $ ideal.quotient.eq_zero_iff_mem.2 hx
 

src/ring_theory/ideals.lean

@@ -180,72 +180,42 @@ 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⟩
-
-@[simp] lemma mk_one (I : ideal α) : mk I 1 = 1 := rfl
+instance (I : ideal α) : has_one I.quotient := ⟨submodule.quotient.mk 1⟩
 
 instance (I : ideal α) : has_mul I.quotient :=
-⟨λ a b, quotient.lift_on₂' a b (λ a b, mk I (a * b)) $
+⟨λ a b, quotient.lift_on₂' a b (λ a b, submodule.quotient.mk (a * b)) $
  λ a₁ a₂ b₁ b₂ h₁ h₂, quot.sound $ begin
   refine calc a₁ * a₂ - b₁ * b₂ = a₂ * (a₁ - b₁) + (a₂ - b₂) * b₁ : _
   ... ∈ I : I.add_mem (I.mul_mem_left h₁) (I.mul_mem_right h₂),
   rw [mul_sub, sub_mul, sub_add_sub_cancel, mul_comm, mul_comm b₁]
  end⟩
 
-@[simp] theorem mk_mul : mk I (x * y) = mk I x * mk I y := rfl
-
 instance (I : ideal α) : comm_ring I.quotient :=
 { mul := (*),
   one := 1,
   mul_assoc := λ a b c, quotient.induction_on₃' a b c $
-    λ a b c, congr_arg (mk _) (mul_assoc a b c),
+    λ a b c, congr_arg submodule.quotient.mk (mul_assoc a b c),
   mul_comm := λ a b, quotient.induction_on₂' a b $
-    λ a b, congr_arg (mk _) (mul_comm a b),
+    λ a b, congr_arg submodule.quotient.mk (mul_comm a b),
   one_mul := λ a, quotient.induction_on' a $
-    λ a, congr_arg (mk _) (one_mul a),
+    λ a, congr_arg submodule.quotient.mk (one_mul a),
   mul_one := λ a, quotient.induction_on' a $
-    λ a, congr_arg (mk _) (mul_one a),
+    λ a, congr_arg submodule.quotient.mk (mul_one a),
   left_distrib := λ a b c, quotient.induction_on₃' a b c $
-    λ a b c, congr_arg (mk _) (left_distrib a b c),
+    λ a b c, congr_arg submodule.quotient.mk (left_distrib a b c),
   right_distrib := λ a b c, quotient.induction_on₃' a b c $
-    λ a b c, congr_arg (mk _) (right_distrib a b c),
+    λ a b c, congr_arg submodule.quotient.mk (right_distrib a b c),
   ..submodule.quotient.add_comm_group I }
 
-/-- `ideal.quotient.mk` as a `ring_hom` -/
-def mk_hom (I : ideal α) : α →+* I.quotient := ⟨mk I, rfl, λ _ _, rfl, rfl, λ _ _, rfl⟩
-
-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⟩,
-  add_mem' := by rintro _ _ ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩;
-    exact ⟨x + y, J.add_mem hx hy, rfl⟩,
-  smul_mem' := by rintro ⟨c⟩ _ ⟨x, hx, rfl⟩;
-    exact ⟨c * x, J.mul_mem_left hx, rfl⟩ }
+/-- The ring homomorphism from a ring `R` to a quotient ring `R/I`. -/
+def mk (I : ideal α) : α →+* I.quotient :=
+⟨λ a, submodule.quotient.mk a, rfl, λ _ _, rfl, rfl, λ _ _, rfl⟩
 
-@[simp] lemma mk_zero (I : ideal α) : mk I 0 = 0 := rfl
-@[simp] lemma mk_add (I : ideal α) (a b : α) : mk I (a + b) = mk I a + mk I b := rfl
-@[simp] lemma mk_neg (I : ideal α) (a : α) : mk I (-a : α) = -mk I a := rfl
-@[simp] lemma mk_sub (I : ideal α) (a b : α) : mk I (a - b : α) = mk I a - mk I b := rfl
-@[simp] lemma mk_pow (I : ideal α) (a : α) (n : ℕ) : mk I (a ^ n : α) = mk I a ^ n :=
-(mk_hom I).map_pow a n
+instance : inhabited (quotient I) := ⟨mk I 37⟩
 
-lemma mk_prod {ι} (I : ideal α) (s : finset ι) (f : ι → α) :
-  mk I (∏ i in s, f i) = ∏ i in s, mk I (f i) :=
-(mk_hom I).map_prod f s
+protected theorem eq : mk I x = mk I y ↔ x - y ∈ I := submodule.quotient.eq I
 
-lemma mk_sum {ι} (I : ideal α) (s : finset ι) (f : ι → α) :
-  mk I (∑ i in s, f i) = ∑ i in s, mk I (f i) :=
-(mk_hom I).map_sum f s
+@[simp] theorem mk_eq_mk (x : α) : (submodule.quotient.mk x : quotient I) = mk I x := rfl
 
 lemma eq_zero_iff_mem {I : ideal α} : mk I a = 0 ↔ a ∈ I :=
 by conv {to_rhs, rw ← sub_zero a }; exact quotient.eq'
@@ -505,15 +475,15 @@ noncomputable instance : inhabited (residue_field α) := ⟨37⟩
 
 /-- The quotient map from a local ring to its residue field. -/
 def residue : α →+* (residue_field α) :=
-ideal.quotient.mk_hom _
+ideal.quotient.mk _
 
 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 (maximal_ideal α) ((ideal.quotient.mk_hom _).comp f) $
+ideal.quotient.lift (maximal_ideal α) ((ideal.quotient.mk _).comp f) $
 λ a ha,
 begin
   erw ideal.quotient.eq_zero_iff_mem,

src/ring_theory/noetherian.lean

@@ -92,8 +92,8 @@ begin
     { rw [sub_right_comm], exact I.sub_mem hr1 hci },
     { rw [sub_smul, ← hyz, add_sub_cancel'], exact hz } },
   rcases this with ⟨c, hc1, hci⟩, refine ⟨c * r, _, _, hs.2⟩,
-  { rw [← ideal.quotient.eq, ideal.quotient.mk_one] at hr1 hc1 ⊢,
-    rw [ideal.quotient.mk_mul, hc1, hr1, mul_one] },
+  { rw [← ideal.quotient.eq, ring_hom.map_one] at hr1 hc1 ⊢,
+    rw [ring_hom.map_mul, hc1, hr1, mul_one] },
   { intros n hn, specialize hrn hn, rw [mem_comap, mem_sup] at hrn,
     rcases hrn with ⟨y, hy, z, hz, hyz⟩, change y + z = r • n at hyz,
     rw mem_smul_span_singleton at hy, rcases hy with ⟨d, hdi, rfl⟩,

src/ring_theory/valuation/basic.lean

@@ -339,7 +339,7 @@ def on_quot {J : ideal R} (hJ : J ≤ supp v) :
   map_add'  := λ xbar ybar, quotient.ind₂' v.map_add xbar ybar }
 
 @[simp] lemma on_quot_comap_eq {J : ideal R} (hJ : J ≤ supp v) :
-  (v.on_quot hJ).comap (ideal.quotient.mk_hom J) = v :=
+  (v.on_quot hJ).comap (ideal.quotient.mk J) = v :=
 ext $ λ r,
 begin
   refine @quotient.lift_on_beta _ _ (J.quotient_rel) v (λ a b h, _) _,
@@ -356,16 +356,16 @@ begin
 end
 
 lemma self_le_supp_comap (J : ideal R) (v : valuation (quotient J) Γ₀) :
-  J ≤ (v.comap (ideal.quotient.mk_hom J)).supp :=
+  J ≤ (v.comap (ideal.quotient.mk J)).supp :=
 by { rw [comap_supp, ← ideal.map_le_iff_le_comap], simp }
 
 @[simp] lemma comap_on_quot_eq (J : ideal R) (v : valuation J.quotient Γ₀) :
-  (v.comap (ideal.quotient.mk_hom J)).on_quot (v.self_le_supp_comap J) = v :=
+  (v.comap (ideal.quotient.mk J)).on_quot (v.self_le_supp_comap J) = v :=
 ext $ by { rintro ⟨x⟩, refl }
 
 /-- The quotient valuation on R/J has support supp(v)/J if J ⊆ supp v. -/
 lemma supp_quot {J : ideal R} (hJ : J ≤ supp v) :
-  supp (v.on_quot hJ) = (supp v).map (ideal.quotient.mk_hom J) :=
+  supp (v.on_quot hJ) = (supp v).map (ideal.quotient.mk J) :=
 begin
   apply le_antisymm,
   { rintro ⟨x⟩ hx,