mathlib3 documentation

number_theory.class_number.finite

Class numbers of global fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. In this file, we use the notion of "admissible absolute value" to prove finiteness of the class group for number fields and function fields, and define class_number as the order of this group.

Main definitions #

noncomputable def class_group.norm_bound {R : Type u_1} {S : Type u_2} [euclidean_domain R] [comm_ring S] [is_domain S] [algebra R S] (abv : absolute_value R ) {ι : Type u_5} [decidable_eq ι] [fintype ι] (bS : basis ι R S) :

If b is an R-basis of S of cardinality n, then norm_bound abv b is an integer such that for every R-integral element a : S with coordinates ≤ y, we have algebra.norm a ≤ norm_bound abv b * y ^ n. (See alsonorm_leandnorm_lt`).

Equations
theorem class_group.norm_bound_pos {R : Type u_1} {S : Type u_2} [euclidean_domain R] [comm_ring S] [is_domain S] [algebra R S] (abv : absolute_value R ) {ι : Type u_5} [decidable_eq ι] [fintype ι] (bS : basis ι R S) :
theorem class_group.norm_le {R : Type u_1} {S : Type u_2} [euclidean_domain R] [comm_ring S] [is_domain S] [algebra R S] (abv : absolute_value R ) {ι : Type u_5} [decidable_eq ι] [fintype ι] (bS : basis ι R S) (a : S) {y : } (hy : (k : ι), abv (((bS.repr) a) k) y) :

If the R-integral element a : S has coordinates ≤ y with respect to some basis b, its norm is less than norm_bound abv b * y ^ dim S.

theorem class_group.norm_lt {R : Type u_1} {S : Type u_2} [euclidean_domain R] [comm_ring S] [is_domain S] [algebra R S] (abv : absolute_value R ) {ι : Type u_5} [decidable_eq ι] [fintype ι] (bS : basis ι R S) {T : Type u_3} [linear_ordered_ring T] (a : S) {y : T} (hy : (k : ι), (abv (((bS.repr) a) k)) < y) :

If the R-integral element a : S has coordinates < y with respect to some basis b, its norm is strictly less than norm_bound abv b * y ^ dim S.

theorem class_group.exists_min {R : Type u_1} {S : Type u_2} [euclidean_domain R] [comm_ring S] [is_domain S] [algebra R S] (abv : absolute_value R ) (I : (non_zero_divisors (ideal S))) :
(b : S) (H : b I), b 0 (c : S), c I abv ((algebra.norm R) c) < abv ((algebra.norm R) b) c = 0

A nonzero ideal has an element of minimal norm.

noncomputable def class_group.cardM {R : Type u_1} {S : Type u_2} [euclidean_domain R] [comm_ring S] [is_domain S] [algebra R S] {abv : absolute_value R } {ι : Type u_5} [decidable_eq ι] [fintype ι] (bS : basis ι R S) (adm : abv.is_admissible) :

If we have a large enough set of elements in R^ι, then there will be a pair whose remainders are close together. We'll show that all sets of cardinality at least cardM bS adm elements satisfy this condition.

The value of cardM is not at all optimal: for specific choices of R, the minimum cardinality can be exponentially smaller.

Equations
noncomputable def class_group.distinct_elems {R : Type u_1} {S : Type u_2} [euclidean_domain R] [comm_ring S] [is_domain S] [algebra R S] {abv : absolute_value R } {ι : Type u_5} [decidable_eq ι] [fintype ι] (bS : basis ι R S) (adm : abv.is_admissible) [infinite R] :

In the following results, we need a large set of distinct elements of R.

Equations
noncomputable def class_group.finset_approx {R : Type u_1} {S : Type u_2} [euclidean_domain R] [comm_ring S] [is_domain S] [algebra R S] {abv : absolute_value R } {ι : Type u_5} [decidable_eq ι] [fintype ι] (bS : basis ι R S) (adm : abv.is_admissible) [infinite R] [decidable_eq R] :

finset_approx is a finite set such that each fractional ideal in the integral closure contains an element close to finset_approx.

Equations
theorem class_group.finset_approx.zero_not_mem {R : Type u_1} {S : Type u_2} [euclidean_domain R] [comm_ring S] [is_domain S] [algebra R S] {abv : absolute_value R } {ι : Type u_5} [decidable_eq ι] [fintype ι] (bS : basis ι R S) (adm : abv.is_admissible) [infinite R] [decidable_eq R] :
@[simp]
theorem class_group.mem_finset_approx {R : Type u_1} {S : Type u_2} [euclidean_domain R] [comm_ring S] [is_domain S] [algebra R S] {abv : absolute_value R } {ι : Type u_5} [decidable_eq ι] [fintype ι] (bS : basis ι R S) (adm : abv.is_admissible) [infinite R] [decidable_eq R] {x : R} :
theorem class_group.exists_mem_finset_approx {R : Type u_1} {S : Type u_2} [euclidean_domain R] [comm_ring S] [is_domain S] [algebra R S] {abv : absolute_value R } {ι : Type u_5} [decidable_eq ι] [fintype ι] (bS : basis ι R S) (adm : abv.is_admissible) [infinite R] [decidable_eq R] (a : S) {b : R} (hb : b 0) :
(q : S) (r : R) (H : r class_group.finset_approx bS adm), abv ((algebra.norm R) (r a - b q)) < abv ((algebra.norm R) ((algebra_map R S) b))

We can approximate a / b : L with q / r, where r has finitely many options for L.

theorem class_group.exists_mem_finset_approx' {R : Type u_1} {S : Type u_2} (L : Type u_4) [euclidean_domain R] [comm_ring S] [is_domain S] [field L] [algRL : algebra R L] [algebra R S] [algebra S L] [ist : is_scalar_tower R S L] [iic : is_integral_closure S R L] {abv : absolute_value R } {ι : Type u_5} [decidable_eq ι] [fintype ι] (bS : basis ι R S) (adm : abv.is_admissible) [infinite R] [decidable_eq R] (h : algebra.is_algebraic R L) (a : S) {b : S} (hb : b 0) :
(q : S) (r : R) (H : r class_group.finset_approx bS adm), abv ((algebra.norm R) (r a - q * b)) < abv ((algebra.norm R) b)

We can approximate a / b : L with q / r, where r has finitely many options for L.

theorem class_group.prod_finset_approx_ne_zero {R : Type u_1} {S : Type u_2} [euclidean_domain R] [comm_ring S] [is_domain S] [algebra R S] {abv : absolute_value R } {ι : Type u_5} [decidable_eq ι] [fintype ι] (bS : basis ι R S) (adm : abv.is_admissible) [infinite R] [decidable_eq R] :
(algebra_map R S) ((class_group.finset_approx bS adm).prod (λ (m : R), m)) 0
theorem class_group.ne_bot_of_prod_finset_approx_mem {R : Type u_1} {S : Type u_2} [euclidean_domain R] [comm_ring S] [is_domain S] [algebra R S] {abv : absolute_value R } {ι : Type u_5} [decidable_eq ι] [fintype ι] (bS : basis ι R S) (adm : abv.is_admissible) [infinite R] [decidable_eq R] (J : ideal S) (h : (algebra_map R S) ((class_group.finset_approx bS adm).prod (λ (m : R), m)) J) :
theorem class_group.exists_mk0_eq_mk0 {R : Type u_1} {S : Type u_2} (L : Type u_4) [euclidean_domain R] [comm_ring S] [is_domain S] [field L] [algRL : algebra R L] [algebra R S] [algebra S L] [ist : is_scalar_tower R S L] [iic : is_integral_closure S R L] {abv : absolute_value R } {ι : Type u_5} [decidable_eq ι] [fintype ι] (bS : basis ι R S) (adm : abv.is_admissible) [infinite R] [decidable_eq R] [is_dedekind_domain S] (h : algebra.is_algebraic R L) (I : (non_zero_divisors (ideal S))) :

Each class in the class group contains an ideal J such that M := Π m ∈ finset_approx is in J.

noncomputable def class_group.mk_M_mem {R : Type u_1} {S : Type u_2} [euclidean_domain R] [comm_ring S] [is_domain S] [algebra R S] {abv : absolute_value R } {ι : Type u_5} [decidable_eq ι] [fintype ι] (bS : basis ι R S) (adm : abv.is_admissible) [infinite R] [decidable_eq R] [is_dedekind_domain S] (J : {J // (algebra_map R S) ((class_group.finset_approx bS adm).prod (λ (m : R), m)) J}) :

class_group.mk_M_mem is a specialization of class_group.mk0 to (the finite set of) ideals that contain M := ∏ m in finset_approx L f abs, m. By showing this function is surjective, we prove that the class group is finite.

Equations
theorem class_group.mk_M_mem_surjective {R : Type u_1} {S : Type u_2} (L : Type u_4) [euclidean_domain R] [comm_ring S] [is_domain S] [field L] [algRL : algebra R L] [algebra R S] [algebra S L] [ist : is_scalar_tower R S L] [iic : is_integral_closure S R L] {abv : absolute_value R } {ι : Type u_5} [decidable_eq ι] [fintype ι] (bS : basis ι R S) (adm : abv.is_admissible) [infinite R] [decidable_eq R] [is_dedekind_domain S] (h : algebra.is_algebraic R L) :
noncomputable def class_group.fintype_of_admissible_of_algebraic {R : Type u_1} {S : Type u_2} (L : Type u_4) [euclidean_domain R] [comm_ring S] [is_domain S] [field L] [algRL : algebra R L] [algebra R S] [algebra S L] [ist : is_scalar_tower R S L] [iic : is_integral_closure S R L] {abv : absolute_value R } {ι : Type u_5} [decidable_eq ι] [fintype ι] (bS : basis ι R S) (adm : abv.is_admissible) [infinite R] [decidable_eq R] [is_dedekind_domain S] (h : algebra.is_algebraic R L) :

The main theorem: the class group of an integral closure S of R in an algebraic extension L is finite if there is an admissible absolute value.

See also class_group.fintype_of_admissible_of_finite where L is a finite extension of K = Frac(R), supplying most of the required assumptions automatically.

Equations
noncomputable def class_group.fintype_of_admissible_of_finite {R : Type u_1} {S : Type u_2} (K : Type u_3) (L : Type u_4) [euclidean_domain R] [comm_ring S] [is_domain S] [field K] [field L] [algebra R K] [is_fraction_ring R K] [algebra K L] [finite_dimensional K L] [is_separable K L] [algRL : algebra R L] [is_scalar_tower R K L] [algebra R S] [algebra S L] [ist : is_scalar_tower R S L] [iic : is_integral_closure S R L] {abv : absolute_value R } (adm : abv.is_admissible) [infinite R] [decidable_eq R] :

The main theorem: the class group of an integral closure S of R in a finite extension L of K = Frac(R) is finite if there is an admissible absolute value.

See also class_group.fintype_of_admissible_of_algebraic where L is an algebraic extension of R, that includes some extra assumptions.

Equations