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)

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.

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

@[irreducible]

def toPrincipalIdeal (R : Type u_4) (K : Type u_5) [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

• toPrincipalIdeal = wrapped✝.1

@[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 ∈ MonoidHom.range (toPrincipalIdeal R K) ↔ ∃ (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] : Subgroup.Normal (MonoidHom.range (toPrincipalIdeal R K))

Equations

• (_ : Subgroup.Normal (MonoidHom.range (toPrincipalIdeal R K))) = (_ : Subgroup.Normal (MonoidHom.range (toPrincipalIdeal R K)))

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))ˣ ⧸ MonoidHom.range (toPrincipalIdeal R (FractionRing R)))

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

Equations

• instCommGroupClassGroup R = QuotientGroup.Quotient.commGroup (MonoidHom.range (toPrincipalIdeal R (FractionRing R)))

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

Equations

• instInhabitedClassGroup R = { default := 1 }

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 = MonoidHom.comp (QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R (FractionRing R)))) (Units.map ↑(FractionalIdeal.canonicalEquiv (nonZeroDivisors R) K (FractionRing R)))

theorem ClassGroup.Quot_mk_eq_mk {R : Type u_1} [CommRing R] [IsDomain R] (I : (FractionalIdeal (nonZeroDivisors R) (FractionRing R))ˣ) : Quot.mk Setoid.r I = ClassGroup.mk I

theorem ClassGroup.mk_eq_mk {R : Type u_1} [CommRing R] [IsDomain R] {I : (FractionalIdeal (nonZeroDivisors R) (FractionRing R))ˣ} {J : (FractionalIdeal (nonZeroDivisors R) (FractionRing R))ˣ} : ClassGroup.mk I = ClassGroup.mk 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 : (FractionalIdeal (nonZeroDivisors R) (FractionRing R))ˣ} {J : (FractionalIdeal (nonZeroDivisors R) (FractionRing R))ˣ} {I' : Ideal R} {J' : Ideal R} (hI : ↑I = ↑I') (hJ : ↑J = ↑J') : ClassGroup.mk I = ClassGroup.mk 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') : ClassGroup.mk 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 (ClassGroup.mk 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)ˣ ⧸ MonoidHom.range (toPrincipalIdeal R K)

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_4) [Field K'] [Algebra R K'] [IsFractionRing R K'] (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ) : (ClassGroup.equiv K') (ClassGroup.mk I) = (QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R K'))) ((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_4) [Field K'] [Algebra R K'] [IsFractionRing R K'] (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ) : ClassGroup.mk ((Units.map ↑(FractionalIdeal.canonicalEquiv (nonZeroDivisors R) K K')) I) = ClassGroup.mk 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

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

@[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))) : ↑((FractionalIdeal.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_4) [Field K'] [Algebra R K'] [IsFractionRing R K'] (I : ↥(nonZeroDivisors (Ideal R))) : (FractionalIdeal.canonicalEquiv (nonZeroDivisors R) K K') ↑((FractionalIdeal.mk0 K) I) = ↑((FractionalIdeal.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_4) [Field K'] [Algebra R K'] [IsFractionRing R K'] (I : ↥(nonZeroDivisors (Ideal R))) : (Units.map ↑(FractionalIdeal.canonicalEquiv (nonZeroDivisors R) K K')) ((FractionalIdeal.mk0 K) I) = (FractionalIdeal.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 = MonoidHom.comp ClassGroup.mk (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))) : ClassGroup.mk ((FractionalIdeal.mk0 K) I) = ClassGroup.mk0 I

@[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))) : (ClassGroup.equiv K) (ClassGroup.mk0 I) = (QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R K))) ((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 : ↥(nonZeroDivisors (Ideal R))} {J : ↥(nonZeroDivisors (Ideal R))} : ClassGroup.mk0 I = ClassGroup.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 : ↥(nonZeroDivisors (Ideal R))} {J : ↥(nonZeroDivisors (Ideal R))} : ClassGroup.mk0 I = ClassGroup.mk0 J ↔ ∃ (x : R) (y : R) (_ : x ≠ 0) (_ : y ≠ 0), Ideal.span {x} * ↑I = Ideal.span {y} * ↑J

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

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

Equations

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

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

theorem ClassGroup.mk0_integralRep {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] (I : (FractionalIdeal (nonZeroDivisors R) (FractionRing R))ˣ) : ClassGroup.mk0 { val := ClassGroup.integralRep ↑I, property := (_ : ClassGroup.integralRep ↑I ∈ nonZeroDivisors (Ideal R)) } = ClassGroup.mk I

theorem ClassGroup.mk0_surjective {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] : Function.Surjective ⇑ClassGroup.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)ˣ} : ClassGroup.mk I = 1 ↔ Submodule.IsPrincipal ↑↑I

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

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

noncomputable instance instFintypeClassGroup {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

• instFintypeClassGroup = { elems := {1}, complete := (_ : ∀ (x : ClassGroup R), x ∈ {1}) }

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.