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)

source

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 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 R⁰ ↑x, inv := fractional_ideal.span_singleton 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 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 R⁰ K)ˣ} {x : Kˣ} :

⇑(to_principal_ideal R K) x = I ↔ fractional_ideal.span_singleton 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) (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

class_group R K = ((fractional_ideal R⁰ K)ˣ ⧸ (to_principal_ideal R K).range)

source

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

comm_group (class_group R K)

source

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

inhabited (class_group R K)

Equations

class_group.inhabited R K = {default := 1}

source

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

⇑(fractional_ideal.mk0 K) I = units.mk0 ↑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] :

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

Send a nonzero integral ideal to an invertible fractional ideal.

Equations

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

source

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

↥(ideal R)⁰ →* class_group R K

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

Equations

class_group.mk0 K = (quotient_group.mk' (to_principal_ideal R K).range).comp (fractional_ideal.mk0 K)

source

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

⇑(class_group.mk0 K) ᾰ = ↑(units.mk0 ↑↑ᾰ _)

source

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

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

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

source

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

source

theorem class_group.mk0_surjective {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] :

function.surjective ⇑(class_group.mk0 K)

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] {I : (fractional_ideal R⁰ K)ˣ} :

⇑(quotient_group.mk' (to_principal_ideal R K).range) I = 1 ↔ ↑I.is_principal

source

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)⁰) :

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

source

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

fintype (class_group R K)

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

Equations

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

source

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

fintype.card (class_group R K) = 1

The class number of a principal ideal domain is 1.

source

theorem card_class_group_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] [fintype (class_group R K)] :

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

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