Ideal class group

TheoremMaking an ideal principal with a factor coprime to a given ideal#✓fully proved

Let \(A\) be a Dedekind domain and let \(I\) and \(\mathfrak{a}\) be nonzero ideals of \(A\). Then there is an ideal \(J\) of \(A\) with \(J + \mathfrak{a} = A\) such that the product \(IJ\) is a principal ideal.

theorem Ideal.exists_isCoprime_mul_isPrincipal (I a : Ideal A) (hI : I ≠ ⊥)
    (ha : a ≠ ⊥) :
    ∃ J : Ideal A, IsCoprime J a ∧ Submodule.IsPrincipal (I * J)

Used by 1

Used byIdeal classes have representatives coprime to a given ideal

TheoremIdeal classes have representatives coprime to a given ideal#✓fully proved

Let \(A\) be a Dedekind domain and let \(\mathfrak{a}\) be a nonzero ideal of \(A\). Then every class \(c\) in the ideal class group of \(A\) is the class of some nonzero ideal \(K\) of \(A\) with \(K + \mathfrak{a} = A\).

theorem ClassGroup.exists_mk0_eq_and_isCoprime (c : ClassGroup A) (a : Ideal A)
    (ha : a ≠ ⊥) :
    ∃ (K : Ideal A) (hK : K ≠ ⊥),
      ClassGroup.mk0 ⟨K, mem_nonZeroDivisors_iff_ne_zero.mpr hK⟩ = c ∧
        IsCoprime K a

Uses 1 · Used by 1

Proof usesMaking an ideal principal with a factor coprime to a given ideal

Used byEvery ideal class contains a fractional ideal coprime to the modulus

AbbreviationSimilar ideals#✓fully proved

Let \(R\) be a Dedekind domain. Two nonzero ideals \(I\) and \(J\) of \(R\) are similar when their classes in the ideal class group of \(R\) are equal.

abbrev IdealsSimilar (I J : (Ideal R)⁰) : Prop := ClassGroup.mk0 I = ClassGroup.mk0 J

TheoremDedekind domains: UFD iff PID#✓fully proved

A Dedekind domain \(R\) is a unique factorization domain if and only if it is a principal ideal domain.

theorem uniqueFactorizationMonoid_iff_isPrincipalIdealRing :
    UniqueFactorizationMonoid R ↔ IsPrincipalIdealRing R

Sources

ATLAS NumberTheoryI, Section 3.2, Corollary 3.15 (first equivalence).

Used by 1

Used byDedekind domains: UFD iff trivial class group

TheoremDedekind domains: PID iff trivial class group#✓fully proved

A Dedekind domain \(R\) is a principal ideal domain if and only if its ideal class group is trivial.

theorem isPrincipalIdealRing_iff_subsingleton_classGroup :
    IsPrincipalIdealRing R ↔ Subsingleton (ClassGroup R)

Sources

ATLAS NumberTheoryI, Section 3.2, Corollary 3.15 (second equivalence).

Used by 1

Used byDedekind domains: UFD iff trivial class group

TheoremDedekind domains: UFD iff trivial class group#✓fully proved

A Dedekind domain \(R\) is a unique factorization domain if and only if its ideal class group is trivial.

theorem uniqueFactorizationMonoid_iff_subsingleton_classGroup :
    UniqueFactorizationMonoid R ↔ Subsingleton (ClassGroup R)

Sources

ATLAS NumberTheoryI, Section 3.2, Corollary 3.15 (combined).

Uses 2

Proof usesDedekind domains: PID iff trivial class group · Dedekind domains: UFD iff PID

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.