# mathlibdocumentation

ring_theory.class_group

# The ideal class group #

This file defines the ideal class group class_group R K of fractional ideals of R inside A's field of fractions K.

## 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)
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ˣ) :
( K) x) =
@[simp]
theorem to_principal_ideal_eq_iff {R : Type u_1} {K : Type u_2} [comm_ring R] [field K] [ K] [ K] {I : K)ˣ} {x : Kˣ} :
K) x = I
@[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) (K : Type u_2) [comm_ring R] [field K] [ K] [ K] :
Type u_2

The ideal class group of R in a field of fractions K is the group of invertible fractional ideals modulo the principal ideals.

Equations
@[protected, instance]
def class_group.comm_group (R : Type u_1) (K : Type u_2) [comm_ring R] [field K] [ K] [ K] :
@[protected, instance]
def class_group.inhabited (R : Type u_1) (K : Type u_2) [comm_ring R] [field K] [ K] [ K] :
Equations
@[simp]
theorem fractional_ideal.mk0_apply {R : Type u_1} (K : Type u_2) [comm_ring R] [field K] [ K] [ K] [is_domain R] (I : (ideal R)) :
= _
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
noncomputable def class_group.mk0 {R : Type u_1} (K : Type u_2) [comm_ring R] [field K] [ K] [ K] [is_domain R]  :

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

Equations
@[simp]
theorem class_group.mk0_apply {R : Type u_1} (K : Type u_2) [comm_ring R] [field K] [ K] [ K] [is_domain R] (ᾰ : (ideal R)) :
= _)
theorem quotient_group.mk'_eq_mk' {G : Type u_1} [group G] {N : subgroup G} [hN : N.normal] {x y : G} :
x = y ∃ (z : G) (H : z N), x * z = y
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 : (ideal R)} :
I = J ∃ (x : K) (H : x 0), = J
theorem class_group.mk0_eq_mk0_iff {R : Type u_1} {K : Type u_2} [comm_ring R] [field K] [ K] [ K] [is_domain R] {I J : (ideal R)} :
I = J ∃ (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} {K : Type u_2} [comm_ring R] [field K] [ K] [ K] [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] {I : K)ˣ} :
theorem class_group.mk0_eq_one_iff {R : Type u_1} {K : Type u_2} [comm_ring R] [field K] [ K] [ K] [is_domain R] {I : ideal R} (hI : I (ideal R)) :
I, hI⟩ = 1
@[protected, instance]
def class_group.fintype {R : Type u_1} {K : Type u_2} [comm_ring R] [field K] [ K] [ K] [is_domain R]  :

The class group of principal ideal domain is finite (in fact a singleton). TODO: generalize to Dedekind domains

Equations
theorem card_class_group_eq_one {R : Type u_1} {K : Type u_2} [comm_ring R] [field K] [ K] [ K] [is_domain R]  :

The class number of a principal ideal domain is 1.

theorem card_class_group_eq_one_iff {R : Type u_1} {K : Type u_2} [comm_ring R] [field K] [ K] [ K] [is_domain R] [fintype K)] :

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