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 invertiblex : K
to an invertible fractional idealclass_group
is the quotient of invertible fractional ideals moduloto_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, whereI ~ J
iffx I = y J
forx y ≠ (0 : R)
@[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' := _}
@[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
@[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
@[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
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 (non_zero_divisors R) K)ˣ ⧸ (to_principal_ideal R K).range)
@[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)
@[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}
@[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))) :
⇑(fractional_ideal.mk0 K) I = units.mk0 ↑I _
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.
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] :
↥(non_zero_divisors (ideal R)) →* class_group R K
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_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 K) I = ⇑(class_group.mk0 K) J ↔ ∃ (x : K) (H : x ≠ 0), fractional_ideal.span_singleton (non_zero_divisors R) x * ↑I = ↑J
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_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] :
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 (non_zero_divisors R) K)ˣ} :
⇑(quotient_group.mk' (to_principal_ideal R K).range) I = 1 ↔ ↑I.is_principal
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)) :
⇑(class_group.mk0 K) ⟨I, hI⟩ = 1 ↔ submodule.is_principal I
@[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 := _}
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
.
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.