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 #

@[irreducible]
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 : Kˣ) :
@[simp]
@[protected, 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
Instances for class_group
@[protected, 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] :
@[protected, 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 : (non_zero_divisors (ideal R))) :
noncomputable 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
noncomputable 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] (ᾰ : (non_zero_divisors (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 : (non_zero_divisors (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 non_zero_divisors (ideal R)) :
@[protected, 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.