chore(data/polynomial/ring_division): remove nontrivial assumptions (#12984)

Additionally, this removes:

* some `polynomial.monic` assumptions that can be handled by casing instead
* the explicit `R` argument from `is_field.to_field R hR`

Author: eric-wieser

src/algebra/field/basic.lean

@@ -243,10 +243,16 @@ lemma field.to_is_field (R : Type u) [field R] : is_field R :=
 { mul_inv_cancel := λ a ha, ⟨a⁻¹, field.mul_inv_cancel ha⟩,
   ..‹field R› }
 
+@[simp] lemma is_field.nontrivial {R : Type u} [ring R] (h : is_field R) : nontrivial R :=
+⟨h.exists_pair_ne⟩
+
+@[simp] lemma not_is_field_of_subsingleton (R : Type u) [ring R] [subsingleton R] : ¬is_field R :=
+λ h, let ⟨x, y, h⟩ := h.exists_pair_ne in h (subsingleton.elim _ _)
+
 open_locale classical
 
 /-- Transferring from is_field to field -/
-noncomputable def is_field.to_field (R : Type u) [ring R] (h : is_field R) : field R :=
+noncomputable def is_field.to_field {R : Type u} [ring R] (h : is_field R) : field R :=
 { inv := λ a, if ha : a = 0 then 0 else classical.some (is_field.mul_inv_cancel h ha),
   inv_zero := dif_pos rfl,
   mul_inv_cancel := λ a ha,

src/algebraic_geometry/prime_spectrum/basic.lean

@@ -417,7 +417,7 @@ begin
       (is_closed_singleton_iff_is_maximal _).1 (t1_space.t1 ⟨⊥, hbot⟩)) (not_not.2 rfl)) },
   { refine ⟨λ x, (is_closed_singleton_iff_is_maximal x).2 _⟩,
     by_cases hx : x.as_ideal = ⊥,
-    { exact hx.symm ▸ @ideal.bot_is_maximal R (@field.to_division_ring _ $ is_field.to_field R h) },
+    { exact hx.symm ▸ @ideal.bot_is_maximal R (@field.to_division_ring _ h.to_field) },
     { exact absurd h (ring.not_is_field_iff_exists_prime.2 ⟨x.as_ideal, ⟨hx, x.2⟩⟩) } }
 end
 

src/data/polynomial/basic.lean

@@ -397,8 +397,8 @@ lemma coeff_C_ne_zero (h : n ≠ 0) : (C a).coeff n = 0 :=
 by rw [coeff_C, if_neg h]
 
 theorem nontrivial.of_polynomial_ne (h : p ≠ q) : nontrivial R :=
-⟨⟨0, 1, λ h01 : 0 = 1, h $
-    by rw [← mul_one p, ← mul_one q, ← C_1, ← h01, C_0, mul_zero, mul_zero] ⟩⟩
+nontrivial_of_ne 0 1 $ λ h01, h $
+  by rw [← mul_one p, ← mul_one q, ← C_1, ← h01, C_0, mul_zero, mul_zero]
 
 lemma monomial_eq_C_mul_X : ∀{n}, monomial n a = C a * X^n
 | 0     := (mul_one _).symm
@@ -710,6 +710,10 @@ mt (congr_arg (λ p, coeff p 1)) (by simp)
 
 end nonzero_semiring
 
+@[simp] lemma nontrivial_iff [semiring R] : nontrivial R[X] ↔ nontrivial R :=
+⟨λ h, let ⟨r, s, hrs⟩ := @exists_pair_ne _ h in nontrivial.of_polynomial_ne hrs,
+  λ h, @polynomial.nontrivial _ _ h⟩
+
 section repr
 variables [semiring R]
 open_locale classical

src/data/polynomial/div.lean

@@ -39,8 +39,7 @@ variables [comm_semiring R] {p q : R[X]}
 
 lemma multiplicity_finite_of_degree_pos_of_monic (hp : (0 : with_bot ℕ) < degree p)
   (hmp : monic p) (hq : q ≠ 0) : multiplicity.finite p q :=
-have zn0 : (0 : R) ≠ 1, from λ h, by haveI := subsingleton_of_zero_eq_one h;
-  exact hq (subsingleton.elim _ _),
+have zn0 : (0 : R) ≠ 1, by haveI := nontrivial.of_polynomial_ne hq; exact zero_ne_one,
 ⟨nat_degree q, λ ⟨r, hr⟩,
   have hp0 : p ≠ 0, from λ hp0, by simp [hp0] at hp; contradiction,
   have hr0 : r ≠ 0, from λ hr0, by simp * at *,
@@ -405,17 +404,20 @@ begin
   ... = p.sum f : p.sum_def _
 end
 
-lemma sum_mod_by_monic_coeff [nontrivial R] (hq : q.monic)
-  {n : ℕ} (hn : q.degree ≤ n) :
+lemma sum_mod_by_monic_coeff (hq : q.monic) {n : ℕ} (hn : q.degree ≤ n) :
   ∑ (i : fin n), monomial i ((p %ₘ q).coeff i) = p %ₘ q :=
-(sum_fin (λ i c, monomial i c) (by simp)
-  ((degree_mod_by_monic_lt _ hq).trans_le hn)).trans
-  (sum_monomial_eq _)
+begin
+  nontriviality R,
+  exact (sum_fin (λ i c, monomial i c) (by simp)
+    ((degree_mod_by_monic_lt _ hq).trans_le hn)).trans
+    (sum_monomial_eq _)
+end
 
 variable (R)
 
-lemma not_is_field [nontrivial R] : ¬ is_field R[X] :=
+lemma not_is_field : ¬ is_field R[X] :=
 begin
+  nontriviality R,
   rw ring.not_is_field_iff_exists_ideal_bot_lt_and_lt_top,
   use ideal.span {polynomial.X},
   split,
@@ -440,11 +442,13 @@ open_locale classical
 
 lemma multiplicity_X_sub_C_finite (a : R) (h0 : p ≠ 0) :
   multiplicity.finite (X - C a) p :=
-multiplicity_finite_of_degree_pos_of_monic
-  (have (0 : R) ≠ 1, from (λ h, by haveI := subsingleton_of_zero_eq_one h;
-      exact h0 (subsingleton.elim _ _)),
-    by haveI : nontrivial R := ⟨⟨0, 1, this⟩⟩; rw degree_X_sub_C; exact dec_trivial)
-    (monic_X_sub_C _) h0
+begin
+  haveI := nontrivial.of_polynomial_ne h0,
+  refine multiplicity_finite_of_degree_pos_of_monic _ (monic_X_sub_C _) h0,
+  rw degree_X_sub_C,
+  dec_trivial,
+end
+
 /-- The largest power of `X - C a` which divides `p`.
 This is computable via the divisibility algorithm `decidable_dvd_monic`. -/
 def root_multiplicity (a : R) (p : R[X]) : ℕ :=

src/data/polynomial/ring_division.lean

@@ -43,39 +43,45 @@ lemma aeval_mod_by_monic_eq_self_of_root [algebra R S]
   aeval x (p %ₘ q) = aeval x p :=
 eval₂_mod_by_monic_eq_self_of_root hq hx
 
-lemma mod_by_monic_eq_of_dvd_sub [nontrivial R] (hq : q.monic) {p₁ p₂ : R[X]}
+lemma mod_by_monic_eq_of_dvd_sub (hq : q.monic) {p₁ p₂ : R[X]}
   (h : q ∣ (p₁ - p₂)) :
   p₁ %ₘ q = p₂ %ₘ q :=
 begin
+  nontriviality R,
   obtain ⟨f, sub_eq⟩ := h,
   refine (div_mod_by_monic_unique (p₂ /ₘ q + f) _ hq
     ⟨_, degree_mod_by_monic_lt _ hq⟩).2,
   rw [sub_eq_iff_eq_add.mp sub_eq, mul_add, ← add_assoc, mod_by_monic_add_div _ hq, add_comm]
 end
 
-lemma add_mod_by_monic [nontrivial R] (hq : q.monic)
-  (p₁ p₂ : R[X]) : (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q :=
-(div_mod_by_monic_unique (p₁ /ₘ q + p₂ /ₘ q) _ hq
-  ⟨by rw [mul_add, add_left_comm, add_assoc, mod_by_monic_add_div _ hq, ← add_assoc,
-          add_comm (q * _), mod_by_monic_add_div _ hq],
-    (degree_add_le _ _).trans_lt (max_lt (degree_mod_by_monic_lt _ hq)
-      (degree_mod_by_monic_lt _ hq))⟩).2
+lemma add_mod_by_monic (p₁ p₂ : R[X]) : (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q :=
+begin
+  by_cases hq : q.monic,
+  { nontriviality R,
+    exact (div_mod_by_monic_unique (p₁ /ₘ q + p₂ /ₘ q) _ hq
+      ⟨by rw [mul_add, add_left_comm, add_assoc, mod_by_monic_add_div _ hq, ← add_assoc,
+              add_comm (q * _), mod_by_monic_add_div _ hq],
+        (degree_add_le _ _).trans_lt (max_lt (degree_mod_by_monic_lt _ hq)
+          (degree_mod_by_monic_lt _ hq))⟩).2 },
+  { simp_rw mod_by_monic_eq_of_not_monic _ hq }
+end
 
-lemma smul_mod_by_monic [nontrivial R] (hq : q.monic)
-  (c : R) (p : R[X]) : (c • p) %ₘ q = c • (p %ₘ q) :=
-(div_mod_by_monic_unique (c • (p /ₘ q)) (c • (p %ₘ q)) hq
-  ⟨by rw [mul_smul_comm, ← smul_add, mod_by_monic_add_div p hq],
-   (degree_smul_le _ _).trans_lt (degree_mod_by_monic_lt _ hq)⟩).2
+lemma smul_mod_by_monic (c : R) (p : R[X]) : (c • p) %ₘ q = c • (p %ₘ q) :=
+begin
+  by_cases hq : q.monic,
+  { nontriviality R,
+    exact (div_mod_by_monic_unique (c • (p /ₘ q)) (c • (p %ₘ q)) hq
+      ⟨by rw [mul_smul_comm, ← smul_add, mod_by_monic_add_div p hq],
+      (degree_smul_le _ _).trans_lt (degree_mod_by_monic_lt _ hq)⟩).2 },
+  { simp_rw mod_by_monic_eq_of_not_monic _ hq }
+end
 
-/--
-`polynomial.mod_by_monic_hom (hq : monic (q : R[X]))` is `_ %ₘ q` as a `R`-linear map.
--/
+/--  `_ %ₘ q` as an `R`-linear map. -/
 @[simps]
-def mod_by_monic_hom [nontrivial R] (hq : q.monic) :
-  R[X] →ₗ[R] R[X] :=
+def mod_by_monic_hom (q : R[X]) : R[X] →ₗ[R] R[X] :=
 { to_fun := λ p, p %ₘ q,
-  map_add' := add_mod_by_monic hq,
-  map_smul' := smul_mod_by_monic hq }
+  map_add' := add_mod_by_monic,
+  map_smul' := smul_mod_by_monic }
 
 end comm_ring
 

src/field_theory/cardinality.lean

@@ -55,7 +55,7 @@ end
 
 lemma fintype.not_is_field_of_card_not_prime_pow {α} [fintype α] [ring α] :
   ¬ is_prime_pow (‖α‖) → ¬ is_field α :=
-mt $ λ h, fintype.nonempty_field_iff.mp ⟨h.to_field α⟩
+mt $ λ h, fintype.nonempty_field_iff.mp ⟨h.to_field⟩
 
 /-- Any infinite type can be endowed a field structure. -/
 lemma infinite.nonempty_field {α : Type u} [infinite α] : nonempty (field α) :=

src/field_theory/is_alg_closed/basic.lean

@@ -265,7 +265,7 @@ begin
   intros x _,
   let p := minpoly K x,
   let N : subalgebra K L := (maximal_subfield_with_hom M hL).carrier,
-  letI : field N := is_field.to_field _ (subalgebra.is_field_of_algebraic N hL),
+  letI : field N := (subalgebra.is_field_of_algebraic N hL).to_field,
   letI : algebra N M := (maximal_subfield_with_hom M hL).emb.to_ring_hom.to_algebra,
   cases is_alg_closed.exists_aeval_eq_zero M (minpoly N x)
     (ne_of_gt (minpoly.degree_pos

src/ring_theory/adjoin_root.lean

@@ -227,31 +227,31 @@ lemma is_integral_root' (hg : g.monic) : is_integral R (root g) :=
 /-- `adjoin_root.mod_by_monic_hom` sends the equivalence class of `f` mod `g` to `f %ₘ g`.
 
 This is a well-defined right inverse to `adjoin_root.mk`, see `adjoin_root.mk_left_inverse`. -/
-def mod_by_monic_hom [nontrivial R] (hg : g.monic) :
+def mod_by_monic_hom (hg : g.monic) :
   adjoin_root g →ₗ[R] R[X] :=
-(submodule.liftq _ (polynomial.mod_by_monic_hom hg)
+(submodule.liftq _ (polynomial.mod_by_monic_hom g)
   (λ f (hf : f ∈ (ideal.span {g}).restrict_scalars R),
     (mem_ker_mod_by_monic hg).mpr (ideal.mem_span_singleton.mp hf))).comp $
 (submodule.quotient.restrict_scalars_equiv R (ideal.span {g} : ideal R[X]))
   .symm.to_linear_map
 
-@[simp] lemma mod_by_monic_hom_mk [nontrivial R] (hg : g.monic) (f : R[X]) :
+@[simp] lemma mod_by_monic_hom_mk (hg : g.monic) (f : R[X]) :
   mod_by_monic_hom hg (mk g f) = f %ₘ g := rfl
 
-lemma mk_left_inverse [nontrivial R] (hg : g.monic) :
+lemma mk_left_inverse (hg : g.monic) :
   function.left_inverse (mk g) (mod_by_monic_hom hg) :=
 λ f, induction_on g f $ λ f, begin
   rw [mod_by_monic_hom_mk hg, mk_eq_mk, mod_by_monic_eq_sub_mul_div _ hg,
       sub_sub_cancel_left, dvd_neg],
   apply dvd_mul_right
 end
 
-lemma mk_surjective [nontrivial R] (hg : g.monic) : function.surjective (mk g) :=
+lemma mk_surjective (hg : g.monic) : function.surjective (mk g) :=
 (mk_left_inverse hg).surjective
 
 /-- The elements `1, root g, ..., root g ^ (d - 1)` form a basis for `adjoin_root g`,
 where `g` is a monic polynomial of degree `d`. -/
-@[simps] def power_basis_aux' [nontrivial R] (hg : g.monic) :
+@[simps] def power_basis_aux' (hg : g.monic) :
   basis (fin g.nat_degree) R (adjoin_root g) :=
 basis.of_equiv_fun
 { to_fun := λ f i, (mod_by_monic_hom hg f).coeff i,
@@ -265,6 +265,7 @@ basis.of_equiv_fun
          rw [mod_by_monic_eq_sub_mul_div _ hg, sub_sub_cancel],
          exact dvd_mul_right _ _ }),
   right_inv := λ x, funext $ λ i, begin
+    nontriviality R,
     simp only [mod_by_monic_hom_mk],
     rw [(mod_by_monic_eq_self_iff hg).mpr, finset_sum_coeff, finset.sum_eq_single i];
       try { simp only [coeff_monomial, eq_self_iff_true, if_true] },
@@ -279,8 +280,7 @@ basis.of_equiv_fun
 
 /-- The power basis `1, root g, ..., root g ^ (d - 1)` for `adjoin_root g`,
 where `g` is a monic polynomial of degree `d`. -/
-@[simps] def power_basis' [nontrivial R] (hg : g.monic) :
-  power_basis R (adjoin_root g) :=
+@[simps] def power_basis' (hg : g.monic) : power_basis R (adjoin_root g) :=
 { gen := root g,
   dim := g.nat_degree,
   basis := power_basis_aux' hg,

src/ring_theory/dedekind_domain/ideal.lean

@@ -430,7 +430,7 @@ begin
   by_cases hI1 : I = ⊤,
   { rw [hI1, coe_ideal_top, one_mul, fractional_ideal.one_inv] },
   by_cases hNF : is_field A,
-  { letI := hNF.to_field A, rcases hI1 (I.eq_bot_or_top.resolve_left hI0) },
+  { letI := hNF.to_field, rcases hI1 (I.eq_bot_or_top.resolve_left hI0) },
   -- We'll show a contradiction with `exists_not_mem_one_of_ne_bot`:
   -- `J⁻¹ = (I * I⁻¹)⁻¹` cannot have an element `x ∉ 1`, so it must equal `1`.
   obtain ⟨J, hJ⟩ : ∃ (J : ideal A), (J : fractional_ideal A⁰ K) = I * I⁻¹ :=

src/ring_theory/fractional_ideal.lean

@@ -978,7 +978,7 @@ end
 
 lemma eq_zero_or_one_of_is_field (hF : is_field R₁) (I : fractional_ideal R₁⁰ K) : I = 0 ∨ I = 1 :=
 begin
-  letI : field R₁ := hF.to_field R₁,
+  letI : field R₁ := hF.to_field,
   -- TODO can this be less ugly?
   exact @eq_zero_or_one R₁ K _ _ _ (by { unfreezingI {cases _inst_4}, convert _inst_9 }) I
 end