# Class numbers of global fields #

In this file, we use the notion of "admissible absolute value" to prove finiteness of the class group for number fields and function fields.

## Main definitions #

• ClassGroup.fintypeOfAdmissibleOfAlgebraic: if R has an admissible absolute value, its integral closure has a finite class group
noncomputable def ClassGroup.normBound {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] (abv : ) {ι : Type u_5} [] [] (bS : Basis ι R S) :

If b is an R-basis of S of cardinality n, then normBound 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 also norm_leandnorm_lt).

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem ClassGroup.normBound_pos {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] (abv : ) {ι : Type u_5} [] [] (bS : Basis ι R S) :
theorem ClassGroup.norm_le {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] (abv : ) {ι : Type u_5} [] [] (bS : Basis ι R S) (a : S) {y : } (hy : ∀ (k : ι), abv ((bS.repr a) k) y) :
abv (() a) ClassGroup.normBound abv bS *

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

theorem ClassGroup.norm_lt {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] (abv : ) {ι : Type u_5} [] [] (bS : Basis ι R S) {T : Type u_6} (a : S) {y : T} (hy : ∀ (k : ι), (abv ((bS.repr a) k)) < y) :
(abv (() a)) < (ClassGroup.normBound abv bS) *

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

theorem ClassGroup.exists_min {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] (abv : ) (I : ()) :
bI, b 0 cI, abv (() c) < abv (() b)c = 0

A nonzero ideal has an element of minimal norm.

noncomputable def ClassGroup.cardM {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] {abv : } {ι : Type u_5} [] [] (bS : Basis ι R S) (adm : abv.IsAdmissible) :

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
Instances For
noncomputable def ClassGroup.distinctElems {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] {abv : } {ι : Type u_5} [] [] (bS : Basis ι R S) (adm : abv.IsAdmissible) [] :

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

Equations
• = Fin.valEmbedding.trans
Instances For
noncomputable def ClassGroup.finsetApprox {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] {abv : } {ι : Type u_5} [] [] (bS : Basis ι R S) (adm : abv.IsAdmissible) [] [] :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem ClassGroup.finsetApprox.zero_not_mem {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] {abv : } {ι : Type u_5} [] [] (bS : Basis ι R S) (adm : abv.IsAdmissible) [] [] :
0
@[simp]
theorem ClassGroup.mem_finsetApprox {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] {abv : } {ι : Type u_5} [] [] (bS : Basis ι R S) (adm : abv.IsAdmissible) [] [] {x : R} :
x ∃ (i : Fin (ClassGroup.cardM bS adm).succ) (j : Fin (ClassGroup.cardM bS adm).succ), i j () i - () j = x
theorem ClassGroup.exists_mem_finsetApprox {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] {abv : } {ι : Type u_5} [] [] (bS : Basis ι R S) (adm : abv.IsAdmissible) [] [] (a : S) {b : R} (hb : b 0) :
∃ (q : S), r, abv (() (r a - b q)) < abv (() (() b))

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

theorem ClassGroup.exists_mem_finset_approx' {R : Type u_1} {S : Type u_2} (L : Type u_4) [] [] [] [] [algRL : Algebra R L] [Algebra R S] [Algebra S L] [ist : ] [iic : ] {abv : } {ι : Type u_5} [] [] (bS : Basis ι R S) (adm : abv.IsAdmissible) [] [] [] (a : S) {b : S} (hb : b 0) :
∃ (q : S), r, abv (() (r a - q * b)) < abv (() b)

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

theorem ClassGroup.prod_finsetApprox_ne_zero {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] {abv : } {ι : Type u_5} [] [] (bS : Basis ι R S) (adm : abv.IsAdmissible) [] [] :
() (m, m) 0
theorem ClassGroup.ne_bot_of_prod_finsetApprox_mem {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] {abv : } {ι : Type u_5} [] [] (bS : Basis ι R S) (adm : abv.IsAdmissible) [] [] (J : ) (h : () (m, m) J) :
theorem ClassGroup.exists_mk0_eq_mk0 {R : Type u_1} {S : Type u_2} (L : Type u_4) [] [] [] [] [algRL : Algebra R L] [Algebra R S] [Algebra S L] [ist : ] [iic : ] {abv : } {ι : Type u_5} [] [] (bS : Basis ι R S) (adm : abv.IsAdmissible) [] [] [] [] (I : ()) :
∃ (J : ()), ClassGroup.mk0 I = ClassGroup.mk0 J () (m, m) J

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

noncomputable def ClassGroup.mkMMem {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] {abv : } {ι : Type u_5} [] [] (bS : Basis ι R S) (adm : abv.IsAdmissible) [] [] [] (J : { J : // () (m, m) J }) :

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

Equations
Instances For
theorem ClassGroup.mkMMem_surjective {R : Type u_1} {S : Type u_2} (L : Type u_4) [] [] [] [] [algRL : Algebra R L] [Algebra R S] [Algebra S L] [ist : ] [iic : ] {abv : } {ι : Type u_5} [] [] (bS : Basis ι R S) (adm : abv.IsAdmissible) [] [] [] [] :
noncomputable def ClassGroup.fintypeOfAdmissibleOfAlgebraic {R : Type u_1} {S : Type u_2} (L : Type u_4) [] [] [] [] [algRL : Algebra R L] [Algebra R S] [Algebra S L] [ist : ] [iic : ] {abv : } {ι : Type u_5} [] [] (bS : Basis ι R S) (adm : abv.IsAdmissible) [] [] [] [] :

The class number 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 ClassGroup.fintypeOfAdmissibleOfFinite where L is a finite extension of K = Frac(R), supplying most of the required assumptions automatically.

Equations
Instances For
noncomputable def ClassGroup.fintypeOfAdmissibleOfFinite {R : Type u_1} {S : Type u_2} (K : Type u_3) (L : Type u_4) [] [] [] [] [] [Algebra R K] [] [Algebra K L] [] [] [algRL : Algebra R L] [] [Algebra R S] [Algebra S L] [ist : ] [iic : ] {abv : } (adm : abv.IsAdmissible) [] [] :

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 ClassGroup.fintypeOfAdmissibleOfAlgebraic where L is an algebraic extension of R`, that includes some extra assumptions.

Equations
• One or more equations did not get rendered due to their size.
Instances For