-
Notifications
You must be signed in to change notification settings - Fork 251
/
MixedCharZero.lean
384 lines (328 loc) · 15.6 KB
/
MixedCharZero.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
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
/-
Copyright (c) 2022 Jon Eugster. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jon Eugster
-/
import Mathlib.Algebra.CharP.LocalRing
import Mathlib.RingTheory.Ideal.Quotient
import Mathlib.Tactic.FieldSimp
#align_import algebra.char_p.mixed_char_zero from "leanprover-community/mathlib"@"70fd9563a21e7b963887c9360bd29b2393e6225a"
/-!
# Equal and mixed characteristic
In commutative algebra, some statements are simpler when working over a `ℚ`-algebra `R`, in which
case one also says that the ring has "equal characteristic zero". A ring that is not a
`ℚ`-algebra has either positive characteristic or there exists a prime ideal `I ⊂ R` such that
the quotient `R ⧸ I` has positive characteristic `p > 0`. In this case one speaks of
"mixed characteristic `(0, p)`", where `p` is only unique if `R` is local.
Examples of mixed characteristic rings are `ℤ` or the `p`-adic integers/numbers.
This file provides the main theorem `split_by_characteristic` that splits any proposition `P` into
the following three cases:
1) Positive characteristic: `CharP R p` (where `p ≠ 0`)
2) Equal characteristic zero: `Algebra ℚ R`
3) Mixed characteristic: `MixedCharZero R p` (where `p` is prime)
## Main definitions
- `MixedCharZero` : A ring has mixed characteristic `(0, p)` if it has characteristic zero
and there exists an ideal such that the quotient `R ⧸ I` has characteristic `p`.
## Main results
- `split_equalCharZero_mixedCharZero` : Split a statement into equal/mixed characteristic zero.
This main theorem has the following three corollaries which include the positive
characteristic case for convenience:
- `split_by_characteristic` : Generally consider positive char `p ≠ 0`.
- `split_by_characteristic_domain` : In a domain we can assume that `p` is prime.
- `split_by_characteristic_localRing` : In a local ring we can assume that `p` is a prime power.
## Implementation Notes
We use the terms `EqualCharZero` and `AlgebraRat` despite not being such definitions in mathlib.
The former refers to the statement `∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I)`, the latter
refers to the existence of an instance `[Algebra ℚ R]`. The two are shown to be
equivalent conditions.
## TODO
- Relate mixed characteristic in a local ring to p-adic numbers [NumberTheory.PAdics].
-/
variable (R : Type*) [CommRing R]
/-!
### Mixed characteristic
-/
/--
A ring of characteristic zero is of "mixed characteristic `(0, p)`" if there exists an ideal
such that the quotient `R ⧸ I` has characteristic `p`.
**Remark:** For `p = 0`, `MixedChar R 0` is a meaningless definition (i.e. satisfied by any ring)
as `R ⧸ ⊥ ≅ R` has by definition always characteristic zero.
One could require `(I ≠ ⊥)` in the definition, but then `MixedChar R 0` would mean something
like `ℤ`-algebra of extension degree `≥ 1` and would be completely independent from
whether something is a `ℚ`-algebra or not (e.g. `ℚ[X]` would satisfy it but `ℚ` wouldn't).
-/
class MixedCharZero (p : ℕ) : Prop where
[toCharZero : CharZero R]
charP_quotient : ∃ I : Ideal R, I ≠ ⊤ ∧ CharP (R ⧸ I) p
#align mixed_char_zero MixedCharZero
namespace MixedCharZero
/--
Reduction to `p` prime: When proving any statement `P` about mixed characteristic rings we
can always assume that `p` is prime.
-/
theorem reduce_to_p_prime {P : Prop} :
(∀ p > 0, MixedCharZero R p → P) ↔ ∀ p : ℕ, p.Prime → MixedCharZero R p → P := by
constructor
· intro h q q_prime q_mixedChar
exact h q (Nat.Prime.pos q_prime) q_mixedChar
· intro h q q_pos q_mixedChar
rcases q_mixedChar.charP_quotient with ⟨I, hI_ne_top, _⟩
-- Krull's Thm: There exists a prime ideal `P` such that `I ≤ P`
rcases Ideal.exists_le_maximal I hI_ne_top with ⟨M, hM_max, h_IM⟩
let r := ringChar (R ⧸ M)
have r_pos : r ≠ 0 := by
have q_zero :=
congr_arg (Ideal.Quotient.factor I M h_IM) (CharP.cast_eq_zero (R ⧸ I) q)
simp only [map_natCast, map_zero] at q_zero
apply ne_zero_of_dvd_ne_zero (ne_of_gt q_pos)
exact (CharP.cast_eq_zero_iff (R ⧸ M) r q).mp q_zero
have r_prime : Nat.Prime r :=
or_iff_not_imp_right.1 (CharP.char_is_prime_or_zero (R ⧸ M) r) r_pos
apply h r r_prime
have : CharZero R := q_mixedChar.toCharZero
exact ⟨⟨M, hM_max.ne_top, ringChar.of_eq rfl⟩⟩
#align mixed_char_zero.reduce_to_p_prime MixedCharZero.reduce_to_p_prime
/--
Reduction to `I` prime ideal: When proving statements about mixed characteristic rings,
after we reduced to `p` prime, we can assume that the ideal `I` in the definition is maximal.
-/
theorem reduce_to_maximal_ideal {p : ℕ} (hp : Nat.Prime p) :
(∃ I : Ideal R, I ≠ ⊤ ∧ CharP (R ⧸ I) p) ↔ ∃ I : Ideal R, I.IsMaximal ∧ CharP (R ⧸ I) p := by
constructor
· intro g
rcases g with ⟨I, ⟨hI_not_top, _⟩⟩
-- Krull's Thm: There exists a prime ideal `M` such that `I ≤ M`.
rcases Ideal.exists_le_maximal I hI_not_top with ⟨M, ⟨hM_max, hM_ge⟩⟩
use M
constructor
· exact hM_max
· cases CharP.exists (R ⧸ M) with
| intro r hr =>
-- Porting note: This is odd. Added `have hr := hr`.
-- Without this it seems that lean does not find `hr` as an instance.
have hr := hr
convert hr
have r_dvd_p : r ∣ p := by
rw [← CharP.cast_eq_zero_iff (R ⧸ M) r p]
convert congr_arg (Ideal.Quotient.factor I M hM_ge) (CharP.cast_eq_zero (R ⧸ I) p)
symm
apply (Nat.Prime.eq_one_or_self_of_dvd hp r r_dvd_p).resolve_left
exact CharP.char_ne_one (R ⧸ M) r
· intro ⟨I, hI_max, h_charP⟩
use I
exact ⟨Ideal.IsMaximal.ne_top hI_max, h_charP⟩
#align mixed_char_zero.reduce_to_maximal_ideal MixedCharZero.reduce_to_maximal_ideal
end MixedCharZero
/-!
### Equal characteristic zero
A commutative ring `R` has "equal characteristic zero" if it satisfies one of the following
equivalent properties:
1) `R` is a `ℚ`-algebra.
2) The quotient `R ⧸ I` has characteristic zero for any proper ideal `I ⊂ R`.
3) `R` has characteristic zero and does not have mixed characteristic for any prime `p`.
We show `(1) ↔ (2) ↔ (3)`, and most of the following is concerned with constructing
an explicit algebra map `ℚ →+* R` (given by `x ↦ (x.num : R) /ₚ ↑x.pnatDen`)
for the direction `(1) ← (2)`.
Note: Property `(2)` is denoted as `EqualCharZero` in the statement names below.
-/
namespace EqualCharZero
/-- `ℚ`-algebra implies equal characteristic. -/
theorem of_algebraRat [Algebra ℚ R] : ∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I) := by
intro I hI
constructor
intro a b h_ab
contrapose! hI
-- `↑a - ↑b` is a unit contained in `I`, which contradicts `I ≠ ⊤`.
refine' I.eq_top_of_isUnit_mem _ (IsUnit.map (algebraMap ℚ R) (IsUnit.mk0 (a - b : ℚ) _))
· simpa only [← Ideal.Quotient.eq_zero_iff_mem, map_sub, sub_eq_zero, map_natCast]
simpa only [Ne, sub_eq_zero] using (@Nat.cast_injective ℚ _ _).ne hI
set_option linter.uppercaseLean3 false in
#align Q_algebra_to_equal_char_zero EqualCharZero.of_algebraRat
section ConstructionAlgebraRat
variable {R}
/-- Internal: Not intended to be used outside this local construction. -/
theorem PNat.isUnit_natCast [h : Fact (∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I))]
(n : ℕ+) : IsUnit (n : R) := by
-- `n : R` is a unit iff `(n)` is not a proper ideal in `R`.
rw [← Ideal.span_singleton_eq_top]
-- So by contrapositive, we should show the quotient does not have characteristic zero.
apply not_imp_comm.mp (h.elim (Ideal.span {↑n}))
intro h_char_zero
-- In particular, the image of `n` in the quotient should be nonzero.
apply h_char_zero.cast_injective.ne n.ne_zero
-- But `n` generates the ideal, so its image is clearly zero.
rw [← map_natCast (Ideal.Quotient.mk _), Nat.cast_zero, Ideal.Quotient.eq_zero_iff_mem]
exact Ideal.subset_span (Set.mem_singleton _)
#align equal_char_zero.pnat_coe_is_unit EqualCharZero.PNat.isUnit_natCast
@[coe]
noncomputable def pnatCast [Fact (∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I))] : ℕ+ → Rˣ :=
fun n => (PNat.isUnit_natCast n).unit
/-- Internal: Not intended to be used outside this local construction. -/
noncomputable instance coePNatUnits
[Fact (∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I))] : Coe ℕ+ Rˣ :=
⟨EqualCharZero.pnatCast⟩
#align equal_char_zero.pnat_has_coe_units EqualCharZero.coePNatUnits
/-- Internal: Not intended to be used outside this local construction. -/
@[simp]
theorem pnatCast_one [Fact (∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I))] : ((1 : ℕ+) : Rˣ) = 1 := by
apply Units.ext
rw [Units.val_one]
change ((PNat.isUnit_natCast (R := R) 1).unit : R) = 1
rw [IsUnit.unit_spec (PNat.isUnit_natCast 1)]
rw [PNat.one_coe, Nat.cast_one]
#align equal_char_zero.pnat_coe_units_eq_one EqualCharZero.pnatCast_one
/-- Internal: Not intended to be used outside this local construction. -/
@[simp]
theorem pnatCast_eq_natCast [Fact (∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I))] (n : ℕ+) :
((n : Rˣ) : R) = ↑n := by
change ((PNat.isUnit_natCast (R := R) n).unit : R) = ↑n
simp only [IsUnit.unit_spec]
#align equal_char_zero.pnat_coe_units_coe_eq_coe EqualCharZero.pnatCast_eq_natCast
/-- Equal characteristic implies `ℚ`-algebra. -/
noncomputable def algebraRat (h : ∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I)) :
Algebra ℚ R :=
haveI : Fact (∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I)) := ⟨h⟩
RingHom.toAlgebra
{ toFun := fun x => x.num /ₚ ↑x.pnatDen
map_zero' := by simp [divp]
map_one' := by simp
map_mul' := by
intro a b
field_simp
trans (↑((a * b).num * a.den * b.den) : R)
· simp_rw [Int.cast_mul, Int.cast_ofNat]
ring
rw [Rat.mul_num_den' a b]
simp
map_add' := by
intro a b
field_simp
trans (↑((a + b).num * a.den * b.den) : R)
· simp_rw [Int.cast_mul, Int.cast_ofNat]
ring
rw [Rat.add_num_den' a b]
simp }
set_option linter.uppercaseLean3 false in
#align equal_char_zero_to_Q_algebra EqualCharZero.algebraRat
end ConstructionAlgebraRat
/-- Not mixed characteristic implies equal characteristic. -/
theorem of_not_mixedCharZero [CharZero R] (h : ∀ p > 0, ¬MixedCharZero R p) :
∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I) := by
intro I hI_ne_top
suffices CharP (R ⧸ I) 0 from CharP.charP_to_charZero _
cases CharP.exists (R ⧸ I) with
| intro p hp =>
cases p with
| zero => exact hp
| succ p =>
have h_mixed : MixedCharZero R p.succ := ⟨⟨I, ⟨hI_ne_top, hp⟩⟩⟩
exact absurd h_mixed (h p.succ p.succ_pos)
#align not_mixed_char_to_equal_char_zero EqualCharZero.of_not_mixedCharZero
/-- Equal characteristic implies not mixed characteristic. -/
theorem to_not_mixedCharZero (h : ∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I)) :
∀ p > 0, ¬MixedCharZero R p := by
intro p p_pos
by_contra hp_mixedChar
rcases hp_mixedChar.charP_quotient with ⟨I, hI_ne_top, hI_p⟩
replace hI_zero : CharP (R ⧸ I) 0 := @CharP.ofCharZero _ _ (h I hI_ne_top)
exact absurd (CharP.eq (R ⧸ I) hI_p hI_zero) (ne_of_gt p_pos)
#align equal_char_zero_to_not_mixed_char EqualCharZero.to_not_mixedCharZero
/--
A ring of characteristic zero has equal characteristic iff it does not
have mixed characteristic for any `p`.
-/
theorem iff_not_mixedCharZero [CharZero R] :
(∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I)) ↔ ∀ p > 0, ¬MixedCharZero R p :=
⟨to_not_mixedCharZero R, of_not_mixedCharZero R⟩
#align equal_char_zero_iff_not_mixed_char EqualCharZero.iff_not_mixedCharZero
/-- A ring is a `ℚ`-algebra iff it has equal characteristic zero. -/
theorem nonempty_algebraRat_iff :
Nonempty (Algebra ℚ R) ↔ ∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I) := by
constructor
· intro h_alg
haveI h_alg' : Algebra ℚ R := h_alg.some
apply of_algebraRat
· intro h
apply Nonempty.intro
exact algebraRat h
set_option linter.uppercaseLean3 false in
#align Q_algebra_iff_equal_char_zero EqualCharZero.nonempty_algebraRat_iff
end EqualCharZero
/--
A ring of characteristic zero is not a `ℚ`-algebra iff it has mixed characteristic for some `p`.
-/
theorem isEmpty_algebraRat_iff_mixedCharZero [CharZero R] :
IsEmpty (Algebra ℚ R) ↔ ∃ p > 0, MixedCharZero R p := by
rw [← not_iff_not]
push_neg
rw [not_isEmpty_iff, ← EqualCharZero.iff_not_mixedCharZero]
apply EqualCharZero.nonempty_algebraRat_iff
set_option linter.uppercaseLean3 false in
#align not_Q_algebra_iff_not_equal_char_zero isEmpty_algebraRat_iff_mixedCharZero
/-!
# Splitting statements into different characteristic
Statements to split a proof by characteristic. There are 3 theorems here that are very
similar. They only differ in the assumptions we can make on the positive characteristic
case:
Generally we need to consider all `p ≠ 0`, but if `R` is a local ring, we can assume
that `p` is a prime power. And if `R` is a domain, we can even assume that `p` is prime.
-/
section MainStatements
variable {P : Prop}
/-- Split a `Prop` in characteristic zero into equal and mixed characteristic. -/
theorem split_equalCharZero_mixedCharZero [CharZero R] (h_equal : Algebra ℚ R → P)
(h_mixed : ∀ p : ℕ, Nat.Prime p → MixedCharZero R p → P) : P := by
by_cases h : ∃ p > 0, MixedCharZero R p
· rcases h with ⟨p, ⟨H, hp⟩⟩
rw [← MixedCharZero.reduce_to_p_prime] at h_mixed
exact h_mixed p H hp
· apply h_equal
rw [← isEmpty_algebraRat_iff_mixedCharZero, not_isEmpty_iff] at h
exact h.some
#align split_equal_mixed_char split_equalCharZero_mixedCharZero
example (n : ℕ) (h : n ≠ 0) : 0 < n :=
zero_lt_iff.mpr h
/--
Split any `Prop` over `R` into the three cases:
- positive characteristic.
- equal characteristic zero.
- mixed characteristic `(0, p)`.
-/
theorem split_by_characteristic (h_pos : ∀ p : ℕ, p ≠ 0 → CharP R p → P) (h_equal : Algebra ℚ R → P)
(h_mixed : ∀ p : ℕ, Nat.Prime p → MixedCharZero R p → P) : P := by
cases CharP.exists R with
| intro p p_charP =>
by_cases h : p = 0
· rw [h] at p_charP
haveI h0 : CharZero R := CharP.charP_to_charZero R
exact split_equalCharZero_mixedCharZero R h_equal h_mixed
· exact h_pos p h p_charP
#align split_by_characteristic split_by_characteristic
/--
In an `IsDomain R`, split any `Prop` over `R` into the three cases:
- *prime* characteristic.
- equal characteristic zero.
- mixed characteristic `(0, p)`.
-/
theorem split_by_characteristic_domain [IsDomain R] (h_pos : ∀ p : ℕ, Nat.Prime p → CharP R p → P)
(h_equal : Algebra ℚ R → P) (h_mixed : ∀ p : ℕ, Nat.Prime p → MixedCharZero R p → P) : P := by
refine split_by_characteristic R ?_ h_equal h_mixed
intro p p_pos p_char
have p_prime : Nat.Prime p := or_iff_not_imp_right.mp (CharP.char_is_prime_or_zero R p) p_pos
exact h_pos p p_prime p_char
#align split_by_characteristic_domain split_by_characteristic_domain
/--
In a `LocalRing R`, split any `Prop` over `R` into the three cases:
- *prime power* characteristic.
- equal characteristic zero.
- mixed characteristic `(0, p)`.
-/
theorem split_by_characteristic_localRing [LocalRing R]
(h_pos : ∀ p : ℕ, IsPrimePow p → CharP R p → P) (h_equal : Algebra ℚ R → P)
(h_mixed : ∀ p : ℕ, Nat.Prime p → MixedCharZero R p → P) : P := by
refine' split_by_characteristic R _ h_equal h_mixed
intro p p_pos p_char
have p_ppow : IsPrimePow (p : ℕ) := or_iff_not_imp_left.mp (charP_zero_or_prime_power R p) p_pos
exact h_pos p p_ppow p_char
#align split_by_characteristic_local_ring split_by_characteristic_localRing
end MainStatements