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} [EuclideanDomain R] [CommRing S] [IsDomain S] [Algebra R S] (abv : AbsoluteValue R ℤ) {ι : Type u_5} [DecidableEq ι] [Fintype ι] (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.

theorem ClassGroup.normBound_pos {R : Type u_1} {S : Type u_2} [EuclideanDomain R] [CommRing S] [IsDomain S] [Algebra R S] (abv : AbsoluteValue R ℤ) {ι : Type u_5} [DecidableEq ι] [Fintype ι] (bS : Basis ι R S) : 0 < ClassGroup.normBound abv bS

theorem ClassGroup.norm_le {R : Type u_1} {S : Type u_2} [EuclideanDomain R] [CommRing S] [IsDomain S] [Algebra R S] (abv : AbsoluteValue R ℤ) {ι : Type u_5} [DecidableEq ι] [Fintype ι] (bS : Basis ι R S) (a : S) {y : ℤ} (hy : ∀ (k : ι), abv ((bS.repr a) k) ≤ y) : abv ((Algebra.norm R) a) ≤ ClassGroup.normBound 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 normBound abv b * y ^ dim S.

theorem ClassGroup.norm_lt {R : Type u_1} {S : Type u_2} [EuclideanDomain R] [CommRing S] [IsDomain S] [Algebra R S] (abv : AbsoluteValue R ℤ) {ι : Type u_5} [DecidableEq ι] [Fintype ι] (bS : Basis ι R S) {T : Type u_6} [LinearOrderedRing T] (a : S) {y : T} (hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y) : ↑(abv ((Algebra.norm R) a)) < ↑(ClassGroup.normBound 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 normBound abv b * y ^ dim S.

theorem ClassGroup.exists_min {R : Type u_1} {S : Type u_2} [EuclideanDomain R] [CommRing S] [IsDomain S] [Algebra R S] (abv : AbsoluteValue R ℤ) (I : ↥(nonZeroDivisors (Ideal S))) : ∃ b ∈ ↑I, b ≠ 0 ∧ ∀ 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 ClassGroup.cardM {R : Type u_1} {S : Type u_2} [EuclideanDomain R] [CommRing S] [IsDomain S] [Algebra R S] {abv : AbsoluteValue R ℤ} {ι : Type u_5} [DecidableEq ι] [Fintype ι] (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

• ClassGroup.cardM bS adm = adm.card (↑(ClassGroup.normBound abv bS) ^ (-1 / ↑(Fintype.card ι))) ^ Fintype.card ι

noncomputable def ClassGroup.distinctElems {R : Type u_1} {S : Type u_2} [EuclideanDomain R] [CommRing S] [IsDomain S] [Algebra R S] {abv : AbsoluteValue R ℤ} {ι : Type u_5} [DecidableEq ι] [Fintype ι] (bS : Basis ι R S) (adm : abv.IsAdmissible) [Infinite R] : Fin (ClassGroup.cardM bS adm).succ ↪ R

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

Equations

• ClassGroup.distinctElems bS adm = Fin.valEmbedding.trans (Infinite.natEmbedding R)

noncomputable def ClassGroup.finsetApprox {R : Type u_1} {S : Type u_2} [EuclideanDomain R] [CommRing S] [IsDomain S] [Algebra R S] {abv : AbsoluteValue R ℤ} {ι : Type u_5} [DecidableEq ι] [Fintype ι] (bS : Basis ι R S) (adm : abv.IsAdmissible) [Infinite R] [DecidableEq R] : Finset R

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.

theorem ClassGroup.finsetApprox.zero_not_mem {R : Type u_1} {S : Type u_2} [EuclideanDomain R] [CommRing S] [IsDomain S] [Algebra R S] {abv : AbsoluteValue R ℤ} {ι : Type u_5} [DecidableEq ι] [Fintype ι] (bS : Basis ι R S) (adm : abv.IsAdmissible) [Infinite R] [DecidableEq R] : 0 ∉ ClassGroup.finsetApprox bS adm

@[simp]

theorem ClassGroup.mem_finsetApprox {R : Type u_1} {S : Type u_2} [EuclideanDomain R] [CommRing S] [IsDomain S] [Algebra R S] {abv : AbsoluteValue R ℤ} {ι : Type u_5} [DecidableEq ι] [Fintype ι] (bS : Basis ι R S) (adm : abv.IsAdmissible) [Infinite R] [DecidableEq R] {x : R} : x ∈ ClassGroup.finsetApprox bS adm ↔ ∃ (i : Fin (ClassGroup.cardM bS adm).succ) (j : Fin (ClassGroup.cardM bS adm).succ), i ≠ j ∧ (ClassGroup.distinctElems bS adm) i - (ClassGroup.distinctElems bS adm) j = x

theorem ClassGroup.exists_mem_finsetApprox {R : Type u_1} {S : Type u_2} [EuclideanDomain R] [CommRing S] [IsDomain S] [Algebra R S] {abv : AbsoluteValue R ℤ} {ι : Type u_5} [DecidableEq ι] [Fintype ι] (bS : Basis ι R S) (adm : abv.IsAdmissible) [Infinite R] [DecidableEq R] (a : S) {b : R} (hb : b ≠ 0) : ∃ (q : S), ∃ r ∈ ClassGroup.finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) 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) [EuclideanDomain R] [CommRing S] [IsDomain S] [Field L] [algRL : Algebra R L] [Algebra R S] [Algebra S L] [ist : IsScalarTower R S L] [iic : IsIntegralClosure S R L] {abv : AbsoluteValue R ℤ} {ι : Type u_5} [DecidableEq ι] [Fintype ι] (bS : Basis ι R S) (adm : abv.IsAdmissible) [Infinite R] [DecidableEq R] [Algebra.IsAlgebraic R L] (a : S) {b : S} (hb : b ≠ 0) : ∃ (q : S), ∃ r ∈ ClassGroup.finsetApprox 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 ClassGroup.prod_finsetApprox_ne_zero {R : Type u_1} {S : Type u_2} [EuclideanDomain R] [CommRing S] [IsDomain S] [Algebra R S] {abv : AbsoluteValue R ℤ} {ι : Type u_5} [DecidableEq ι] [Fintype ι] (bS : Basis ι R S) (adm : abv.IsAdmissible) [Infinite R] [DecidableEq R] : (algebraMap R S) (∏ m ∈ ClassGroup.finsetApprox bS adm, m) ≠ 0

theorem ClassGroup.ne_bot_of_prod_finsetApprox_mem {R : Type u_1} {S : Type u_2} [EuclideanDomain R] [CommRing S] [IsDomain S] [Algebra R S] {abv : AbsoluteValue R ℤ} {ι : Type u_5} [DecidableEq ι] [Fintype ι] (bS : Basis ι R S) (adm : abv.IsAdmissible) [Infinite R] [DecidableEq R] (J : Ideal S) (h : (algebraMap R S) (∏ m ∈ ClassGroup.finsetApprox bS adm, m) ∈ J) : J ≠ ⊥

theorem ClassGroup.exists_mk0_eq_mk0 {R : Type u_1} {S : Type u_2} (L : Type u_4) [EuclideanDomain R] [CommRing S] [IsDomain S] [Field L] [algRL : Algebra R L] [Algebra R S] [Algebra S L] [ist : IsScalarTower R S L] [iic : IsIntegralClosure S R L] {abv : AbsoluteValue R ℤ} {ι : Type u_5} [DecidableEq ι] [Fintype ι] (bS : Basis ι R S) (adm : abv.IsAdmissible) [Infinite R] [DecidableEq R] [IsDedekindDomain S] [Algebra.IsAlgebraic R L] (I : ↥(nonZeroDivisors (Ideal S))) : ∃ (J : ↥(nonZeroDivisors (Ideal S))), ClassGroup.mk0 I = ClassGroup.mk0 J ∧ (algebraMap R S) (∏ m ∈ ClassGroup.finsetApprox bS adm, 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} [EuclideanDomain R] [CommRing S] [IsDomain S] [Algebra R S] {abv : AbsoluteValue R ℤ} {ι : Type u_5} [DecidableEq ι] [Fintype ι] (bS : Basis ι R S) (adm : abv.IsAdmissible) [Infinite R] [DecidableEq R] [IsDedekindDomain S] (J : { J : Ideal S // (algebraMap R S) (∏ m ∈ ClassGroup.finsetApprox bS adm, m) ∈ J }) : ClassGroup S

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

• ClassGroup.mkMMem bS adm J = ClassGroup.mk0 ⟨↑J, ⋯⟩

theorem ClassGroup.mkMMem_surjective {R : Type u_1} {S : Type u_2} (L : Type u_4) [EuclideanDomain R] [CommRing S] [IsDomain S] [Field L] [algRL : Algebra R L] [Algebra R S] [Algebra S L] [ist : IsScalarTower R S L] [iic : IsIntegralClosure S R L] {abv : AbsoluteValue R ℤ} {ι : Type u_5} [DecidableEq ι] [Fintype ι] (bS : Basis ι R S) (adm : abv.IsAdmissible) [Infinite R] [DecidableEq R] [IsDedekindDomain S] [Algebra.IsAlgebraic R L] : Function.Surjective (ClassGroup.mkMMem bS adm)

noncomputable def ClassGroup.fintypeOfAdmissibleOfAlgebraic {R : Type u_1} {S : Type u_2} (L : Type u_4) [EuclideanDomain R] [CommRing S] [IsDomain S] [Field L] [algRL : Algebra R L] [Algebra R S] [Algebra S L] [ist : IsScalarTower R S L] [iic : IsIntegralClosure S R L] {abv : AbsoluteValue R ℤ} {ι : Type u_5} [DecidableEq ι] [Fintype ι] (bS : Basis ι R S) (adm : abv.IsAdmissible) [Infinite R] [DecidableEq R] [IsDedekindDomain S] [Algebra.IsAlgebraic R L] : Fintype (ClassGroup S)

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

• ClassGroup.fintypeOfAdmissibleOfAlgebraic L bS adm = Fintype.ofSurjective (ClassGroup.mkMMem bS adm) ⋯

noncomputable def ClassGroup.fintypeOfAdmissibleOfFinite {R : Type u_1} {S : Type u_2} (K : Type u_3) (L : Type u_4) [EuclideanDomain R] [CommRing S] [IsDomain S] [Field K] [Field L] [Algebra R K] [IsFractionRing R K] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [algRL : Algebra R L] [IsScalarTower R K L] [Algebra R S] [Algebra S L] [ist : IsScalarTower R S L] [iic : IsIntegralClosure S R L] {abv : AbsoluteValue R ℤ} (adm : abv.IsAdmissible) [Infinite R] [DecidableEq R] : Fintype (ClassGroup 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 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.