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.

source

@[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] :

Kˣ →* (fractional_ideal (non_zero_divisors R) K)ˣ

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

Equations

to_principal_ideal R K = {to_fun := λ (x : Kˣ), {val := fractional_ideal.span_singleton (non_zero_divisors R) ↑x, inv := fractional_ideal.span_singleton (non_zero_divisors R) (↑x)⁻¹, val_inv := _, inv_val := _}, map_one' := _, map_mul' := _}

source

@[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ˣ) :

↑(⇑(to_principal_ideal R K) x) = fractional_ideal.span_singleton (non_zero_divisors R) ↑x

source

@[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 : (fractional_ideal (non_zero_divisors R) K)ˣ} {x : Kˣ} :

⇑(to_principal_ideal R K) x = I ↔ fractional_ideal.span_singleton (non_zero_divisors R) ↑x = ↑I

source

theorem mem_principal_ideals_iff {R : Type u_1} {K : Type u_2} [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] {I : (fractional_ideal (non_zero_divisors R) K)ˣ} :

I ∈ (to_principal_ideal R K).range ↔ ∃ (x : K), fractional_ideal.span_singleton (non_zero_divisors R) x = ↑I

source

@[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] :

(to_principal_ideal R K).range.normal

source

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

class_group R = ((fractional_ideal (non_zero_divisors R) (fraction_ring R))ˣ ⧸ (to_principal_ideal R (fraction_ring R)).range)

Instances for class_group

source

@[protected, instance]

noncomputable def class_group.comm_group (R : Type u_1) [comm_ring R] [is_domain R] :

comm_group (class_group R)

source

@[protected, instance]

noncomputable def class_group.inhabited (R : Type u_1) [comm_ring R] [is_domain R] :

inhabited (class_group R)

Equations

class_group.inhabited R = {default := 1}

source

noncomputable def class_group.mk {R : Type u_1} {K : Type u_2} [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] :

(fractional_ideal (non_zero_divisors R) K)ˣ →* class_group R

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

Equations

class_group.mk = (quotient_group.mk' (to_principal_ideal R (fraction_ring R)).range).comp (units.map ↑(fractional_ideal.canonical_equiv (non_zero_divisors R) K (fraction_ring R)))

source

theorem class_group.mk_eq_mk {R : Type u_1} [comm_ring R] [is_domain R] {I J : (fractional_ideal (non_zero_divisors R) (fraction_ring R))ˣ} :

⇑class_group.mk I = ⇑class_group.mk J ↔ ∃ (x : (fraction_ring R)ˣ), I * ⇑(to_principal_ideal R (fraction_ring R)) x = J

source

theorem class_group.mk_eq_mk_of_coe_ideal {R : Type u_1} [comm_ring R] [is_domain R] {I J : (fractional_ideal (non_zero_divisors R) (fraction_ring R))ˣ} {I' J' : ideal R} (hI : ↑I = ↑I') (hJ : ↑J = ↑J') :

⇑class_group.mk I = ⇑class_group.mk J ↔ ∃ (x y : R), x ≠ 0 ∧ y ≠ 0 ∧ ideal.span {x} * I' = ideal.span {y} * J'

source

theorem class_group.mk_eq_one_of_coe_ideal {R : Type u_1} [comm_ring R] [is_domain R] {I : (fractional_ideal (non_zero_divisors R) (fraction_ring R))ˣ} {I' : ideal R} (hI : ↑I = ↑I') :

⇑class_group.mk I = 1 ↔ ∃ (x : R), x ≠ 0 ∧ I' = ideal.span {x}

source

theorem class_group.induction {R : Type u_1} (K : Type u_2) [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] {P : class_group R → Prop} (h : ∀ (I : (fractional_ideal (non_zero_divisors R) K)ˣ), P (⇑class_group.mk I)) (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.

source

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

class_group R ≃* (fractional_ideal (non_zero_divisors R) K)ˣ ⧸ (to_principal_ideal R K).range

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

Equations

class_group.equiv K = quotient_group.congr (to_principal_ideal R (fraction_ring R)).range (to_principal_ideal R K).range (units.map_equiv ↑(fractional_ideal.canonical_equiv (non_zero_divisors R) (fraction_ring R) K)) _

source

@[simp]

theorem class_group.equiv_mk {R : Type u_1} (K : Type u_2) [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] (K' : Type u_3) [field K'] [algebra R K'] [is_fraction_ring R K'] (I : (fractional_ideal (non_zero_divisors R) K)ˣ) :

⇑(class_group.equiv K') (⇑class_group.mk I) = ⇑(quotient_group.mk' (to_principal_ideal R K').range) (⇑(units.map_equiv ↑(fractional_ideal.canonical_equiv (non_zero_divisors R) K K')) I)

source

@[simp]

theorem class_group.mk_canonical_equiv {R : Type u_1} (K : Type u_2) [comm_ring R] [field K] [algebra R K] [is_fraction_ring R K] [is_domain R] (K' : Type u_3) [field K'] [algebra R K'] [is_fraction_ring R K'] (I : (fractional_ideal (non_zero_divisors R) K)ˣ) :

⇑class_group.mk (⇑(units.map ↑(fractional_ideal.canonical_equiv (non_zero_divisors R) K K')) I) = ⇑class_group.mk I

source

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] :

↥(non_zero_divisors (ideal R)) →* (fractional_ideal (non_zero_divisors R) K)ˣ

Send a nonzero integral ideal to an invertible fractional ideal.

Equations

fractional_ideal.mk0 K = {to_fun := λ (I : ↥(non_zero_divisors (ideal R))), units.mk0 ↑I _, map_one' := _, map_mul' := _}

source

@[simp]

theorem fractional_ideal.coe_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] (I : ↥(non_zero_divisors (ideal R))) :

↑(⇑(fractional_ideal.mk0 K) I) = ↑I

source

theorem fractional_ideal.canonical_equiv_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] (K' : Type u_3) [field K'] [algebra R K'] [is_fraction_ring R K'] (I : ↥(non_zero_divisors (ideal R))) :

⇑(fractional_ideal.canonical_equiv (non_zero_divisors R) K K') ↑(⇑(fractional_ideal.mk0 K) I) = ↑(⇑(fractional_ideal.mk0 K') I)

source

@[simp]

theorem fractional_ideal.map_canonical_equiv_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] (K' : Type u_3) [field K'] [algebra R K'] [is_fraction_ring R K'] (I : ↥(non_zero_divisors (ideal R))) :

⇑(units.map ↑(fractional_ideal.canonical_equiv (non_zero_divisors R) K K')) (⇑(fractional_ideal.mk0 K) I) = ⇑(fractional_ideal.mk0 K') I

source

noncomputable def class_group.mk0 {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] :

↥(non_zero_divisors (ideal R)) →* class_group R

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

Equations

class_group.mk0 = class_group.mk.comp (fractional_ideal.mk0 (fraction_ring R))

source

@[simp]

theorem class_group.mk_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] (I : ↥(non_zero_divisors (ideal R))) :

⇑class_group.mk (⇑(fractional_ideal.mk0 K) I) = ⇑class_group.mk0 I

source

@[simp]

theorem class_group.equiv_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] (I : ↥(non_zero_divisors (ideal R))) :

⇑(class_group.equiv K) (⇑class_group.mk0 I) = ⇑(quotient_group.mk' (to_principal_ideal R K).range) (⇑(fractional_ideal.mk0 K) I)

source

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 : ↥(non_zero_divisors (ideal R))} :

⇑class_group.mk0 I = ⇑class_group.mk0 J ↔ ∃ (x : K) (H : x ≠ 0), fractional_ideal.span_singleton (non_zero_divisors R) x * ↑I = ↑J

source

theorem class_group.mk0_eq_mk0_iff {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] {I J : ↥(non_zero_divisors (ideal R))} :

⇑class_group.mk0 I = ⇑class_group.mk0 J ↔ ∃ (x y : R) (hx : x ≠ 0) (hy : y ≠ 0), ideal.span {x} * ↑I = ideal.span {y} * ↑J

source

theorem class_group.mk0_surjective {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] :

function.surjective ⇑class_group.mk0

source

theorem class_group.mk_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] {I : (fractional_ideal (non_zero_divisors R) K)ˣ} :

⇑class_group.mk I = 1 ↔ ↑I.is_principal

source

theorem class_group.mk0_eq_one_iff {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] {I : ideal R} (hI : I ∈ non_zero_divisors (ideal R)) :

⇑class_group.mk0 ⟨I, hI⟩ = 1 ↔ submodule.is_principal I

source

@[protected, instance]

noncomputable def class_group.fintype {R : Type u_1} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] :

fintype (class_group 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

class_group.fintype = {elems := {1}, complete := _}

source

theorem card_class_group_eq_one {R : Type u_1} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] :

fintype.card (class_group R) = 1

The class number of a principal ideal domain is 1.

source

theorem card_class_group_eq_one_iff {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] [fintype (class_group R)] :

fintype.card (class_group R) = 1 ↔ is_principal_ideal_ring R

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