The ideal class group

This file defines the ideal class group ClassGroup R of fractional ideals of R inside its field of fractions.

Main definitions

• toPrincipalIdeal sends an invertible x : K to an invertible fractional ideal
• ClassGroup is the quotient of invertible fractional ideals modulo toPrincipalIdeal.range
• ClassGroup.mk0 sends a nonzero integral ideal in a Dedekind domain to its class

Main results

• ClassGroup.mk0_eq_mk0_iff shows the equivalence with the "classical" definition, where I ~ J iff x I = y J for x y ≠ (0 : R)
• ClassGroup.mk0_eq_quotientMk identifies ClassGroup.mk0 with the canonical quotient projection on (FractionalIdeal R⁰ (FractionRing R))ˣ

Implementation details

The definition of ClassGroup R involves FractionRing R. However, the API should be completely identical no matter the choice of field of fractions for R.

@[irreducible]

def toPrincipalIdeal (R : Type u_3) (K : Type u_4) [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] : Kˣ →* (FractionalIdeal (nonZeroDivisors R) K)ˣ

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

Equations

• One or more equations did not get rendered due to their size.

theorem toPrincipalIdeal_def (R : Type u_3) (K : Type u_4) [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] : toPrincipalIdeal R K = { toFun := fun (x : Kˣ) => { val := FractionalIdeal.spanSingleton (nonZeroDivisors R) ↑x, inv := FractionalIdeal.spanSingleton (nonZeroDivisors R) (↑x)⁻¹, val_inv := ⋯, inv_val := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem coe_toPrincipalIdeal {R : Type u_1} {K : Type u_2} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] (x : Kˣ) : ↑((toPrincipalIdeal R K) x) = FractionalIdeal.spanSingleton (nonZeroDivisors R) ↑x

@[simp]

theorem toPrincipalIdeal_eq_iff {R : Type u_1} {K : Type u_2} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] {I : (FractionalIdeal (nonZeroDivisors R) K)ˣ} {x : Kˣ} : (toPrincipalIdeal R K) x = I ↔ FractionalIdeal.spanSingleton (nonZeroDivisors R) ↑x = ↑I

theorem mem_principal_ideals_iff {R : Type u_1} {K : Type u_2} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] {I : (FractionalIdeal (nonZeroDivisors R) K)ˣ} : I ∈ (toPrincipalIdeal R K).range ↔ ∃ (x : K), FractionalIdeal.spanSingleton (nonZeroDivisors R) x = ↑I

instance PrincipalIdeals.normal {R : Type u_1} {K : Type u_2} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] : (toPrincipalIdeal R K).range.Normal

def ClassGroup (R : Type u_1) [CommRing R] [IsDomain R] : Type u_1

The ideal class group of R is the group of invertible fractional ideals modulo the principal ideals.

Equations

• ClassGroup R = ((FractionalIdeal (nonZeroDivisors R) (FractionRing R))ˣ ⧸ (toPrincipalIdeal R (FractionRing R)).range)

@[instance_reducible]

noncomputable instance instCommGroupClassGroup (R : Type u_1) [CommRing R] [IsDomain R] : CommGroup (ClassGroup R)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance instInhabitedClassGroup (R : Type u_1) [CommRing R] [IsDomain R] : Inhabited (ClassGroup R)

Equations

• instInhabitedClassGroup R = { default := instInhabitedClassGroup._aux_1 R }

noncomputable def ClassGroup.mulEquivUnitsSubmoduleQuotRange (R : Type u_1) [CommRing R] [IsDomain R] : ClassGroup R ≃* (Submodule R (FractionRing R))ˣ ⧸ (Units.map ↑(Submodule.spanSingleton R)).range

The class group of R is isomorphic to the group of invertible R-submodules in Frac(R) modulo the principal submodules (invertible submodules are automatically fractional ideals).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ClassGroup.mk {R : Type u_1} (K : Type u_2) [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] : (FractionalIdeal (nonZeroDivisors R) K)ˣ →* ClassGroup R

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

Equations

• ClassGroup.mk K = (QuotientGroup.mk' (toPrincipalIdeal R (FractionRing R)).range).comp (Units.map ↑(FractionalIdeal.canonicalEquiv (nonZeroDivisors R) K (FractionRing R)))

theorem ClassGroup.mk_def {R : Type u_1} {K : Type u_2} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ) : (mk K) I = (QuotientGroup.mk' (toPrincipalIdeal R (FractionRing R)).range) ((Units.map ↑(FractionalIdeal.canonicalEquiv (nonZeroDivisors R) K (FractionRing R))) I)

theorem ClassGroup.Quot_mk_eq_mk {R : Type u_1} [CommRing R] [IsDomain R] (I : (FractionalIdeal (nonZeroDivisors R) (FractionRing R))ˣ) : Quot.mk (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range)) I = (mk (FractionRing R)) I

theorem ClassGroup.mk_eq_mk {R : Type u_1} [CommRing R] [IsDomain R] {I J : (FractionalIdeal (nonZeroDivisors R) (FractionRing R))ˣ} : (mk (FractionRing R)) I = (mk (FractionRing R)) J ↔ ∃ (x : (FractionRing R)ˣ), I * (toPrincipalIdeal R (FractionRing R)) x = J

theorem ClassGroup.mk_eq_mk_of_coe_ideal {R : Type u_1} [CommRing R] [IsDomain R] {I J : (FractionalIdeal (nonZeroDivisors R) (FractionRing R))ˣ} {I' J' : Ideal R} (hI : ↑I = ↑I') (hJ : ↑J = ↑J') : (mk (FractionRing R)) I = (mk (FractionRing R)) J ↔ ∃ (x : R) (y : R), x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J'

theorem ClassGroup.mk_eq_one_of_coe_ideal {R : Type u_1} [CommRing R] [IsDomain R] {I : (FractionalIdeal (nonZeroDivisors R) (FractionRing R))ˣ} {I' : Ideal R} (hI : ↑I = ↑I') : (mk (FractionRing R)) I = 1 ↔ ∃ (x : R), x ≠ 0 ∧ I' = Ideal.span {x}

theorem ClassGroup.induction {R : Type u_1} (K : Type u_2) [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] {P : ClassGroup R → Prop} (h : ∀ (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ), P ((mk K) I)) (x : ClassGroup R) : P x

Induction principle for the class group: to show something holds for all x : ClassGroup R, we can choose a fraction field K and show it holds for the equivalence class of each I : FractionalIdeal R⁰ K.

noncomputable def ClassGroup.equiv {R : Type u_1} (K : Type u_2) [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] : ClassGroup R ≃* (FractionalIdeal (nonZeroDivisors R) K)ˣ ⧸ (toPrincipalIdeal R K).range

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ClassGroup.equiv_mk {R : Type u_1} (K : Type u_2) [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] (K' : Type u_3) [Field K'] [Algebra R K'] [IsFractionRing R K'] (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ) : (equiv K') ((mk K) I) = (QuotientGroup.mk' (toPrincipalIdeal R K').range) ((Units.mapEquiv ↑(FractionalIdeal.canonicalEquiv (nonZeroDivisors R) K K')) I)

@[simp]

theorem ClassGroup.mk_canonicalEquiv {R : Type u_1} (K : Type u_2) [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] (K' : Type u_3) [Field K'] [Algebra R K'] [IsFractionRing R K'] (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ) : (mk K') ((Units.map ↑(FractionalIdeal.canonicalEquiv (nonZeroDivisors R) K K')) I) = (mk K) I

noncomputable def FractionalIdeal.mk0 {R : Type u_1} (K : Type u_2) [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] [IsDedekindDomain R] : ↥(nonZeroDivisors (Ideal R)) →* (FractionalIdeal (nonZeroDivisors R) K)ˣ

Send a nonzero integral ideal to an invertible fractional ideal.

Equations

• FractionalIdeal.mk0 K = { toFun := fun (I : ↥(nonZeroDivisors (Ideal R))) => Units.mk0 ↑↑I ⋯, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem FractionalIdeal.coe_mk0 {R : Type u_1} (K : Type u_2) [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] [IsDedekindDomain R] (I : ↥(nonZeroDivisors (Ideal R))) : ↑((mk0 K) I) = ↑↑I

theorem FractionalIdeal.canonicalEquiv_mk0 {R : Type u_1} (K : Type u_2) [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] [IsDedekindDomain R] (K' : Type u_3) [Field K'] [Algebra R K'] [IsFractionRing R K'] (I : ↥(nonZeroDivisors (Ideal R))) : (canonicalEquiv (nonZeroDivisors R) K K') ↑((mk0 K) I) = ↑((mk0 K') I)

@[simp]

theorem FractionalIdeal.map_canonicalEquiv_mk0 {R : Type u_1} (K : Type u_2) [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] [IsDedekindDomain R] (K' : Type u_3) [Field K'] [Algebra R K'] [IsFractionRing R K'] (I : ↥(nonZeroDivisors (Ideal R))) : (Units.map ↑(canonicalEquiv (nonZeroDivisors R) K K')) ((mk0 K) I) = (mk0 K') I

noncomputable def ClassGroup.mk0 {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] : ↥(nonZeroDivisors (Ideal R)) →* ClassGroup R

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

Equations

• ClassGroup.mk0 = (ClassGroup.mk (FractionRing R)).comp (FractionalIdeal.mk0 (FractionRing R))

@[simp]

theorem ClassGroup.mk_mk0 {R : Type u_1} (K : Type u_2) [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] [IsDedekindDomain R] (I : ↥(nonZeroDivisors (Ideal R))) : (mk K) ((FractionalIdeal.mk0 K) I) = mk0 I

theorem ClassGroup.mk0_eq_quotientMk {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] (I : ↥(nonZeroDivisors (Ideal R))) : mk0 I = ↑((FractionalIdeal.mk0 (FractionRing R)) I)

ClassGroup.mk0 factors through the canonical quotient projection on (FractionalIdeal R⁰ (FractionRing R))ˣ.

@[simp]

theorem ClassGroup.equiv_mk0 {R : Type u_1} (K : Type u_2) [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] [IsDedekindDomain R] (I : ↥(nonZeroDivisors (Ideal R))) : (equiv K) (mk0 I) = (QuotientGroup.mk' (toPrincipalIdeal R K).range) ((FractionalIdeal.mk0 K) I)

theorem ClassGroup.mk0_eq_mk0_iff_exists_fraction_ring {R : Type u_1} (K : Type u_2) [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] [IsDedekindDomain R] {I J : ↥(nonZeroDivisors (Ideal R))} : mk0 I = mk0 J ↔ ∃ (x : K) (_ : x ≠ 0), FractionalIdeal.spanSingleton (nonZeroDivisors R) x * ↑↑I = ↑↑J

theorem ClassGroup.mk0_eq_mk0_iff {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] {I J : ↥(nonZeroDivisors (Ideal R))} : mk0 I = mk0 J ↔ ∃ (x : R) (y : R) (_ : x ≠ 0) (_ : y ≠ 0), Ideal.span {x} * ↑I = Ideal.span {y} * ↑J

theorem FractionalIdeal.isUnit_num {R : Type u_1} [CommRing R] [IsDomain R] {I : FractionalIdeal (nonZeroDivisors R) (FractionRing R)} : IsUnit ↑I.num ↔ IsUnit I

A fractional ideal is a unit iff its integral numerator num is a unit.

noncomputable def ClassGroup.integralRep {R : Type u_1} [CommRing R] (I : FractionalIdeal (nonZeroDivisors R) (FractionRing R)) : Ideal R

Maps a nonzero fractional ideal to an integral representative in the class group.

Equations

• ClassGroup.integralRep I = I.num

theorem ClassGroup.integralRep_mem_nonZeroDivisors {R : Type u_1} [CommRing R] [IsDomain R] {I : FractionalIdeal (nonZeroDivisors R) (FractionRing R)} (hI : I ≠ 0) : I.num ∈ nonZeroDivisors (Ideal R)

theorem ClassGroup.mk0_integralRep {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] (I : (FractionalIdeal (nonZeroDivisors R) (FractionRing R))ˣ) : mk0 ⟨integralRep ↑I, ⋯⟩ = (mk (FractionRing R)) I

theorem ClassGroup.mk0_surjective {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] : Function.Surjective ⇑mk0

theorem ClassGroup.mk_eq_one_iff {R : Type u_1} {K : Type u_2} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] {I : (FractionalIdeal (nonZeroDivisors R) K)ˣ} : (mk K) I = 1 ↔ (↑↑I).IsPrincipal

theorem FractionalIdeal.isPrincipal.of_isPrincipal_pow_of_coprime {R : Type u_1} {K : Type u_2} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] [IsDedekindDomain R] [Fintype (ClassGroup R)] {n : ℕ} (hn : n.Coprime (Fintype.card (ClassGroup R))) (I : FractionalIdeal (nonZeroDivisors R) K) (hI : (↑(I ^ n)).IsPrincipal) : (↑I).IsPrincipal

A fractional ideal is principal if a power coprime to the class number is principal.

theorem ClassGroup.isPrincipal_coeSubmodule_of_isUnit {R : Type u_1} {K : Type u_2} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] [Subsingleton (ClassGroup R)] (I : FractionalIdeal (nonZeroDivisors R) K) (hI : IsUnit I) : (↑I).IsPrincipal

If the class group is trivial, any unit fractional ideal is principal.

theorem ClassGroup.isPrincipal_of_isUnit_coeIdeal {R : Type u_1} {K : Type u_2} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] [Subsingleton (ClassGroup R)] (I : Ideal R) (hI : IsUnit ↑I) : Submodule.IsPrincipal I

If the class group is trivial, any integral ideal that is a unit as a fractional ideal is principal.

theorem ClassGroup.mk0_eq_one_iff {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] {I : Ideal R} (hI : I ∈ nonZeroDivisors (Ideal R)) : mk0 ⟨I, hI⟩ = 1 ↔ Submodule.IsPrincipal I

theorem Ideal.IsPrincipal.of_isPrincipal_pow_of_coprime {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] [Fintype (ClassGroup R)] {n : ℕ} (hn : n.Coprime (Fintype.card (ClassGroup R))) {I : Ideal R} (hI : Submodule.IsPrincipal (I ^ n)) : Submodule.IsPrincipal I

An ideal is principal if a power coprime to the class number is principal.

theorem ClassGroup.mk0_eq_mk0_inv_iff {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] {I J : ↥(nonZeroDivisors (Ideal R))} : mk0 I = (mk0 J)⁻¹ ↔ ∃ (x : R), x ≠ 0 ∧ ↑I * ↑J = Ideal.span {x}

@[instance_reducible]

noncomputable instance instFintypeClassGroupOfIsPrincipalIdealRing {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] : Fintype (ClassGroup R)

The class group of principal ideal domain is finite (in fact a singleton).

See ClassGroup.fintypeOfAdmissibleOfFinite for a finiteness proof that works for rings of integers of global fields.

Equations

• instFintypeClassGroupOfIsPrincipalIdealRing = { elems := {1}, complete := ⋯ }

theorem card_classGroup_eq_one {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] : Fintype.card (ClassGroup R) = 1

The class number of a principal ideal domain is 1.

theorem card_classGroup_eq_one_iff {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] [Fintype (ClassGroup R)] : Fintype.card (ClassGroup R) = 1 ↔ IsPrincipalIdealRing R

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

theorem FractionalIdeal.map_ringEquivOfRingEquiv_toPrincipalIdeal {R : Type u_1} {K : Type u_2} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] {S : Type u_3} {L : Type u_4} [CommRing S] [IsDomain S] [Field L] [Algebra S L] [IsFractionRing S L] (f : R ≃+* S) : Subgroup.map (Units.mapEquiv ↑(ringEquivOfRingEquiv K L f)).toMonoidHom (toPrincipalIdeal R K).range = (toPrincipalIdeal S L).range

noncomputable def ClassGroup.mulEquiv {R : Type u_1} [CommRing R] [IsDomain R] {R' : Type u_3} [CommRing R'] [IsDomain R'] (g : R ≃+* R') : ClassGroup R ≃* ClassGroup R'

A ring isomorphism R ≃+* R' induces an isomorphism on their class groups.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ClassGroup.mulEquiv_symm_apply {R : Type u_1} [CommRing R] [IsDomain R] {R' : Type u_3} [CommRing R'] [IsDomain R'] (g : R ≃+* R') (a✝ : ClassGroup R') : (mulEquiv g).symm a✝ = (equiv (FractionRing R)).symm ((QuotientGroup.congr (toPrincipalIdeal R' (FractionRing R')).range (toPrincipalIdeal R (FractionRing R)).range (Units.mapEquiv (↑(FractionalIdeal.ringEquivOfRingEquiv (FractionRing R) (FractionRing R') g)).symm) ⋯) ((equiv (FractionRing R')) a✝))

@[simp]

theorem ClassGroup.mulEquiv_apply {R : Type u_1} [CommRing R] [IsDomain R] {R' : Type u_3} [CommRing R'] [IsDomain R'] (g : R ≃+* R') (a✝ : ClassGroup R) : (mulEquiv g) a✝ = (equiv (FractionRing R')).symm ((QuotientGroup.congr (toPrincipalIdeal R (FractionRing R)).range (toPrincipalIdeal R' (FractionRing R')).range (Units.mapEquiv ↑(FractionalIdeal.ringEquivOfRingEquiv (FractionRing R) (FractionRing R') g)) ⋯) ((equiv (FractionRing R)) a✝))