Documentation

Mathlib.RingTheory.ClassGroup

The ideal class group #

This file defines the ideal class group ClassGroup R of fractional ideals of R inside its field of fractions.

Main definitions #

Main results #

Implementation details #

The definition of ClassGroup R involves FractionRing R. However, the API should be completely identical no matter the choice of field of fractions for R.

theorem toPrincipalIdeal_def (R : Type u_4) (K : Type u_5) [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] :
toPrincipalIdeal R K = { toOneHom := { toFun := fun (x : Kˣ) => { val := FractionalIdeal.spanSingleton (nonZeroDivisors R) x, inv := FractionalIdeal.spanSingleton (nonZeroDivisors R) (x)⁻¹, val_inv := , inv_val := }, map_one' := }, map_mul' := }
@[irreducible]
def toPrincipalIdeal (R : Type u_4) (K : Type u_5) [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] :

toPrincipalIdeal R K x sends x ≠ 0 : K to the fractional R-ideal generated by x

Equations
Instances For
    @[simp]
    theorem coe_toPrincipalIdeal {R : Type u_1} {K : Type u_2} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] (x : Kˣ) :
    @[simp]
    Equations
    • =
    def ClassGroup (R : Type u_1) [CommRing R] [IsDomain R] :
    Type u_1

    The ideal class group of R is the group of invertible fractional ideals modulo the principal ideals.

    Equations
    Instances For
      noncomputable instance instInhabitedClassGroup (R : Type u_1) [CommRing R] [IsDomain R] :
      Equations
      noncomputable def ClassGroup.mk {R : Type u_1} {K : Type u_2} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] :

      Send a nonzero fractional ideal to the corresponding class in the class group.

      Equations
      Instances For
        theorem ClassGroup.Quot_mk_eq_mk {R : Type u_1} [CommRing R] [IsDomain R] (I : (FractionalIdeal (nonZeroDivisors R) (FractionRing R))ˣ) :
        Quot.mk Setoid.r I = ClassGroup.mk I
        theorem ClassGroup.mk_eq_mk {R : Type u_1} [CommRing R] [IsDomain R] {I : (FractionalIdeal (nonZeroDivisors R) (FractionRing R))ˣ} {J : (FractionalIdeal (nonZeroDivisors R) (FractionRing R))ˣ} :
        ClassGroup.mk I = ClassGroup.mk J ∃ (x : (FractionRing R)ˣ), I * (toPrincipalIdeal R (FractionRing R)) x = J
        theorem ClassGroup.mk_eq_mk_of_coe_ideal {R : Type u_1} [CommRing R] [IsDomain R] {I : (FractionalIdeal (nonZeroDivisors R) (FractionRing R))ˣ} {J : (FractionalIdeal (nonZeroDivisors R) (FractionRing R))ˣ} {I' : Ideal R} {J' : Ideal R} (hI : I = I') (hJ : J = J') :
        ClassGroup.mk I = ClassGroup.mk J ∃ (x : R) (y : R), x 0 y 0 Ideal.span {x} * I' = Ideal.span {y} * J'
        theorem ClassGroup.mk_eq_one_of_coe_ideal {R : Type u_1} [CommRing R] [IsDomain R] {I : (FractionalIdeal (nonZeroDivisors R) (FractionRing R))ˣ} {I' : Ideal R} (hI : I = I') :
        ClassGroup.mk I = 1 ∃ (x : R), x 0 I' = Ideal.span {x}
        theorem ClassGroup.induction {R : Type u_1} (K : Type u_2) [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] {P : ClassGroup RProp} (h : ∀ (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ), P (ClassGroup.mk I)) (x : ClassGroup R) :
        P x

        Induction principle for the class group: to show something holds for all x : ClassGroup R, we can choose a fraction field K and show it holds for the equivalence class of each I : FractionalIdeal R⁰ K.

        The definition of the class group does not depend on the choice of field of fractions.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem ClassGroup.equiv_mk {R : Type u_1} (K : Type u_2) [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] (K' : Type u_4) [Field K'] [Algebra R K'] [IsFractionRing R K'] (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ) :
          @[simp]
          theorem ClassGroup.mk_canonicalEquiv {R : Type u_1} (K : Type u_2) [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] (K' : Type u_4) [Field K'] [Algebra R K'] [IsFractionRing R K'] (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ) :
          ClassGroup.mk ((Units.map (FractionalIdeal.canonicalEquiv (nonZeroDivisors R) K K')) I) = ClassGroup.mk I
          noncomputable def FractionalIdeal.mk0 {R : Type u_1} (K : Type u_2) [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] [IsDedekindDomain R] :

          Send a nonzero integral ideal to an invertible fractional ideal.

          Equations
          Instances For
            @[simp]
            theorem FractionalIdeal.coe_mk0 {R : Type u_1} (K : Type u_2) [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] [IsDedekindDomain R] (I : (nonZeroDivisors (Ideal R))) :
            ((FractionalIdeal.mk0 K) I) = I
            noncomputable def ClassGroup.mk0 {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] :

            Send a nonzero ideal to the corresponding class in the class group.

            Equations
            Instances For
              @[simp]
              theorem ClassGroup.mk_mk0 {R : Type u_1} (K : Type u_2) [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] [IsDedekindDomain R] (I : (nonZeroDivisors (Ideal R))) :
              ClassGroup.mk ((FractionalIdeal.mk0 K) I) = ClassGroup.mk0 I
              @[simp]
              theorem ClassGroup.equiv_mk0 {R : Type u_1} (K : Type u_2) [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] [IsDedekindDomain R] (I : (nonZeroDivisors (Ideal R))) :
              theorem ClassGroup.mk0_eq_mk0_iff_exists_fraction_ring {R : Type u_1} (K : Type u_2) [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] [IsDedekindDomain R] {I : (nonZeroDivisors (Ideal R))} {J : (nonZeroDivisors (Ideal R))} :
              ClassGroup.mk0 I = ClassGroup.mk0 J ∃ (x : K) (_ : x 0), FractionalIdeal.spanSingleton (nonZeroDivisors R) x * I = J
              theorem ClassGroup.mk0_eq_mk0_iff {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] {I : (nonZeroDivisors (Ideal R))} {J : (nonZeroDivisors (Ideal R))} :
              ClassGroup.mk0 I = ClassGroup.mk0 J ∃ (x : R) (y : R) (_ : x 0) (_ : y 0), Ideal.span {x} * I = Ideal.span {y} * J
              noncomputable def ClassGroup.integralRep {R : Type u_1} [CommRing R] (I : FractionalIdeal (nonZeroDivisors R) (FractionRing R)) :

              Maps a nonzero fractional ideal to an integral representative in the class group.

              Equations
              Instances For
                theorem ClassGroup.mk0_integralRep {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] (I : (FractionalIdeal (nonZeroDivisors R) (FractionRing R))ˣ) :
                ClassGroup.mk0 { val := ClassGroup.integralRep I, property := } = ClassGroup.mk I
                theorem ClassGroup.mk_eq_one_iff {R : Type u_1} {K : Type u_2} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] {I : (FractionalIdeal (nonZeroDivisors R) K)ˣ} :
                ClassGroup.mk I = 1 Submodule.IsPrincipal I
                theorem ClassGroup.mk0_eq_one_iff {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] {I : Ideal R} (hI : I nonZeroDivisors (Ideal R)) :
                ClassGroup.mk0 { val := I, property := hI } = 1 Submodule.IsPrincipal I
                theorem ClassGroup.mk0_eq_mk0_inv_iff {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] {I : (nonZeroDivisors (Ideal R))} {J : (nonZeroDivisors (Ideal R))} :
                ClassGroup.mk0 I = (ClassGroup.mk0 J)⁻¹ ∃ (x : R), x 0 I * J = Ideal.span {x}
                noncomputable instance instFintypeClassGroup {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] :

                The class group of principal ideal domain is finite (in fact a singleton).

                See ClassGroup.fintypeOfAdmissibleOfFinite for a finiteness proof that works for rings of integers of global fields.

                Equations
                • instFintypeClassGroup = { elems := {1}, complete := }

                The class number of a principal ideal domain is 1.

                The class number is 1 iff the ring of integers is a principal ideal domain.