feat(number_theory): define the class number (#9071)

We instantiate the finiteness proof of the class group for rings of integers, and define the class number of a number field, or of a separable function field, as the finite cardinality of the class group.

Co-Authored-By: Ashvni <ashvni.n@gmail.com>
Co-Authored-By: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>



Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

src/data/polynomial/field_division.lean

@@ -369,6 +369,8 @@ lemma coe_norm_unit_of_ne_zero (hp : p ≠ 0) : (norm_unit p : polynomial R) = C
 have p.leading_coeff ≠ 0 := mt leading_coeff_eq_zero.mp hp,
 by simp [comm_group_with_zero.coe_norm_unit _ this]
 
+lemma normalize_monic (h : monic p) : normalize p = p := by simp [h]
+
 theorem map_dvd_map' [field k] (f : R →+* k) {x y : polynomial R} : x.map f ∣ y.map f ↔ x ∣ y :=
 if H : x = 0 then by rw [H, map_zero, zero_dvd_iff, zero_dvd_iff, map_eq_zero]
 else by rw [← normalize_dvd_iff, ← @normalize_dvd_iff (polynomial R),

src/number_theory/class_number/finite.lean

@@ -7,8 +7,6 @@ Authors: Anne Baanen
 import linear_algebra.free_module.pid
 import linear_algebra.matrix.absolute_value
 import number_theory.class_number.admissible_absolute_value
-import number_theory.function_field
-import number_theory.number_field
 import ring_theory.class_group
 import ring_theory.norm
 

src/number_theory/class_number/function_field.lean

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2021 Anne Baanen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen
+-/
+import number_theory.class_number.admissible_card_pow_degree
+import number_theory.class_number.finite
+import number_theory.function_field
+
+/-!
+# Class numbers of function fields
+
+This file defines the class number of a function field as the (finite) cardinality of
+the class group of its ring of integers. It also proves some elementary results
+on the class number.
+
+## Main definitions
+- `function_field.class_number`: the class number of a function field is the (finite)
+cardinality of the class group of its ring of integers
+-/
+
+namespace function_field
+
+variables (Fq F : Type) [field Fq] [fintype Fq] [field F]
+variables [algebra (polynomial Fq) F] [algebra (ratfunc Fq) F]
+variables [is_scalar_tower (polynomial Fq) (ratfunc Fq) F]
+variables [function_field Fq F] [is_separable (ratfunc Fq) F]
+
+open_locale classical
+
+namespace ring_of_integers
+
+open function_field
+
+noncomputable instance  : fintype (class_group (ring_of_integers Fq F) F) :=
+class_group.fintype_of_admissible_of_finite (ratfunc Fq) F
+  (polynomial.card_pow_degree_is_admissible : absolute_value.is_admissible
+    (polynomial.card_pow_degree : absolute_value (polynomial Fq) ℤ))
+
+end ring_of_integers
+
+/-- The class number in a function field is the (finite) cardinality of the class group. -/
+noncomputable def class_number : ℕ := fintype.card (class_group (ring_of_integers Fq F) F)
+
+/-- The class number of a function field is `1` iff the ring of integers is a PID. -/
+theorem class_number_eq_one_iff :
+  class_number Fq F = 1 ↔ is_principal_ideal_ring (ring_of_integers Fq F) :=
+card_class_group_eq_one_iff
+
+end function_field

src/number_theory/class_number/number_field.lean

@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2021 Anne Baanen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen
+-/
+import number_theory.class_number.admissible_abs
+import number_theory.class_number.finite
+import number_theory.number_field
+
+/-!
+# Class numbers of number fields
+
+This file defines the class number of a number field as the (finite) cardinality of
+the class group of its ring of integers. It also proves some elementary results
+on the class number.
+
+## Main definitions
+- `number_field.class_number`: the class number of a number field is the (finite)
+cardinality of the class group of its ring of integers
+-/
+
+namespace number_field
+
+variables (K : Type*) [field K] [number_field K]
+
+namespace ring_of_integers
+
+noncomputable instance : fintype (class_group (ring_of_integers K) K) :=
+class_group.fintype_of_admissible_of_finite ℚ _ absolute_value.abs_is_admissible
+
+end ring_of_integers
+
+/-- The class number of a number field is the (finite) cardinality of the class group. -/
+noncomputable def class_number : ℕ := fintype.card (class_group (ring_of_integers K) K)
+
+variables {K}
+
+/-- The class number of a number field is `1` iff the ring of integers is a PID. -/
+theorem class_number_eq_one_iff :
+  class_number K = 1 ↔ is_principal_ideal_ring (ring_of_integers K) :=
+card_class_group_eq_one_iff
+
+end number_field
+
+namespace rat
+
+open number_field
+
+theorem class_number_eq : number_field.class_number ℚ = 1 :=
+class_number_eq_one_iff.mpr $ by convert is_principal_ideal_ring.of_surjective
+  (rat.ring_of_integers_equiv.symm : ℤ →+* ring_of_integers ℚ)
+  (rat.ring_of_integers_equiv.symm.surjective)
+
+end rat

src/number_theory/function_field.lean

@@ -5,6 +5,7 @@ Authors: Anne Baanen, Ashvni Narayanan
 -/
 import field_theory.ratfunc
 import ring_theory.algebraic
+import ring_theory.dedekind_domain
 import ring_theory.integrally_closed
 
 /-!
@@ -99,7 +100,9 @@ integral_closure.is_fraction_ring_of_finite_extension (ratfunc Fq) F
 instance : is_integrally_closed (ring_of_integers Fq F) :=
 integral_closure.is_integrally_closed_of_finite_extension (ratfunc Fq)
 
--- TODO: show `ring_of_integers Fq F` is a Dedekind domain
+instance [is_separable (ratfunc Fq) F] :
+  is_dedekind_domain (ring_of_integers Fq F) :=
+is_integral_closure.is_dedekind_domain (polynomial Fq) (ratfunc Fq) F _
 
 end ring_of_integers
 

src/number_theory/number_field.lean

@@ -84,7 +84,8 @@ variables (K)
 
 instance [number_field K] : char_zero (ring_of_integers K) := char_zero.of_algebra K
 
--- TODO: show `ring_of_integers K` is a Dedekind domain
+instance [number_field K] : is_dedekind_domain (ring_of_integers K) :=
+is_integral_closure.is_dedekind_domain ℤ ℚ K _
 
 end ring_of_integers
 

src/ring_theory/unique_factorization_domain.lean

@@ -139,7 +139,7 @@ class unique_factorization_monoid (α : Type*) [comm_cancel_monoid_with_zero α]
 (irreducible_iff_prime : ∀ {a : α}, irreducible a ↔ prime a)
 
 /-- Can't be an instance because it would cause a loop `ufm → wf_dvd_monoid → ufm → ...`. -/
-lemma ufm_of_gcd_of_wf_dvd_monoid [comm_cancel_monoid_with_zero α]
+@[reducible] lemma ufm_of_gcd_of_wf_dvd_monoid [comm_cancel_monoid_with_zero α]
   [wf_dvd_monoid α] [gcd_monoid α] : unique_factorization_monoid α :=
 { irreducible_iff_prime := λ _, gcd_monoid.irreducible_iff_prime
   .. ‹wf_dvd_monoid α› }