# mathlib3documentation

ring_theory.class_group

# The ideal class group #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Main definitions #

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

## Main results #

• class_group.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 class_group R involves fraction_ring R. However, the API should be completely identical no matter the choice of field of fractions for R.

@[irreducible]
def to_principal_ideal (R : Type u_1) (K : Type u_2) [comm_ring R] [field K] [ K] [ K] :

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

Equations
@[simp]
theorem coe_to_principal_ideal {R : Type u_1} {K : Type u_2} [comm_ring R] [field K] [ K] [ K] (x : Kˣ) :
@[simp]
theorem to_principal_ideal_eq_iff {R : Type u_1} {K : Type u_2} [comm_ring R] [field K] [ K] [ K] {I : ˣ} {x : Kˣ} :
K) x = I
theorem mem_principal_ideals_iff {R : Type u_1} {K : Type u_2} [comm_ring R] [field K] [ K] [ K] {I : ˣ} :
I K).range (x : K),
@[protected, instance]
def principal_ideals.normal {R : Type u_1} {K : Type u_2} [comm_ring R] [field K] [ K] [ K] :
def class_group (R : Type u_1) [comm_ring R] [is_domain R] :
Type u_1

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

Equations
Instances for class_group
@[protected, instance]
noncomputable def class_group.comm_group (R : Type u_1) [comm_ring R] [is_domain R] :
@[protected, instance]
noncomputable def class_group.inhabited (R : Type u_1) [comm_ring R] [is_domain R] :
Equations
noncomputable def class_group.mk {R : Type u_1} {K : Type u_2} [comm_ring R] [field K] [ K] [ K] [is_domain R] :

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

Equations
theorem class_group.mk_eq_mk {R : Type u_1} [comm_ring R] [is_domain R] {I J : ˣ} :
(x : ˣ), I * (fraction_ring R)) x = J
theorem class_group.mk_eq_mk_of_coe_ideal {R : Type u_1} [comm_ring R] [is_domain R] {I J : ˣ} {I' J' : ideal R} (hI : I = I') (hJ : J = J') :
(x y : R), x 0 y 0 ideal.span {x} * I' = ideal.span {y} * J'
theorem class_group.mk_eq_one_of_coe_ideal {R : Type u_1} [comm_ring R] [is_domain R] {I : ˣ} {I' : ideal R} (hI : I = I') :
(x : R), x 0 I' = ideal.span {x}
theorem class_group.induction {R : Type u_1} (K : Type u_2) [comm_ring R] [field K] [ K] [ K] [is_domain R] {P : Prop} (h : (I : ˣ), P ) (x : class_group R) :
P x

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

noncomputable def class_group.equiv {R : Type u_1} (K : Type u_2) [comm_ring R] [field K] [ K] [ K] [is_domain R] :

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

Equations
@[simp]
theorem class_group.equiv_mk {R : Type u_1} (K : Type u_2) [comm_ring R] [field K] [ K] [ K] [is_domain R] (K' : Type u_3) [field K'] [ K'] [ K'] (I : ˣ) :
= I)
@[simp]
theorem class_group.mk_canonical_equiv {R : Type u_1} (K : Type u_2) [comm_ring R] [field K] [ K] [ K] [is_domain R] (K' : Type u_3) [field K'] [ K'] [ K'] (I : ˣ) :
noncomputable def fractional_ideal.mk0 {R : Type u_1} (K : Type u_2) [comm_ring R] [field K] [ K] [ K] [is_domain R]  :

Send a nonzero integral ideal to an invertible fractional ideal.

Equations
@[simp]
theorem fractional_ideal.coe_mk0 {R : Type u_1} (K : Type u_2) [comm_ring R] [field K] [ K] [ K] [is_domain R] (I : (non_zero_divisors (ideal R))) :
I) = I
theorem fractional_ideal.canonical_equiv_mk0 {R : Type u_1} (K : Type u_2) [comm_ring R] [field K] [ K] [ K] [is_domain R] (K' : Type u_3) [field K'] [ K'] [ K'] (I : (non_zero_divisors (ideal R))) :
I) = ( I)
@[simp]
theorem fractional_ideal.map_canonical_equiv_mk0 {R : Type u_1} (K : Type u_2) [comm_ring R] [field K] [ K] [ K] [is_domain R] (K' : Type u_3) [field K'] [ K'] [ K'] (I : (non_zero_divisors (ideal R))) :
I) = I
noncomputable def class_group.mk0 {R : Type u_1} [comm_ring R] [is_domain R]  :

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

Equations
@[simp]
theorem class_group.mk_mk0 {R : Type u_1} (K : Type u_2) [comm_ring R] [field K] [ K] [ K] [is_domain R] (I : (non_zero_divisors (ideal R))) :
@[simp]
theorem class_group.equiv_mk0 {R : Type u_1} (K : Type u_2) [comm_ring R] [field K] [ K] [ K] [is_domain R] (I : (non_zero_divisors (ideal R))) :
= I)
theorem class_group.mk0_eq_mk0_iff_exists_fraction_ring {R : Type u_1} (K : Type u_2) [comm_ring R] [field K] [ K] [ K] [is_domain R] {I J : (non_zero_divisors (ideal R))} :
(x : K) (H : x 0),
theorem class_group.mk0_eq_mk0_iff {R : Type u_1} [comm_ring R] [is_domain R] {I J : (non_zero_divisors (ideal R))} :
(x y : R) (hx : x 0) (hy : y 0), ideal.span {x} * I = ideal.span {y} * J
theorem class_group.mk0_surjective {R : Type u_1} [comm_ring R] [is_domain R]  :
theorem class_group.mk_eq_one_iff {R : Type u_1} {K : Type u_2} [comm_ring R] [field K] [ K] [ K] [is_domain R] {I : ˣ} :
theorem class_group.mk0_eq_one_iff {R : Type u_1} [comm_ring R] [is_domain R] {I : ideal R} (hI : I ) :
@[protected, instance]
noncomputable def class_group.fintype {R : Type u_1} [comm_ring R] [is_domain R]  :

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

See class_group.fintype_of_admissible for a finiteness proof that works for rings of integers of global fields.

Equations
theorem card_class_group_eq_one {R : Type u_1} [comm_ring R] [is_domain R]  :
= 1

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.