The ideal class group #
This file defines the ideal class group
class_group R K of fractional ideals of
A's field of fractions
Main definitions #
to_principal_idealsends an invertible
x : Kto an invertible fractional ideal
class_groupis the quotient of invertible fractional ideals modulo
class_group.mk0sends a nonzero integral ideal in a Dedekind domain to its class
Main results #
class_group.mk0_eq_mk0_iffshows the equivalence with the "classical" definition, where
I ~ Jiff
x I = y Jfor
x y ≠ (0 : R)
to_principal_ideal R K x sends
x ≠ 0 : K to the fractional
R-ideal generated by
The ideal class group of
R in a field of fractions
is the group of invertible fractional ideals modulo the principal ideals.
Send a nonzero integral ideal to an invertible fractional ideal.
Send a nonzero ideal to the corresponding class in the class group.
The class group of principal ideal domain is finite (in fact a singleton). TODO: generalize to Dedekind domains
The class number is
1 iff the ring of integers is a principal ideal domain.