Documentation

Mathlib.NumberTheory.ClassNumber.Finite

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 #

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.
Instances For
    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) :
    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) :

    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))) :
    bI, b 0 cI, 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
    Instances For
      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
      Instances For
        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] :

        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} [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] :
          @[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), rClassGroup.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), rClassGroup.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) (mClassGroup.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) (mClassGroup.finsetApprox bS adm, m) 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) (mClassGroup.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) (mClassGroup.finsetApprox bS adm, 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) [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] :
            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] :

            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) [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] :

              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