-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathnumber_field.lean
144 lines (105 loc) · 5.2 KB
/
number_field.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
/-
Copyright (c) 2021 Ashvni Narayanan. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Ashvni Narayanan, Anne Baanen
-/
import algebra.field.basic
import data.rat.basic
import ring_theory.algebraic
import ring_theory.dedekind_domain.integral_closure
import ring_theory.integral_closure
import ring_theory.polynomial.rational_root
/-!
# Number fields
This file defines a number field and the ring of integers corresponding to it.
## Main definitions
- `number_field` defines a number field as a field which has characteristic zero and is finite
dimensional over ℚ.
- `ring_of_integers` defines the ring of integers (or number ring) corresponding to a number field
as the integral closure of ℤ in the number field.
## Implementation notes
The definitions that involve a field of fractions choose a canonical field of fractions,
but are independent of that choice.
## References
* [D. Marcus, *Number Fields*][marcus1977number]
* [J.W.S. Cassels, A. Frölich, *Algebraic Number Theory*][cassels1967algebraic]
* [P. Samuel, *Algebraic Theory of Numbers*][samuel1970algebraic]
## Tags
number field, ring of integers
-/
/-- A number field is a field which has characteristic zero and is finite
dimensional over ℚ. -/
class number_field (K : Type*) [field K] : Prop :=
[to_char_zero : char_zero K]
[to_finite_dimensional : finite_dimensional ℚ K]
open function
open_locale classical big_operators
/-- `ℤ` with its usual ring structure is not a field. -/
lemma int.not_is_field : ¬ is_field ℤ :=
λ h, int.not_even_one $ (h.mul_inv_cancel two_ne_zero).imp $ λ a, (by rw ← two_mul; exact eq.symm)
namespace number_field
variables (K L : Type*) [field K] [field L] [nf : number_field K]
include nf
-- See note [lower instance priority]
attribute [priority 100, instance] number_field.to_char_zero number_field.to_finite_dimensional
protected lemma is_algebraic : algebra.is_algebraic ℚ K := algebra.is_algebraic_of_finite _ _
omit nf
/-- The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field. -/
def ring_of_integers := integral_closure ℤ K
localized "notation `𝓞` := number_field.ring_of_integers" in number_field
lemma mem_ring_of_integers (x : K) : x ∈ 𝓞 K ↔ is_integral ℤ x := iff.rfl
/-- Given an algebra between two fields, create an algebra between their two rings of integers.
For now, this is not an instance by default as it creates an equal-but-not-defeq diamond with
`algebra.id` when `K = L`. This is caused by `x = ⟨x, x.prop⟩` not being defeq on subtypes. This
will likely change in Lean 4. -/
def ring_of_integers_algebra [algebra K L] : algebra (𝓞 K) (𝓞 L) := ring_hom.to_algebra
{ to_fun := λ k, ⟨algebra_map K L k, is_integral.algebra_map k.2⟩,
map_zero' := subtype.ext $ by simp only [subtype.coe_mk, subalgebra.coe_zero, map_zero],
map_one' := subtype.ext $ by simp only [subtype.coe_mk, subalgebra.coe_one, map_one],
map_add' := λ x y, subtype.ext $ by simp only [map_add, subalgebra.coe_add, subtype.coe_mk],
map_mul' := λ x y, subtype.ext $ by simp only [subalgebra.coe_mul, map_mul, subtype.coe_mk] }
namespace ring_of_integers
variables {K}
instance [number_field K] : is_fraction_ring (𝓞 K) K :=
integral_closure.is_fraction_ring_of_finite_extension ℚ _
instance : is_integral_closure (𝓞 K) ℤ K :=
integral_closure.is_integral_closure _ _
instance [number_field K] : is_integrally_closed (𝓞 K) :=
integral_closure.is_integrally_closed_of_finite_extension ℚ
lemma is_integral_coe (x : 𝓞 K) : is_integral ℤ (x : K) :=
x.2
/-- The ring of integers of `K` are equivalent to any integral closure of `ℤ` in `K` -/
protected noncomputable def equiv (R : Type*) [comm_ring R] [algebra R K]
[is_integral_closure R ℤ K] : 𝓞 K ≃+* R :=
(is_integral_closure.equiv ℤ R K _).symm.to_ring_equiv
variables (K)
instance [number_field K] : char_zero (𝓞 K) := char_zero.of_module _ K
/-- The ring of integers of a number field is not a field. -/
lemma not_is_field [number_field K] : ¬ is_field (𝓞 K) :=
begin
have h_inj : function.injective ⇑(algebra_map ℤ (𝓞 K)),
{ exact ring_hom.injective_int (algebra_map ℤ (𝓞 K)) },
intro hf,
exact int.not_is_field ((is_integral.is_field_iff_is_field
(is_integral_closure.is_integral_algebra ℤ K) h_inj).mpr hf)
end
instance [number_field K] : is_dedekind_domain (𝓞 K) :=
is_integral_closure.is_dedekind_domain ℤ ℚ K _
end ring_of_integers
end number_field
namespace rat
open number_field
local attribute [instance] subsingleton_rat_module
instance rat.number_field : number_field ℚ :=
{ to_char_zero := infer_instance,
to_finite_dimensional :=
-- The vector space structure of `ℚ` over itself can arise in multiple ways:
-- all fields are vector spaces over themselves (used in `rat.finite_dimensional`)
-- all char 0 fields have a canonical embedding of `ℚ` (used in `number_field`).
-- Show that these coincide:
by convert (infer_instance : finite_dimensional ℚ ℚ), }
/-- The ring of integers of `ℚ` as a number field is just `ℤ`. -/
noncomputable def ring_of_integers_equiv : ring_of_integers ℚ ≃+* ℤ :=
ring_of_integers.equiv ℤ
end rat