# 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 #

• toPrincipalIdeal sends an invertible x : K to an invertible fractional ideal
• ClassGroup is the quotient of invertible fractional ideals modulo toPrincipalIdeal.range
• ClassGroup.mk0 sends a nonzero integral ideal in a Dedekind domain to its class

## Main results #

• ClassGroup.mk0_eq_mk0_iff shows the equivalence with the "classical" definition, where I ~ J iff x I = y J for x y ≠ (0 : R)

## 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) [] [] [Algebra R K] [] :
= { toOneHom := { toFun := fun x => { val := , inv := , val_inv := (_ : = 1), inv_val := (_ : = 1) }, map_one' := (_ : (fun x => { val := , inv := , val_inv := (_ : = 1), inv_val := (_ : = 1) }) 1 = 1) }, map_mul' := (_ : ∀ (x y : Kˣ), OneHom.toFun { toFun := fun x => { val := , inv := , val_inv := (_ : = 1), inv_val := (_ : = 1) }, map_one' := (_ : (fun x => { val := , inv := , val_inv := (_ : = 1), inv_val := (_ : = 1) }) 1 = 1) } (x * y) = OneHom.toFun { toFun := fun x => { val := , inv := , val_inv := (_ : = 1), inv_val := (_ : = 1) }, map_one' := (_ : (fun x => { val := , inv := , val_inv := (_ : = 1), inv_val := (_ : = 1) }) 1 = 1) } x * OneHom.toFun { toFun := fun x => { val := , inv := , val_inv := (_ : = 1), inv_val := (_ : = 1) }, map_one' := (_ : (fun x => { val := , inv := , val_inv := (_ : = 1), inv_val := (_ : = 1) }) 1 = 1) } y) }
@[irreducible]
def toPrincipalIdeal (R : Type u_4) (K : Type u_5) [] [] [Algebra R K] [] :

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

Instances For
@[simp]
theorem coe_toPrincipalIdeal {R : Type u_1} {K : Type u_2} [] [] [Algebra R K] [] (x : Kˣ) :
↑(↑() x) =
@[simp]
theorem toPrincipalIdeal_eq_iff {R : Type u_1} {K : Type u_2} [] [] [Algebra R K] [] {I : ()ˣ} {x : Kˣ} :
↑() x = I
theorem mem_principal_ideals_iff {R : Type u_1} {K : Type u_2} [] [] [Algebra R K] [] {I : ()ˣ} :
I x,
instance PrincipalIdeals.normal {R : Type u_1} {K : Type u_2} [] [] [Algebra R K] [] :
def ClassGroup (R : Type u_1) [] [] :
Type u_1

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

Instances For
noncomputable instance instCommGroupClassGroup (R : Type u_1) [] [] :
noncomputable instance instInhabitedClassGroup (R : Type u_1) [] [] :
noncomputable def ClassGroup.mk {R : Type u_1} {K : Type u_2} [] [] [Algebra R K] [] [] :
()ˣ →*

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

Instances For
theorem ClassGroup.Quot_mk_eq_mk {R : Type u_1} [] [] (I : ()ˣ) :
Quot.mk Setoid.r I = ClassGroup.mk I
theorem ClassGroup.mk_eq_mk {R : Type u_1} [] [] {I : ()ˣ} {J : ()ˣ} :
ClassGroup.mk I = ClassGroup.mk J x, I * ↑() x = J
theorem ClassGroup.mk_eq_mk_of_coe_ideal {R : Type u_1} [] [] {I : ()ˣ} {J : ()ˣ} {I' : } {J' : } (hI : I = I') (hJ : J = J') :
ClassGroup.mk I = ClassGroup.mk J x y, x 0 y 0 Ideal.span {x} * I' = Ideal.span {y} * J'
theorem ClassGroup.mk_eq_one_of_coe_ideal {R : Type u_1} [] [] {I : ()ˣ} {I' : } (hI : I = I') :
ClassGroup.mk I = 1 x, x 0 I' = Ideal.span {x}
theorem ClassGroup.induction {R : Type u_1} (K : Type u_2) [] [] [Algebra R K] [] [] {P : } (h : (I : ()ˣ) → P (ClassGroup.mk I)) (x : ) :
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.

noncomputable def ClassGroup.equiv {R : Type u_1} (K : Type u_2) [] [] [Algebra R K] [] [] :
≃* ()ˣ

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

Instances For
@[simp]
theorem ClassGroup.equiv_mk {R : Type u_1} (K : Type u_2) [] [] [Algebra R K] [] [] (K' : Type u_4) [Field K'] [Algebra R K'] [] (I : ()ˣ) :
↑() (ClassGroup.mk I) = ↑() (↑() I)
@[simp]
theorem ClassGroup.mk_canonicalEquiv {R : Type u_1} (K : Type u_2) [] [] [Algebra R K] [] [] (K' : Type u_4) [Field K'] [Algebra R K'] [] (I : ()ˣ) :
ClassGroup.mk (↑() I) = ClassGroup.mk I
noncomputable def FractionalIdeal.mk0 {R : Type u_1} (K : Type u_2) [] [] [Algebra R K] [] [] [] :
{ x // x } →* ()ˣ

Send a nonzero integral ideal to an invertible fractional ideal.

Instances For
@[simp]
theorem FractionalIdeal.coe_mk0 {R : Type u_1} (K : Type u_2) [] [] [Algebra R K] [] [] [] (I : { x // x }) :
↑(↑() I) = I
theorem FractionalIdeal.canonicalEquiv_mk0 {R : Type u_1} (K : Type u_2) [] [] [Algebra R K] [] [] [] (K' : Type u_4) [Field K'] [Algebra R K'] [] (I : { x // x }) :
↑() ↑(↑() I) = ↑(↑() I)
@[simp]
theorem FractionalIdeal.map_canonicalEquiv_mk0 {R : Type u_1} (K : Type u_2) [] [] [Algebra R K] [] [] [] (K' : Type u_4) [Field K'] [Algebra R K'] [] (I : { x // x }) :
↑() (↑() I) = ↑() I
noncomputable def ClassGroup.mk0 {R : Type u_1} [] [] [] :
{ x // x } →*

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

Instances For
@[simp]
theorem ClassGroup.mk_mk0 {R : Type u_1} (K : Type u_2) [] [] [Algebra R K] [] [] [] (I : { x // x }) :
ClassGroup.mk (↑() I) = ClassGroup.mk0 I
@[simp]
theorem ClassGroup.equiv_mk0 {R : Type u_1} (K : Type u_2) [] [] [Algebra R K] [] [] [] (I : { x // x }) :
↑() (ClassGroup.mk0 I) = ↑() (↑() I)
theorem ClassGroup.mk0_eq_mk0_iff_exists_fraction_ring {R : Type u_1} (K : Type u_2) [] [] [Algebra R K] [] [] [] {I : { x // x }} {J : { x // x }} :
ClassGroup.mk0 I = ClassGroup.mk0 J x x_1, = J
theorem ClassGroup.mk0_eq_mk0_iff {R : Type u_1} [] [] [] {I : { x // x }} {J : { x // x }} :
ClassGroup.mk0 I = ClassGroup.mk0 J x y _hx _hy, Ideal.span {x} * I = Ideal.span {y} * J
noncomputable def ClassGroup.integralRep {R : Type u_1} [] [] (I : ) :

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

Instances For
theorem ClassGroup.integralRep_mem_nonZeroDivisors {R : Type u_1} [] [] {I : } (hI : I 0) :
theorem ClassGroup.mk0_integralRep {R : Type u_1} [] [] [] (I : ()ˣ) :
ClassGroup.mk0 { val := , property := (_ : ) } = ClassGroup.mk I
theorem ClassGroup.mk0_surjective {R : Type u_1} [] [] [] :
Function.Surjective ClassGroup.mk0
theorem ClassGroup.mk_eq_one_iff {R : Type u_1} {K : Type u_2} [] [] [Algebra R K] [] [] {I : ()ˣ} :
ClassGroup.mk I = 1
theorem ClassGroup.mk0_eq_one_iff {R : Type u_1} [] [] [] {I : } (hI : I ) :
ClassGroup.mk0 { val := I, property := hI } = 1
noncomputable instance instFintypeClassGroup {R : Type u_1} [] [] :

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.

theorem card_classGroup_eq_one {R : Type u_1} [] [] :
= 1

The class number of a principal ideal domain is 1.

theorem card_classGroup_eq_one_iff {R : Type u_1} [] [] [] [] :

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