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 #

source
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
source
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) :
0 < class_group.norm_bound abv bS
source
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) :
⇑abv (⇑(algebra.norm R) a) ≤ class_group.norm_bound abv bS * y ^ fintype.card ι

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.

source
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) :
↑(⇑abv (⇑(algebra.norm R) a)) < ↑(class_group.norm_bound abv bS) * y ^ fintype.card ι

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.

source
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.

source
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
source
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] :
fin (class_group.cardM bS adm).succ ↪ R

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

Equations
source
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 R

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

Equations
source
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] :
0 ∉ class_group.finset_approx bS adm
source
@[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} :
x ∈ class_group.finset_approx bS adm ↔ ∃ (i j : fin (class_group.cardM bS adm).succ), i ≠ j ∧ ⇑(class_group.distinct_elems bS adm) i - ⇑(class_group.distinct_elems bS adm) j = x
source
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.

source
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.

source
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
source
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) :
J ≠ ⊥
source
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))) :
∃ (J : ↥(non_zero_divisors (ideal S))), ⇑class_group.mk0 I = ⇑class_group.mk0 J ∧ ⇑(algebra_map R S) ((class_group.finset_approx bS adm).prod (λ (m : R), m)) ∈ ↑J

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

source
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 S

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
source
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) :
function.surjective (class_group.mk_M_mem bS adm)
source
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) :
fintype (class_group S)

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
source
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] :
fintype (class_group S)

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