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.

source

📐 coverage

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' := ⋯ }

source

🔸 coverage

@[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

Instances For

source

📐 coverage

@[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

source

📐 coverage

@[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

source

📐 coverage

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

source

📐 coverage

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

source

🔸 coverage

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.

Instances For

source

🔸 coverage

@[implicit_reducible]

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

CommGroup (ClassGroup R)

source

🔸 coverage

@[implicit_reducible]

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

Inhabited (ClassGroup R)

source

🔸 coverage

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).

Instances For

source

🔸 coverage

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.

Instances For

source

📐 coverage

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

source

📐 coverage

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 I

source

📐 coverage

theorem ClassGroup.mk_eq_mk {R : Type u_1} [CommRing R] [IsDomain R] {I J : (FractionalIdeal (nonZeroDivisors R) (FractionRing R))ˣ} :

mk I = mk J ↔ ∃ (x : (FractionRing R)ˣ), I * (toPrincipalIdeal R (FractionRing R)) x = J

source

📐 coverage

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 I = mk J ↔ ∃ (x : R) (y : R), x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J'

source

📐 coverage

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 I = 1 ↔ ∃ (x : R), x ≠ 0 ∧ I' = Ideal.span {x}

source

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 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.

source

🔸 coverage

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.

Instances For

source

📐 coverage

@[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 I) = (QuotientGroup.mk' (toPrincipalIdeal R K').range) ((Units.mapEquiv ↑(FractionalIdeal.canonicalEquiv (nonZeroDivisors R) K K')) I)

source

📐 coverage

@[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 ((Units.map ↑(FractionalIdeal.canonicalEquiv (nonZeroDivisors R) K K')) I) = mk I

source

🔸 coverage

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.

Instances For

source

📐 coverage

@[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

source

📐 coverage

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)

source

📐 coverage

@[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

source

🔸 coverage

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.

Instances For

source

📐 coverage

@[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 ((FractionalIdeal.mk0 K) I) = mk0 I

source

📐 coverage

@[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)

source

📐 coverage

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

source

📐 coverage

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

source

📐 coverage

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.

source

🔸 coverage

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.

Instances For

source

📐 coverage

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)

source

📐 coverage

theorem ClassGroup.mk0_integralRep {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] (I : (FractionalIdeal (nonZeroDivisors R) (FractionRing R))ˣ) :

mk0 ⟨integralRep ↑I, ⋯⟩ = mk I

source

📐 coverage

theorem ClassGroup.mk0_surjective {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] :

Function.Surjective ⇑mk0

source

📐 coverage

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 I = 1 ↔ (↑↑I).IsPrincipal

source

📐 coverage

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.

source

📐 coverage

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.

source

📐 coverage

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

source

📐 coverage

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}

source

🔸 coverage

@[implicit_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.

source

📐 coverage

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.

source

📐 coverage

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.

Documentation

Mathlib.RingTheory.ClassGroup

The ideal class group #

Main definitions #

Main results #

Implementation details #