mathlib documentation

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 #

Main results #

def to_principal_ideal (R : Type u_1) (K : Type u_2) [comm_ring R] [field K] [algebra R K] [is_fraction_ring R 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] [algebra R K] [is_fraction_ring R K] (x : units K) :
@[simp]
theorem to_principal_ideal_eq_iff {R : Type u_1} {K : Type u_2} [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] {I : units (fractional_ideal R K)} {x : units K} :
@[instance]
def principal_ideals.normal {R : Type u_1} {K : Type u_2} [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] :
def class_group (R : Type u_1) (K : Type u_2) [comm_ring R] [field K] [algebra R K] [is_fraction_ring R 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
@[instance]
def class_group.comm_group (R : Type u_1) (K : Type u_2) [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] :
@[instance]
def class_group.inhabited (R : Type u_1) (K : Type u_2) [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] :
Equations
@[simp]
theorem fractional_ideal.mk0_apply {R : Type u_1} (K : Type u_2) [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] [is_dedekind_domain R] (I : (ideal R)) :
def fractional_ideal.mk0 {R : Type u_1} (K : Type u_2) [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] [is_dedekind_domain R] :

Send a nonzero integral ideal to an invertible fractional ideal.

Equations
def class_group.mk0 {R : Type u_1} (K : Type u_2) [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] [is_dedekind_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] [algebra R K] [is_fraction_ring R K] [is_domain R] [is_dedekind_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} :
(quotient_group.mk' N) x = (quotient_group.mk' N) 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] [algebra R K] [is_fraction_ring R K] [is_domain R] [is_dedekind_domain R] {I J : (ideal R)} :
theorem class_group.mk0_eq_mk0_iff {R : Type u_1} {K : Type u_2} [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] [is_dedekind_domain R] {I J : (ideal R)} :
(class_group.mk0 K) I = (class_group.mk0 K) J ∃ (x y : R) (hx : x 0) (hy : y 0), (ideal.span {x}) * I = (ideal.span {y}) * J
theorem class_group.mk0_eq_one_iff {R : Type u_1} {K : Type u_2} [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] [is_dedekind_domain R] {I : ideal R} (hI : I (ideal R)) :
@[instance]
def class_group.fintype {R : Type u_1} {K : Type u_2} [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] [is_principal_ideal_ring 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] [algebra R K] [is_fraction_ring R K] [is_domain R] [is_principal_ideal_ring R] :

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.