-
Notifications
You must be signed in to change notification settings - Fork 259
/
Basic.lean
157 lines (117 loc) · 6.82 KB
/
Basic.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
/-
Copyright (c) 2020 Kenji Nakagawa. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kenji Nakagawa, Anne Baanen, Filippo A. E. Nuccio
-/
import Mathlib.RingTheory.Ideal.Over
import Mathlib.RingTheory.Polynomial.RationalRoot
/-!
# Dedekind rings and domains
This file defines the notion of a Dedekind ring (domain),
as a Noetherian integrally closed commutative ring (domain) of Krull dimension at most one.
## Main definitions
- `IsDedekindRing` defines a Dedekind ring as a commutative ring that is
Noetherian, integrally closed in its field of fractions and has Krull dimension at most one.
`isDedekindRing_iff` shows that this does not depend on the choice of field of fractions.
- `IsDedekindDomain` defines a Dedekind domain as a Dedekind ring that is a domain.
## Implementation notes
The definitions that involve a field of fractions choose a canonical field of fractions,
but are independent of that choice. The `..._iff` lemmas express this independence.
`IsDedekindRing` and `IsDedekindDomain` form a cycle in the typeclass hierarchy:
`IsDedekindRing R + IsDomain R` imply `IsDedekindDomain R`, which implies `IsDedekindRing R`.
This should be safe since the start and end point is the literal same expression,
which the tabled typeclass synthesis algorithm can deal with.
Often, definitions assume that Dedekind rings are not fields. We found it more practical
to add a `(h : ¬ IsField A)` assumption whenever this is explicitly needed.
## References
* [D. Marcus, *Number Fields*][marcus1977number]
* [J.W.S. Cassels, A. Frölich, *Algebraic Number Theory*][cassels1967algebraic]
* [J. Neukirch, *Algebraic Number Theory*][Neukirch1992]
## Tags
dedekind domain, dedekind ring
-/
variable (R A K : Type*) [CommRing R] [CommRing A] [Field K]
open scoped nonZeroDivisors Polynomial
/-- A ring `R` has Krull dimension at most one if all nonzero prime ideals are maximal. -/
class Ring.DimensionLEOne : Prop :=
(maximalOfPrime : ∀ {p : Ideal R}, p ≠ ⊥ → p.IsPrime → p.IsMaximal)
open Ideal Ring
theorem Ideal.IsPrime.isMaximal {R : Type*} [CommRing R] [DimensionLEOne R]
{p : Ideal R} (h : p.IsPrime) (hp : p ≠ ⊥) : p.IsMaximal :=
DimensionLEOne.maximalOfPrime hp h
namespace Ring
instance DimensionLEOne.principal_ideal_ring [IsDomain A] [IsPrincipalIdealRing A] :
DimensionLEOne A where
maximalOfPrime := fun nonzero _ =>
IsPrime.to_maximal_ideal nonzero
theorem DimensionLEOne.isIntegralClosure (B : Type*) [CommRing B] [IsDomain B] [Nontrivial R]
[Algebra R A] [Algebra R B] [Algebra B A] [IsScalarTower R B A] [IsIntegralClosure B R A]
[DimensionLEOne R] : DimensionLEOne B where
maximalOfPrime := fun {p} ne_bot _ =>
IsIntegralClosure.isMaximal_of_isMaximal_comap (R := R) A p
(Ideal.IsPrime.isMaximal inferInstance (IsIntegralClosure.comap_ne_bot A ne_bot))
nonrec instance DimensionLEOne.integralClosure [Nontrivial R] [IsDomain A] [Algebra R A]
[DimensionLEOne R] : DimensionLEOne (integralClosure R A) :=
DimensionLEOne.isIntegralClosure R A (integralClosure R A)
variable {R}
theorem DimensionLEOne.not_lt_lt [Ring.DimensionLEOne R] (p₀ p₁ p₂ : Ideal R) [hp₁ : p₁.IsPrime]
[hp₂ : p₂.IsPrime] : ¬(p₀ < p₁ ∧ p₁ < p₂)
| ⟨h01, h12⟩ => h12.ne ((hp₁.isMaximal (bot_le.trans_lt h01).ne').eq_of_le hp₂.ne_top h12.le)
theorem DimensionLEOne.eq_bot_of_lt [Ring.DimensionLEOne R] (p P : Ideal R) [p.IsPrime]
[P.IsPrime] (hpP : p < P) : p = ⊥ :=
by_contra fun hp0 => not_lt_lt ⊥ p P ⟨Ne.bot_lt hp0, hpP⟩
end Ring
/-- A Dedekind ring is a commutative ring that is Noetherian, integrally closed, and
has Krull dimension at most one.
This is exactly `IsDedekindDomain` minus the `IsDomain` hypothesis.
The integral closure condition is independent of the choice of field of fractions:
use `isDedekindRing_iff` to prove `IsDedekindRing` for a given `fraction_map`.
-/
class IsDedekindRing
extends IsNoetherian A A, DimensionLEOne A, IsIntegralClosure A A (FractionRing A) : Prop
/-- An integral domain is a Dedekind domain if and only if it is
Noetherian, has dimension ≤ 1, and is integrally closed in a given fraction field.
In particular, this definition does not depend on the choice of this fraction field. -/
theorem isDedekindRing_iff (K : Type*) [CommRing K] [Algebra A K] [IsFractionRing A K] :
IsDedekindRing A ↔
IsNoetherianRing A ∧ DimensionLEOne A ∧
∀ {x : K}, IsIntegral A x → ∃ y, algebraMap A K y = x :=
⟨fun _ => ⟨inferInstance, inferInstance,
fun {_} => (isIntegrallyClosed_iff K).mp inferInstance⟩,
fun ⟨hr, hd, hi⟩ => { hr, hd, (isIntegrallyClosed_iff K).mpr @hi with }⟩
/-- A Dedekind domain is an integral domain that is Noetherian, integrally closed, and
has Krull dimension at most one.
This is definition 3.2 of [Neukirch1992].
This is exactly `IsDedekindRing` plus the `IsDomain` hypothesis.
The integral closure condition is independent of the choice of field of fractions:
use `isDedekindDomain_iff` to prove `IsDedekindDomain` for a given `fraction_map`.
This is the default implementation, but there are equivalent definitions,
`is_dedekind_domain_dvr` and `is_dedekind_domain_inv`.
TODO: Prove that these are actually equivalent definitions.
-/
class IsDedekindDomain
extends IsDomain A, IsDedekindRing A : Prop
attribute [instance 90] IsDedekindDomain.toIsDomain
/-- Make a Dedekind domain from a Dedekind ring given that it is a domain.
`IsDedekindRing` and `IsDedekindDomain` form a cycle in the typeclass hierarchy:
`IsDedekindRing R + IsDomain R` imply `IsDedekindDomain R`, which implies `IsDedekindRing R`.
This should be safe since the start and end point is the literal same expression,
which the tabled typeclass synthesis algorithm can deal with.
-/
instance [IsDomain A] [IsDedekindRing A] : IsDedekindDomain A where
/-- An integral domain is a Dedekind domain iff and only if it is
Noetherian, has dimension ≤ 1, and is integrally closed in a given fraction field.
In particular, this definition does not depend on the choice of this fraction field. -/
theorem isDedekindDomain_iff (K : Type*) [Field K] [Algebra A K] [IsFractionRing A K] :
IsDedekindDomain A ↔
IsDomain A ∧ IsNoetherianRing A ∧ DimensionLEOne A ∧
∀ {x : K}, IsIntegral A x → ∃ y, algebraMap A K y = x :=
⟨fun _ => ⟨inferInstance, inferInstance, inferInstance,
fun {_} => (isIntegrallyClosed_iff K).mp inferInstance⟩,
fun ⟨hid, hr, hd, hi⟩ => { hid, hr, hd, (isIntegrallyClosed_iff K).mpr @hi with }⟩
-- See library note [lower instance priority]
instance (priority := 100) IsPrincipalIdealRing.isDedekindDomain
[IsDomain A] [IsPrincipalIdealRing A] :
IsDedekindDomain A :=
{ PrincipalIdealRing.isNoetherianRing, Ring.DimensionLEOne.principal_ideal_ring A,
UniqueFactorizationMonoid.instIsIntegrallyClosed with }