# 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)
@[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
@[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
Instances for class_group
@[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 : (non_zero_divisors (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] (ᾰ : (non_zero_divisors (ideal R))) :
= _)
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))} :
I = J ∃ (x : K) (H : x 0),
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 : (non_zero_divisors (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 : ˣ} :
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 ) :
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.