refactor(number_theory): reorganize number field results into new sub…

…folder (#16764)

- Create a new dir `number_field` in `number_theory`
- Move the current file `number_field.lean` to `number_theory/number_field/basic.lean`
- Move the results about embeddings from this file to a new file `number_theory/number_field/embeddings.lean`
- Move the file `number_theory/class_number/number_field.lean` to `number_theory/number_field/class_number.lean`

src/number_theory/cyclotomic/basic.lean

@@ -5,7 +5,7 @@ Authors: Riccardo Brasca
 -/
 
 import ring_theory.polynomial.cyclotomic.basic
-import number_theory.number_field
+import number_theory.number_field.basic
 import algebra.char_p.algebra
 import field_theory.galois
 

src/number_theory/number_field/basic.lean

@@ -0,0 +1,167 @@
+/-
+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 ring_theory.dedekind_domain.integral_closure
+import algebra.char_p.algebra
+
+/-!
+# 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 (name := ring_of_integers)
+  `𝓞` := number_field.ring_of_integers" in number_field
+
+lemma mem_ring_of_integers (x : K) : x ∈ 𝓞 K ↔ is_integral ℤ x := iff.rfl
+
+lemma is_integral_of_mem_ring_of_integers {K : Type*} [field K] {x : K} (hx : x ∈ 𝓞 K) :
+  is_integral ℤ (⟨x, hx⟩ : 𝓞 K) :=
+begin
+  obtain ⟨P, hPm, hP⟩ := hx,
+  refine ⟨P, hPm, _⟩,
+  rw [← polynomial.aeval_def, ← subalgebra.coe_eq_zero, polynomial.aeval_subalgebra_coe,
+    polynomial.aeval_def,  subtype.coe_mk, hP]
+end
+
+/-- 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
+
+instance [number_field K] : is_noetherian ℤ (𝓞 K) := is_integral_closure.is_noetherian _ ℚ 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_closure.is_integral_algebra ℤ K).is_field_iff_is_field 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
+
+instance 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
+
+namespace adjoin_root
+
+section
+
+open_locale polynomial
+
+local attribute [-instance] algebra_rat
+
+/-- The quotient of `ℚ[X]` by the ideal generated by an irreducible polynomial of `ℚ[X]`
+is a number field. -/
+instance {f : ℚ[X]} [hf : fact (irreducible f)] : number_field (adjoin_root f) :=
+{ to_char_zero := char_zero_of_injective_algebra_map (algebra_map ℚ _).injective,
+  to_finite_dimensional := by convert (adjoin_root.power_basis hf.out.ne_zero).finite_dimensional }
+end
+
+end adjoin_root

src/number_theory/class_number/number_field.lean → src/number_theory/number_field/class_number.lean

@@ -5,7 +5,7 @@ Authors: Anne Baanen
 -/
 import number_theory.class_number.admissible_abs
 import number_theory.class_number.finite
-import number_theory.number_field
+import number_theory.number_field.basic
 
 /-!
 # Class numbers of number fields

src/number_theory/number_field.lean → src/number_theory/number_field/embeddings.lean

@@ -1,179 +1,28 @@
 /-
-Copyright (c) 2021 Ashvni Narayanan. All rights reserved.
+Copyright (c) 2022 Xavier Roblot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Ashvni Narayanan, Anne Baanen
+Authors: Alex J. Best, Xavier Roblot
 -/
 
-import ring_theory.dedekind_domain.integral_closure
-import algebra.char_p.algebra
 import analysis.normed_space.basic
+import number_theory.number_field.basic
 import topology.algebra.polynomial
 
 /-!
-# Number fields
-This file defines a number field, the ring of integers corresponding to it and includes some
-basic facts about the embeddings into an algebraic closed field.
+# Embeddings of number fields
+This file defines the embeddings of a number field into an algebraic closed field.
 
-## 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.
-
-## Main Result
- - `eq_roots`: let `x ∈ K` with `K` number field and let `A` be an algebraic closed field of
-    char. 0, then the images of `x` by the embeddings of `K` in `A` are exactly the roots in
-    `A` of the minimal polynomial of `x` over `ℚ`.
-
-## 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]
+## Main Results
+* `number_field.embeddings.eq_roots`: let `x ∈ K` with `K` number field and let `A` be an algebraic
+  closed field of char. 0, then the images of `x` by the embeddings of `K` in `A` are exactly the
+  roots in `A` of the minimal polynomial of `x` over `ℚ`.
+* `number_field.embeddings.pow_eq_one_of_norm_eq_one`: an algebraic integer whose conjugates are
+  all of norm one is a root of unity.
 
 ## Tags
-number field, ring of integers
+number field, embeddings
 -/
 
-/-- 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 (name := ring_of_integers)
-  `𝓞` := number_field.ring_of_integers" in number_field
-
-lemma mem_ring_of_integers (x : K) : x ∈ 𝓞 K ↔ is_integral ℤ x := iff.rfl
-
-lemma is_integral_of_mem_ring_of_integers {K : Type*} [field K] {x : K} (hx : x ∈ 𝓞 K) :
-  is_integral ℤ (⟨x, hx⟩ : 𝓞 K) :=
-begin
-  obtain ⟨P, hPm, hP⟩ := hx,
-  refine ⟨P, hPm, _⟩,
-  rw [← polynomial.aeval_def, ← subalgebra.coe_eq_zero, polynomial.aeval_subalgebra_coe,
-    polynomial.aeval_def,  subtype.coe_mk, hP]
-end
-
-/-- 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
-
-instance [number_field K] : is_noetherian ℤ (𝓞 K) := is_integral_closure.is_noetherian _ ℚ 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_closure.is_integral_algebra ℤ K).is_field_iff_is_field 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
-
-instance 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
-
-namespace adjoin_root
-
-section
-
-open_locale polynomial
-
-local attribute [-instance] algebra_rat
-
-/-- The quotient of `ℚ[X]` by the ideal generated by an irreducible polynomial of `ℚ[X]`
-is a number field. -/
-instance {f : ℚ[X]} [hf : fact (irreducible f)] : number_field (adjoin_root f) :=
-{ to_char_zero := char_zero_of_injective_algebra_map (algebra_map ℚ _).injective,
-  to_finite_dimensional := by convert (adjoin_root.power_basis hf.out.ne_zero).finite_dimensional }
-end
-
-end adjoin_root
-
 namespace number_field.embeddings
 
 section fintype

src/ring_theory/discriminant.lean

@@ -6,7 +6,7 @@ Authors: Riccardo Brasca
 
 import ring_theory.trace
 import ring_theory.norm
-import number_theory.number_field
+import number_theory.number_field.basic
 
 /-!
 # Discriminant of a family of vectors