-
Notifications
You must be signed in to change notification settings - Fork 298
/
nilpotent.lean
233 lines (178 loc) · 7.11 KB
/
nilpotent.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
/-
Copyright (c) 2021 Oliver Nash. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Oliver Nash
-/
import data.nat.choose.sum
import algebra.algebra.bilinear
import ring_theory.ideal.operations
/-!
# Nilpotent elements
## Main definitions
* `is_nilpotent`
* `is_nilpotent_neg_iff`
* `commute.is_nilpotent_add`
* `commute.is_nilpotent_mul_left`
* `commute.is_nilpotent_mul_right`
* `commute.is_nilpotent_sub`
-/
universes u v
variables {R S : Type u} {x y : R}
/-- An element is said to be nilpotent if some natural-number-power of it equals zero.
Note that we require only the bare minimum assumptions for the definition to make sense. Even
`monoid_with_zero` is too strong since nilpotency is important in the study of rings that are only
power-associative. -/
def is_nilpotent [has_zero R] [has_pow R ℕ] (x : R) : Prop := ∃ (n : ℕ), x^n = 0
lemma is_nilpotent.mk [has_zero R] [has_pow R ℕ] (x : R) (n : ℕ)
(e : x ^ n = 0) : is_nilpotent x := ⟨n, e⟩
lemma is_nilpotent.zero [monoid_with_zero R] : is_nilpotent (0 : R) := ⟨1, pow_one 0⟩
lemma is_nilpotent.neg [ring R] (h : is_nilpotent x) : is_nilpotent (-x) :=
begin
obtain ⟨n, hn⟩ := h,
use n,
rw [neg_pow, hn, mul_zero],
end
@[simp] lemma is_nilpotent_neg_iff [ring R] : is_nilpotent (-x) ↔ is_nilpotent x :=
⟨λ h, neg_neg x ▸ h.neg, λ h, h.neg⟩
lemma is_nilpotent.map [monoid_with_zero R] [monoid_with_zero S] {r : R}
{F : Type*} [monoid_with_zero_hom_class F R S] (hr : is_nilpotent r) (f : F) :
is_nilpotent (f r) :=
by { use hr.some, rw [← map_pow, hr.some_spec, map_zero] }
/-- A structure that has zero and pow is reduced if it has no nonzero nilpotent elements. -/
class is_reduced (R : Type*) [has_zero R] [has_pow R ℕ] : Prop :=
(eq_zero : ∀ (x : R), is_nilpotent x → x = 0)
@[priority 900]
instance is_reduced_of_no_zero_divisors [monoid_with_zero R] [no_zero_divisors R] : is_reduced R :=
⟨λ _ ⟨_, hn⟩, pow_eq_zero hn⟩
@[priority 900]
instance is_reduced_of_subsingleton [has_zero R] [has_pow R ℕ] [subsingleton R] :
is_reduced R := ⟨λ _ _, subsingleton.elim _ _⟩
lemma is_nilpotent.eq_zero [has_zero R] [has_pow R ℕ] [is_reduced R]
(h : is_nilpotent x) : x = 0 :=
is_reduced.eq_zero x h
@[simp] lemma is_nilpotent_iff_eq_zero [monoid_with_zero R] [is_reduced R] :
is_nilpotent x ↔ x = 0 :=
⟨λ h, h.eq_zero, λ h, h.symm ▸ is_nilpotent.zero⟩
lemma is_reduced_of_injective [monoid_with_zero R] [monoid_with_zero S]
{F : Type*} [monoid_with_zero_hom_class F R S] (f : F)
(hf : function.injective f) [_root_.is_reduced S] : _root_.is_reduced R :=
begin
constructor,
intros x hx,
apply hf,
rw map_zero,
exact (hx.map f).eq_zero,
end
namespace commute
section semiring
variables [semiring R] (h_comm : commute x y)
include h_comm
lemma is_nilpotent_add (hx : is_nilpotent x) (hy : is_nilpotent y) : is_nilpotent (x + y) :=
begin
obtain ⟨n, hn⟩ := hx,
obtain ⟨m, hm⟩ := hy,
use n + m - 1,
rw h_comm.add_pow',
apply finset.sum_eq_zero,
rintros ⟨i, j⟩ hij,
suffices : x^i * y^j = 0, { simp only [this, nsmul_eq_mul, mul_zero], },
cases nat.le_or_le_of_add_eq_add_pred (finset.nat.mem_antidiagonal.mp hij) with hi hj,
{ rw [pow_eq_zero_of_le hi hn, zero_mul], },
{ rw [pow_eq_zero_of_le hj hm, mul_zero], },
end
lemma is_nilpotent_mul_left (h : is_nilpotent x) : is_nilpotent (x * y) :=
begin
obtain ⟨n, hn⟩ := h,
use n,
rw [h_comm.mul_pow, hn, zero_mul],
end
lemma is_nilpotent_mul_right (h : is_nilpotent y) : is_nilpotent (x * y) :=
by { rw h_comm.eq, exact h_comm.symm.is_nilpotent_mul_left h, }
end semiring
section ring
variables [ring R] (h_comm : commute x y)
include h_comm
lemma is_nilpotent_sub (hx : is_nilpotent x) (hy : is_nilpotent y) : is_nilpotent (x - y) :=
begin
rw ← neg_right_iff at h_comm,
rw ← is_nilpotent_neg_iff at hy,
rw sub_eq_add_neg,
exact h_comm.is_nilpotent_add hx hy,
end
end ring
end commute
section comm_semiring
variable [comm_semiring R]
/-- The nilradical of a commutative semiring is the ideal of nilpotent elements. -/
def nilradical (R : Type*) [comm_semiring R] : ideal R := (0 : ideal R).radical
lemma mem_nilradical : x ∈ nilradical R ↔ is_nilpotent x := iff.rfl
lemma nilradical_eq_Inf (R : Type*) [comm_semiring R] :
nilradical R = Inf { J : ideal R | J.is_prime } :=
(ideal.radical_eq_Inf ⊥).trans $ by simp_rw and_iff_right bot_le
lemma nilpotent_iff_mem_prime : is_nilpotent x ↔ ∀ (J : ideal R), J.is_prime → x ∈ J :=
by { rw [← mem_nilradical, nilradical_eq_Inf, submodule.mem_Inf], refl }
lemma nilradical_le_prime (J : ideal R) [H : J.is_prime] : nilradical R ≤ J :=
(nilradical_eq_Inf R).symm ▸ Inf_le H
@[simp] lemma nilradical_eq_zero (R : Type*) [comm_semiring R] [is_reduced R] : nilradical R = 0 :=
ideal.ext $ λ _, is_nilpotent_iff_eq_zero
end comm_semiring
namespace algebra
variables (R) {A : Type v} [comm_semiring R] [semiring A] [algebra R A]
@[simp] lemma is_nilpotent_lmul_left_iff (a : A) :
is_nilpotent (lmul_left R a) ↔ is_nilpotent a :=
begin
split; rintros ⟨n, hn⟩; use n;
simp only [lmul_left_eq_zero_iff, pow_lmul_left] at ⊢ hn;
exact hn,
end
@[simp] lemma is_nilpotent_lmul_right_iff (a : A) :
is_nilpotent (lmul_right R a) ↔ is_nilpotent a :=
begin
split; rintros ⟨n, hn⟩; use n;
simp only [lmul_right_eq_zero_iff, pow_lmul_right] at ⊢ hn;
exact hn,
end
end algebra
namespace module.End
variables {M : Type v} [ring R] [add_comm_group M] [module R M]
variables {f : module.End R M} {p : submodule R M} (hp : p ≤ p.comap f)
lemma is_nilpotent.mapq (hnp : is_nilpotent f) : is_nilpotent (p.mapq p f hp) :=
begin
obtain ⟨k, hk⟩ := hnp,
use k,
simp [← p.mapq_pow, hk],
end
end module.End
namespace ideal
variables [comm_semiring R] [comm_ring S] [algebra R S] (I : ideal S)
/-- Let `P` be a property on ideals. If `P` holds for square-zero ideals, and if
`P I → P (J ⧸ I) → P J`, then `P` holds for all nilpotent ideals. -/
lemma is_nilpotent.induction_on
(hI : is_nilpotent I)
{P : ∀ ⦃S : Type*⦄ [comm_ring S], by exactI ∀ I : ideal S, Prop}
(h₁ : ∀ ⦃S : Type*⦄ [comm_ring S], by exactI ∀ I : ideal S, I ^ 2 = ⊥ → P I)
(h₂ : ∀ ⦃S : Type*⦄ [comm_ring S], by exactI
∀ I J : ideal S, I ≤ J → P I → P (J.map (ideal.quotient.mk I)) → P J) : P I :=
begin
obtain ⟨n, hI : I ^ n = ⊥⟩ := hI,
unfreezingI { revert S },
apply nat.strong_induction_on n,
clear n,
introsI n H S _ I hI,
by_cases hI' : I = ⊥,
{ subst hI', apply h₁, rw [← ideal.zero_eq_bot, zero_pow], exact zero_lt_two },
cases n,
{ rw [pow_zero, ideal.one_eq_top] at hI,
haveI := subsingleton_of_bot_eq_top hI.symm,
exact (hI' (subsingleton.elim _ _)).elim },
cases n,
{ rw [pow_one] at hI,
exact (hI' hI).elim },
apply h₂ (I ^ 2) _ (ideal.pow_le_self two_ne_zero),
{ apply H n.succ _ (I ^ 2),
{ rw [← pow_mul, eq_bot_iff, ← hI, nat.succ_eq_add_one, nat.succ_eq_add_one],
exact ideal.pow_le_pow (by linarith) },
{ exact le_refl n.succ.succ } },
{ apply h₁, rw [← ideal.map_pow, ideal.map_quotient_self] },
end
end ideal