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

@[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

Equations
Instances For
theorem toPrincipalIdeal_def (R : Type u_4) (K : Type u_5) [] [] [Algebra R K] [] :
= { toFun := fun (x : Kˣ) => { val := , inv := , val_inv := , inv_val := }, map_one' := , map_mul' := }
@[simp]
theorem coe_toPrincipalIdeal {R : Type u_1} {K : Type u_2} [] [] [Algebra R K] [] (x : Kˣ) :
((toPrincipalIdeal R K) x) =
@[simp]
theorem toPrincipalIdeal_eq_iff {R : Type u_1} {K : Type u_2} [] [] [Algebra R K] [] {I : ˣ} {x : Kˣ} :
theorem mem_principal_ideals_iff {R : Type u_1} {K : Type u_2} [] [] [Algebra R K] [] {I : ˣ} :
I (toPrincipalIdeal R K).range ∃ (x : K),
instance PrincipalIdeals.normal {R : Type u_1} {K : Type u_2} [] [] [Algebra R K] [] :
(toPrincipalIdeal R K).range.Normal
Equations
• =
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.

Equations
Instances For
noncomputable instance instCommGroupClassGroup (R : Type u_1) [] [] :
Equations
noncomputable instance instInhabitedClassGroup (R : Type u_1) [] [] :
Equations
• = { default := 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.

Equations
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 : (FractionRing R)ˣ), I * (toPrincipalIdeal R (FractionRing R)) 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 : 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} [] [] {I : ˣ} {I' : } (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) [] [] [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.

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) [] [] [Algebra R K] [] [] (K' : Type u_4) [Field K'] [Algebra R K'] [] (I : ˣ) :
(ClassGroup.equiv K') (ClassGroup.mk I) = (QuotientGroup.mk' (toPrincipalIdeal R K').range) ((Units.mapEquiv ) 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 ((Units.map ) 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.

Equations
• = { toFun := fun (I : { x : // x }) => Units.mk0 I , map_one' := , map_mul' := }
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 }) :
(Units.map ) ( I) = I
noncomputable def ClassGroup.mk0 {R : Type u_1} [] [] [] :
{ x : // x } →*

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

Equations
• ClassGroup.mk0 = ClassGroup.mk.comp
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) = (QuotientGroup.mk' (toPrincipalIdeal R K).range) ( 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 : K) (_ : x 0), = J
theorem ClassGroup.mk0_eq_mk0_iff {R : Type u_1} [] [] [] {I : { x : // x }} {J : { x : // x }} :
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} [] (I : ) :

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

Equations
• = I.num
Instances For
theorem ClassGroup.integralRep_mem_nonZeroDivisors {R : Type u_1} [] [] {I : } (hI : I 0) :
I.num
theorem ClassGroup.mk0_integralRep {R : Type u_1} [] [] [] (I : ˣ) :
ClassGroup.mk0 , = 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 (↑I).IsPrincipal
theorem ClassGroup.mk0_eq_one_iff {R : Type u_1} [] [] [] {I : } (hI : I ) :
ClassGroup.mk0 I, hI = 1
theorem ClassGroup.mk0_eq_mk0_inv_iff {R : Type u_1} [] [] [] {I : { x : // x }} {J : { x : // x }} :
ClassGroup.mk0 I = (ClassGroup.mk0 J)⁻¹ ∃ (x : R), x 0 I * J = Ideal.span {x}
noncomputable instance instFintypeClassGroupOfIsPrincipalIdealRing {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.

Equations
• instFintypeClassGroupOfIsPrincipalIdealRing = { elems := {1}, complete := }
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.