[Merged by Bors] - feat: units of polynomial rings

Mathlib/Data/Polynomial/RingDivision.lean

@@ -226,6 +226,8 @@ theorem degree_coe_units [Nontrivial R] (u : R[X]ˣ) : degree (u : R[X]) = 0 :=
   degree_eq_zero_of_isUnit ⟨u, rfl⟩
 #align polynomial.degree_coe_units Polynomial.degree_coe_units
 
+/-- Characterization of a unit of a polynomial ring over an integral domain `R`.
+See `Polynomial.isUnit_iff_coeff_isUnit_isNilpotent` when `R` is a commutative ring. -/
 theorem isUnit_iff : IsUnit p ↔ ∃ r : R, IsUnit r ∧ C r = p :=
   ⟨fun hp =>
     ⟨p.coeff 0,

Mathlib/RingTheory/Nilpotent.lean

@@ -11,6 +11,7 @@ Authors: Oliver Nash
 import Mathlib.Data.Nat.Choose.Sum
 import Mathlib.Algebra.Algebra.Bilinear
 import Mathlib.RingTheory.Ideal.Operations
+import Mathlib.Algebra.GeomSum
 
 /-!
 # Nilpotent elements
@@ -28,6 +29,8 @@ import Mathlib.RingTheory.Ideal.Operations
 
 universe u v
 
+open BigOperators
+
 variable {R S : Type u} {x y : R}
 
 /-- An element is said to be nilpotent if some natural-number-power of it equals zero.
@@ -64,6 +67,23 @@ theorem IsNilpotent.map [MonoidWithZero R] [MonoidWithZero S] {r : R} {F : Type
   rw [← map_pow, hr.choose_spec, map_zero]
 #align is_nilpotent.map IsNilpotent.map
 
+theorem IsNilpotent.sub_one_isUnit [Ring R] {r : R} (hnil : IsNilpotent r) : IsUnit (r - 1) := by
+  obtain ⟨n, hn⟩ := hnil
+  refine' ⟨⟨r - 1, -∑ i in Finset.range n, r ^ i, _, _⟩, rfl⟩
+  · rw [mul_neg, mul_geom_sum, hn]
+    simp
+  · rw [neg_mul, geom_sum_mul, hn]
+    simp
+
+theorem Commute.IsNilpotent.add_isUnit [Ring R] {r : R} {u : Rˣ} (hnil : IsNilpotent r)
+  (hru : Commute r (↑u⁻¹ : R)) : IsUnit (u + r) := by
+  rw [← Units.isUnit_mul_units _ u⁻¹, add_mul, Units.mul_inv, ← IsUnit.neg_iff, add_comm, neg_add,
+    ← sub_eq_add_neg]
+  obtain ⟨n, hn⟩ := hnil
+  refine' IsNilpotent.sub_one_isUnit ⟨n, _⟩
+  rw [neg_pow, hru.mul_pow, hn]
+  simp
+
 /-- A structure that has zero and pow is reduced if it has no nonzero nilpotent elements. -/
 @[mk_iff isReduced_iff]
 class IsReduced (R : Type _) [Zero R] [Pow R ℕ] : Prop where

Mathlib/RingTheory/Polynomial/Basic.lean

@@ -14,6 +14,7 @@ import Mathlib.Data.MvPolynomial.CommRing
 import Mathlib.Data.MvPolynomial.Equiv
 import Mathlib.RingTheory.Polynomial.Content
 import Mathlib.RingTheory.UniqueFactorizationDomain
+import Mathlib.RingTheory.Ideal.QuotientOperations
 
 /-!
 # Ring-theoretic supplement of Data.Polynomial.
@@ -256,6 +257,13 @@ theorem monic_geom_sum_X {n : ℕ} (hn : n ≠ 0) : (∑ i in range n, (X : R[X]
 set_option linter.uppercaseLean3 false in
 #align polynomial.monic_geom_sum_X Polynomial.monic_geom_sum_X
 
+theorem IsNilpotent.C_mul_X_pow_isNilpotent {r : R} (n : ℕ) (hnil : IsNilpotent r) :
+    IsNilpotent ((C r) * X ^ n) := by
+  refine' Commute.isNilpotent_mul_left (commute_X_pow _ _).symm _
+  obtain ⟨m, hm⟩ := hnil
+  refine' ⟨m, _⟩
+  rw [← C_pow, hm, C_0]
+
 end Semiring
 
 section Ring
@@ -460,6 +468,58 @@ theorem ker_modByMonicHom (hq : q.Monic) :
 
 end ModByMonic
 
+/-- Let `P` be a polynomial over `R`. If its constant term is a unit and its other coefficients are
+nilpotent, then `P` is a unit. -/
+theorem isUnit_of_coeff_isUnit_isNilpotent {P : Polynomial R} (hunit : IsUnit (P.coeff 0))
+    (hnil : ∀ i, i ≠ 0 → IsNilpotent (P.coeff i)) : IsUnit P := by
+  induction' h : P.natDegree using Nat.strong_induction_on with k hind generalizing P
+  by_cases hdeg : P.natDegree = 0
+  { rw [eq_C_of_natDegree_eq_zero hdeg]
+    exact hunit.map C }
+  set P₁ := P.eraseLead with hP₁
+  suffices IsUnit P₁ by
+    rw [← eraseLead_add_monomial_natDegree_leadingCoeff P, ← C_mul_X_pow_eq_monomial]
+    obtain ⟨Q, hQ⟩ := this
+    rw [← hP₁, ← hQ]
+    refine' Commute.IsNilpotent.add_isUnit (IsNilpotent.C_mul_X_pow_isNilpotent _ (hnil _ hdeg))
+      ((Commute.all _ _).mul_left (Commute.all _ _))
+  have hdeg₂ := lt_of_le_of_lt P.eraseLead_natDegree_le (Nat.sub_lt
+    (Nat.pos_of_ne_zero hdeg) zero_lt_one)
+  refine' hind P₁.natDegree _ _ (fun i hi => _) rfl
+  · simp_rw [← h, hdeg₂]
+  · simp_rw [eraseLead_coeff_of_ne _ (Ne.symm hdeg), hunit]
+  · by_cases H : i ≤ P₁.natDegree
+    simp_rw [eraseLead_coeff_of_ne _ (ne_of_lt (lt_of_le_of_lt H hdeg₂)), hnil i hi]
+    simp_rw [coeff_eq_zero_of_natDegree_lt (lt_of_not_ge H), IsNilpotent.zero]
+
+/-- Let `P` be a polynomial over `R`. If `P` is a unit, then all its coefficients are nilpotent,
+except its constant term which is a unit. -/
+theorem coeff_isUnit_isNilpotent_of_isUnit {P : Polynomial R} (hunit : IsUnit P) :
+    IsUnit (P.coeff 0) ∧ (∀ i, i ≠ 0 → IsNilpotent (P.coeff i)) := by
+  obtain ⟨Q, hQ⟩ := IsUnit.exists_right_inv hunit
+  constructor
+  . refine' isUnit_of_mul_eq_one _ (Q.coeff 0) _
+    have h := (mul_coeff_zero P Q).symm
+    rwa [hQ, coeff_one_zero] at h
+  . intros n hn
+    rw [nilpotent_iff_mem_prime]
+    intros I hI
+    let f := mapRingHom (Ideal.Quotient.mk I)
+    have hPQ : degree (f P) = 0 ∧ degree (f Q) = 0 := by
+      rw [← Nat.WithBot.add_eq_zero_iff, ← degree_mul, ← _root_.map_mul, hQ, map_one, degree_one]
+    have hcoeff : (f P).coeff n = 0 := by
+      refine' coeff_eq_zero_of_degree_lt _
+      rw [hPQ.1]
+      exact (@WithBot.coe_pos _ _ _ n).2 (Ne.bot_lt hn)
+    rw [coe_mapRingHom, coeff_map, ← RingHom.mem_ker, Ideal.mk_ker] at hcoeff
+    exact hcoeff
+
+/-- Let `P` be a polynomial over `R`. `P` is a unit if and only if all its coefficients are
+nilpotent, except its constant term which is a unit. -/
+theorem isUnit_iff_coeff_isUnit_isNilpotent (P : Polynomial R) :
+    IsUnit P ↔ IsUnit (P.coeff 0) ∧ (∀ i, i ≠ 0 → IsNilpotent (P.coeff i)) :=
+  ⟨coeff_isUnit_isNilpotent_of_isUnit, fun H => isUnit_of_coeff_isUnit_isNilpotent H.1 H.2⟩
+
 end CommRing
 
 end Polynomial