Skip to content

Commit c4190b4

Browse files
ocfnashocfnash
committed
feat: lemmas about nilpotency and polynomials (#6450)
1 parent 807aecc commit c4190b4

12 files changed

Lines changed: 307 additions & 72 deletions

File tree

‎Mathlib.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2034,6 +2034,7 @@ import Mathlib.GroupTheory.Submonoid.Inverses
20342034
import Mathlib.GroupTheory.Submonoid.Membership
20352035
import Mathlib.GroupTheory.Submonoid.Operations
20362036
import Mathlib.GroupTheory.Submonoid.Pointwise
2037+
import Mathlib.GroupTheory.Submonoid.ZeroDivisors
20372038
import Mathlib.GroupTheory.Subsemigroup.Basic
20382039
import Mathlib.GroupTheory.Subsemigroup.Center
20392040
import Mathlib.GroupTheory.Subsemigroup.Centralizer
@@ -2842,6 +2843,7 @@ import Mathlib.RingTheory.Polynomial.GaussLemma
28422843
import Mathlib.RingTheory.Polynomial.Hermite.Basic
28432844
import Mathlib.RingTheory.Polynomial.Hermite.Gaussian
28442845
import Mathlib.RingTheory.Polynomial.IntegralNormalization
2846+
import Mathlib.RingTheory.Polynomial.Nilpotent
28452847
import Mathlib.RingTheory.Polynomial.Opposites
28462848
import Mathlib.RingTheory.Polynomial.Pochhammer
28472849
import Mathlib.RingTheory.Polynomial.Quotient

‎Mathlib/Algebra/Regular/Basic.lean‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -70,6 +70,8 @@ structure IsRegular (c : R) : Prop where
7070
right : IsRightRegular c
7171
#align is_regular IsRegular
7272

73+
attribute [simp] IsRegular.left IsRegular.right
74+
7375
attribute [to_additive] IsRegular
7476

7577
@[to_additive]
@@ -266,6 +268,14 @@ theorem not_isRightRegular_zero [nR : Nontrivial R] : ¬IsRightRegular (0 : R) :
266268
theorem not_isRegular_zero [Nontrivial R] : ¬IsRegular (0 : R) := fun h => IsRegular.ne_zero h rfl
267269
#align not_is_regular_zero not_isRegular_zero
268270

271+
@[simp] lemma IsLeftRegular.mul_left_eq_zero_iff (hb : IsLeftRegular b) : b * a = 0 ↔ a = 0 := by
272+
nth_rw 1 [← mul_zero b]
273+
exact ⟨fun h ↦ hb h, fun ha ↦ by rw [ha, mul_zero]⟩
274+
275+
@[simp] lemma IsRightRegular.mul_right_eq_zero_iff (hb : IsRightRegular b) : a * b = 0 ↔ a = 0 := by
276+
nth_rw 1 [← zero_mul b]
277+
exact ⟨fun h ↦ hb h, fun ha ↦ by rw [ha, zero_mul]⟩
278+
269279
end MulZeroClass
270280

271281
section MulOneClass

‎Mathlib/Data/Nat/SuccPred.lean‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -72,6 +72,10 @@ instance : IsSuccArchimedean ℕ :=
7272
instance : IsPredArchimedean ℕ :=
7373
⟨fun {a} {b} h => ⟨b - a, by rw [pred_eq_pred, pred_iterate, tsub_tsub_cancel_of_le h]⟩⟩
7474

75+
lemma forall_ne_zero_iff (P : ℕ → Prop) :
76+
(∀ i, i ≠ 0 → P i) ↔ (∀ i, P (i + 1)) :=
77+
SuccOrder.forall_ne_bot_iff P
78+
7579
/-! ### Covering relation -/
7680

7781

‎Mathlib/Data/Polynomial/Basic.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -729,6 +729,9 @@ theorem coeff_C_zero : coeff (C a) 0 = a :=
729729
theorem coeff_C_ne_zero (h : n ≠ 0) : (C a).coeff n = 0 := by rw [coeff_C, if_neg h]
730730
#align polynomial.coeff_C_ne_zero Polynomial.coeff_C_ne_zero
731731

732+
@[simp]
733+
lemma coeff_C_succ {r : R} {n : ℕ} : coeff (C r) (n + 1) = 0 := by simp [coeff_C]
734+
732735
@[simp]
733736
theorem coeff_nat_cast_ite : (Nat.cast m : R[X]).coeff n = ite (n = 0) m 0 := by
734737
simp only [← C_eq_nat_cast, coeff_C, Nat.cast_ite, Nat.cast_zero]

‎Mathlib/Data/Polynomial/Coeff.lean‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
66
import Mathlib.Data.Polynomial.Basic
77
import Mathlib.Data.Finset.NatAntidiagonal
88
import Mathlib.Data.Nat.Choose.Sum
9+
import Mathlib.Algebra.Regular.Pow
910

1011
#align_import data.polynomial.coeff from "leanprover-community/mathlib"@"2651125b48fc5c170ab1111afd0817c903b1fc6c"
1112

@@ -179,12 +180,12 @@ theorem coeff_mul_C (p : R[X]) (n : ℕ) (a : R) : coeff (p * C a) n = coeff p n
179180
exact AddMonoidAlgebra.mul_single_zero_apply p a n
180181
#align polynomial.coeff_mul_C Polynomial.coeff_mul_C
181182

183+
@[simp]
182184
theorem coeff_X_pow (k n : ℕ) : coeff (X ^ k : R[X]) n = if n = k then 1 else 0 := by
183185
simp only [one_mul, RingHom.map_one, ← coeff_C_mul_X_pow]
184186
#align polynomial.coeff_X_pow Polynomial.coeff_X_pow
185187

186-
@[simp]
187-
theorem coeff_X_pow_self (n : ℕ) : coeff (X ^ n : R[X]) n = 1 := by simp [coeff_X_pow]
188+
theorem coeff_X_pow_self (n : ℕ) : coeff (X ^ n : R[X]) n = 1 := by simp
188189
#align polynomial.coeff_X_pow_self Polynomial.coeff_X_pow_self
189190

190191
section Fewnomials
@@ -293,16 +294,15 @@ theorem mul_X_pow_eq_zero {p : R[X]} {n : ℕ} (H : p * X ^ n = 0) : p = 0 :=
293294
ext fun k => (coeff_mul_X_pow p n k).symm.trans <| ext_iff.1 H (k + n)
294295
#align polynomial.mul_X_pow_eq_zero Polynomial.mul_X_pow_eq_zero
295296

296-
theorem mul_X_pow_injective (n : ℕ) : Function.Injective fun P : R[X] => X ^ n * P := by
297-
intro P Q hPQ
298-
simp only at hPQ
297+
@[simp] theorem isRegular_X : IsRegular (X : R[X]) := by
298+
suffices : IsLeftRegular (X : R[X])
299+
· exact ⟨this, this.right_of_commute commute_X⟩
300+
intro P Q (hPQ : X * P = X * Q)
299301
ext i
300-
rw [← coeff_X_pow_mul P n i, hPQ, coeff_X_pow_mul Q n i]
301-
#align polynomial.mul_X_pow_injective Polynomial.mul_X_pow_injective
302+
rw [← coeff_X_mul P i, hPQ, coeff_X_mul Q i]
302303

303-
theorem mul_X_injective : Function.Injective fun P : R[X] => X * P :=
304-
pow_one (X : R[X]) ▸ mul_X_pow_injective 1
305-
#align polynomial.mul_X_injective Polynomial.mul_X_injective
304+
-- TODO Unify this with `Polynomial.Monic.isRegular`
305+
theorem isRegular_X_pow (n : ℕ) : IsRegular (X ^ n : R[X]) := isRegular_X.pow n
306306

307307
theorem coeff_X_add_C_pow (r : R) (n k : ℕ) :
308308
((X + C r) ^ n).coeff k = r ^ (n - k) * (n.choose k : R) := by

‎Mathlib/Data/Polynomial/Laurent.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -605,7 +605,7 @@ theorem isLocalization : IsLocalization (Submonoid.closure ({X} : Set R[X])) R[T
605605
exact ⟨1, rfl⟩
606606
· rintro ⟨⟨h, hX⟩, h⟩
607607
rcases Submonoid.mem_closure_singleton.mp hX with ⟨n, rfl⟩
608-
exact mul_X_pow_injective n h }
608+
exact (isRegular_X_pow n).left h }
609609
#align laurent_polynomial.is_localization LaurentPolynomial.isLocalization
610610

611611
end CommSemiring

‎Mathlib/Data/Polynomial/Reverse.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -78,6 +78,8 @@ theorem revAt_le {N i : ℕ} (H : i ≤ N) : revAt N i = N - i :=
7878
if_pos H
7979
#align polynomial.rev_at_le Polynomial.revAt_le
8080

81+
lemma revAt_eq_self_of_lt {N i : ℕ} (h : N < i) : revAt N i = i := by simp [revAt, Nat.not_le.mpr h]
82+
8183
theorem revAt_add {N O n o : ℕ} (hn : n ≤ N) (ho : o ≤ O) :
8284
revAt (N + O) (n + o) = revAt N n + revAt O o := by
8385
rcases Nat.le.dest hn with ⟨n', rfl⟩

‎Mathlib/GroupTheory/Submonoid/ZeroDivisors.lean‎

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,65 @@
1+
/-
2+
Copyright (c) 2023 Oliver Nash. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Oliver Nash
5+
-/
6+
import Mathlib.GroupTheory.Submonoid.Basic
7+
8+
/-!
9+
# Zero divisors
10+
11+
## Main definitions
12+
13+
* `nonZeroDivisorsLeft`: the elements of a `MonoidWithZero` that are not left zero divisors.
14+
* `nonZeroDivisorsRight`: the elements of a `MonoidWithZero` that are not right zero divisors.
15+
16+
-/
17+
18+
section MonoidWithZero
19+
20+
variable (M₀ : Type _) [MonoidWithZero M₀]
21+
22+
/-- The collection of elements of a `MonoidWithZero` that are not left zero divisors form a
23+
`Submonoid`. -/
24+
def nonZeroDivisorsLeft : Submonoid M₀ where
25+
carrier := {x | ∀ y, y * x = 0 → y = 0}
26+
one_mem' := by simp
27+
mul_mem' {x} {y} hx hy := fun z hz ↦ hx _ <| hy _ (mul_assoc z x y ▸ hz)
28+
29+
@[simp] lemma mem_nonZeroDivisorsLeft_iff {x : M₀} :
30+
x ∈ nonZeroDivisorsLeft M₀ ↔ ∀ y, y * x = 0 → y = 0 :=
31+
Iff.rfl
32+
33+
/-- The collection of elements of a `MonoidWithZero` that are not right zero divisors form a
34+
`Submonoid`. -/
35+
def nonZeroDivisorsRight : Submonoid M₀ where
36+
carrier := {x | ∀ y, x * y = 0 → y = 0}
37+
one_mem' := by simp
38+
mul_mem' := fun {x} {y} hx hy z hz ↦ hy _ (hx _ ((mul_assoc x y z).symm ▸ hz))
39+
40+
@[simp] lemma mem_nonZeroDivisorsRight_iff {x : M₀} :
41+
x ∈ nonZeroDivisorsRight M₀ ↔ ∀ y, x * y = 0 → y = 0 :=
42+
Iff.rfl
43+
44+
lemma nonZeroDivisorsLeft_eq_right (M₀ : Type _) [CommMonoidWithZero M₀] :
45+
nonZeroDivisorsLeft M₀ = nonZeroDivisorsRight M₀ := by
46+
ext x; simp [mul_comm x]
47+
48+
@[simp] lemma coe_nonZeroDivisorsLeft_eq [NoZeroDivisors M₀] [Nontrivial M₀] :
49+
nonZeroDivisorsLeft M₀ = {x : M₀ | x ≠ 0} := by
50+
ext x
51+
simp only [SetLike.mem_coe, mem_nonZeroDivisorsLeft_iff, mul_eq_zero, forall_eq_or_imp, true_and,
52+
Set.mem_setOf_eq]
53+
refine' ⟨fun h ↦ _, fun hx y hx' ↦ by contradiction⟩
54+
contrapose! h
55+
exact ⟨1, h, one_ne_zero⟩
56+
57+
@[simp] lemma coe_nonZeroDivisorsRight_eq [NoZeroDivisors M₀] [Nontrivial M₀] :
58+
nonZeroDivisorsRight M₀ = {x : M₀ | x ≠ 0} := by
59+
ext x
60+
simp only [SetLike.mem_coe, mem_nonZeroDivisorsRight_iff, mul_eq_zero, Set.mem_setOf_eq]
61+
refine' ⟨fun h ↦ _, fun hx y hx' ↦ by aesop⟩
62+
contrapose! h
63+
exact ⟨1, Or.inl h, one_ne_zero⟩
64+
65+
end MonoidWithZero

‎Mathlib/Order/SuccPred/Basic.lean‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1511,3 +1511,14 @@ theorem Pred.rec_top (p : α → Prop) (htop : p ⊤) (hpred : ∀ a, p a → p
15111511
#align pred.rec_top Pred.rec_top
15121512

15131513
end OrderTop
1514+
1515+
lemma SuccOrder.forall_ne_bot_iff
1516+
[Nontrivial α] [PartialOrder α] [OrderBot α] [SuccOrder α] [IsSuccArchimedean α]
1517+
(P : α → Prop) :
1518+
(∀ i, i ≠ ⊥ → P i) ↔ (∀ i, P (SuccOrder.succ i)) := by
1519+
refine' ⟨fun h i ↦ h _ (Order.succ_ne_bot i), fun h i hi ↦ _⟩
1520+
obtain ⟨j, rfl⟩ := exists_succ_iterate_of_le (bot_le : ⊥ ≤ i)
1521+
have hj : 0 < j := by apply Nat.pos_of_ne_zero; contrapose! hi; simp [hi]
1522+
rw [← Nat.succ_pred_eq_of_pos hj]
1523+
simp only [Function.iterate_succ', Function.comp_apply]
1524+
apply h

‎Mathlib/RingTheory/Nilpotent.lean‎

Lines changed: 34 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ Authors: Oliver Nash
55
-/
66
import Mathlib.Data.Nat.Choose.Sum
77
import Mathlib.Algebra.Algebra.Bilinear
8+
import Mathlib.GroupTheory.Submonoid.ZeroDivisors
89
import Mathlib.RingTheory.Ideal.Operations
910
import Mathlib.Algebra.GeomSum
1011

@@ -43,7 +44,7 @@ theorem IsNilpotent.mk [Zero R] [Pow R ℕ] (x : R) (n : ℕ) (e : x ^ n = 0) :
4344
⟨n, e⟩
4445
#align is_nilpotent.mk IsNilpotent.mk
4546

46-
theorem IsNilpotent.zero [MonoidWithZero R] : IsNilpotent (0 : R) :=
47+
@[simp] theorem IsNilpotent.zero [MonoidWithZero R] : IsNilpotent (0 : R) :=
4748
⟨1, pow_one 0⟩
4849
#align is_nilpotent.zero IsNilpotent.zero
4950

@@ -172,17 +173,43 @@ theorem isNilpotent_add (hx : IsNilpotent x) (hy : IsNilpotent y) : IsNilpotent
172173
· rw [pow_eq_zero_of_le hj hm, MulZeroClass.mul_zero]
173174
#align commute.is_nilpotent_add Commute.isNilpotent_add
174175

176+
protected lemma isNilpotent_sum {ι : Type _} {s : Finset ι} {f : ι → R}
177+
(hnp : ∀ i ∈ s, IsNilpotent (f i)) (h_comm : ∀ i j, i ∈ s → j ∈ s → Commute (f i) (f j)) :
178+
IsNilpotent (∑ i in s, f i) := by
179+
classical
180+
induction' s using Finset.induction with j s hj ih; simp
181+
rw [Finset.sum_insert hj]
182+
apply Commute.isNilpotent_add
183+
· exact Commute.sum_right _ _ _ (fun i hi ↦ h_comm _ _ (by simp) (by simp [hi]))
184+
· apply hnp; simp
185+
· exact ih (fun i hi ↦ hnp i (by simp [hi]))
186+
(fun i j hi hj ↦ h_comm i j (by simp [hi]) (by simp [hj]))
187+
175188
theorem isNilpotent_mul_left (h : IsNilpotent x) : IsNilpotent (x * y) := by
176189
obtain ⟨n, hn⟩ := h
177190
use n
178191
rw [h_comm.mul_pow, hn, MulZeroClass.zero_mul]
179192
#align commute.is_nilpotent_mul_left Commute.isNilpotent_mul_left
180193

194+
protected lemma isNilpotent_mul_left_iff (hy : y ∈ nonZeroDivisorsLeft R) :
195+
IsNilpotent (x * y) ↔ IsNilpotent x := by
196+
refine' ⟨_, h_comm.isNilpotent_mul_left⟩
197+
rintro ⟨k, hk⟩
198+
rw [mul_pow h_comm] at hk
199+
exact ⟨k, (nonZeroDivisorsLeft R).pow_mem hy k _ hk⟩
200+
181201
theorem isNilpotent_mul_right (h : IsNilpotent y) : IsNilpotent (x * y) := by
182202
rw [h_comm.eq]
183203
exact h_comm.symm.isNilpotent_mul_left h
184204
#align commute.is_nilpotent_mul_right Commute.isNilpotent_mul_right
185205

206+
protected lemma isNilpotent_mul_right_iff (hx : x ∈ nonZeroDivisorsRight R) :
207+
IsNilpotent (x * y) ↔ IsNilpotent y := by
208+
refine' ⟨_, h_comm.isNilpotent_mul_right⟩
209+
rintro ⟨k, hk⟩
210+
rw [mul_pow h_comm] at hk
211+
exact ⟨k, (nonZeroDivisorsRight R).pow_mem hx k _ hk⟩
212+
186213
end Semiring
187214

188215
section Ring
@@ -202,7 +229,12 @@ end Commute
202229

203230
section CommSemiring
204231

205-
variable [CommSemiring R]
232+
variable [CommSemiring R] {x y : R}
233+
234+
lemma isNilpotent_sum {ι : Type _} {s : Finset ι} {f : ι → R}
235+
(hnp : ∀ i ∈ s, IsNilpotent (f i)) :
236+
IsNilpotent (∑ i in s, f i) :=
237+
Commute.isNilpotent_sum hnp fun _ _ _ _ ↦ Commute.all _ _
206238

207239
/-- The nilradical of a commutative semiring is the ideal of nilpotent elements. -/
208240
def nilradical (R : Type _) [CommSemiring R] : Ideal R :=

0 commit comments

Comments
 (0)