feat(ring_theory): define the ideal class group (#8626)

This PR defines the ideal class group of an integral domain, as the quotient of the invertible fractional ideals by the principal fractional ideals. It also shows that this corresponds to the more traditional definition in a Dedekind domain, namely the quotient of the nonzero ideals by `I ~ J ↔ ∃ xy, xI = yJ`.

Co-Authored-By: Ashvni ashvni.n@gmail.com
Co-Authored-By: Filippo A. E. Nuccio filippo.nuccio@univ-st-etienne.fr



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

Author: Vierkantor

src/ring_theory/class_group.lean

@@ -0,0 +1,251 @@
+/-
+Copyright (c) 2021 Anne Baanen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen
+-/
+
+import group_theory.quotient_group
+import ring_theory.dedekind_domain
+
+/-!
+# The ideal class group
+
+This file defines the ideal class group `class_group R K` of fractional ideals of `R`
+inside `A`'s field of fractions `K`.
+
+## Main definitions
+ - `to_principal_ideal` sends an invertible `x : K` to an invertible fractional ideal
+ - `class_group` is the quotient of invertible fractional ideals modulo `to_principal_ideal.range`
+ - `class_group.mk0` sends a nonzero integral ideal in a Dedekind domain to its class
+
+## Main results
+ - `class_group.mk0_eq_mk0_iff` shows the equivalence with the "classical" definition,
+   where `I ~ J` iff `x I = y J` for `x y ≠ (0 : R)`
+-/
+
+section integral_domain
+
+variables {R K L : Type*} [integral_domain R]
+variables [field K] [field L] [decidable_eq L]
+variables [algebra R K] [is_fraction_ring R K]
+variables [algebra K L] [finite_dimensional K L]
+variables [algebra R L] [is_scalar_tower R K L]
+
+open_locale non_zero_divisors
+
+open is_localization is_fraction_ring fractional_ideal units
+
+section
+
+variables (R K)
+
+/-- `to_principal_ideal R K x` sends `x ≠ 0 : K` to the fractional `R`-ideal generated by `x` -/
+@[irreducible]
+def to_principal_ideal : units K →* units (fractional_ideal R⁰ K) :=
+{ to_fun := λ x,
+  ⟨span_singleton _ x,
+   span_singleton _ x⁻¹,
+   by simp only [span_singleton_one, units.mul_inv', span_singleton_mul_span_singleton],
+   by simp only [span_singleton_one, units.inv_mul', span_singleton_mul_span_singleton]⟩,
+  map_mul' := λ x y, ext
+    (by simp only [units.coe_mk, units.coe_mul, span_singleton_mul_span_singleton]),
+  map_one' := ext (by simp only [span_singleton_one, units.coe_mk, units.coe_one]) }
+
+local attribute [semireducible] to_principal_ideal
+
+variables {R K}
+
+@[simp] lemma coe_to_principal_ideal (x : units K) :
+  (to_principal_ideal R K x : fractional_ideal R⁰ K) = span_singleton _ x :=
+rfl
+
+@[simp] lemma to_principal_ideal_eq_iff {I : units (fractional_ideal R⁰ K)} {x : units K} :
+  to_principal_ideal R K x = I ↔ span_singleton R⁰ (x : K) = I :=
+units.ext_iff
+
+end
+
+instance principal_ideals.normal : (to_principal_ideal R K).range.normal :=
+subgroup.normal_of_comm _
+
+section
+
+variables (R K)
+
+/-- The ideal class group of `R` in a field of fractions `K`
+is the group of invertible fractional ideals modulo the principal ideals. -/
+@[derive(comm_group)]
+def class_group := quotient_group.quotient (to_principal_ideal R K).range
+
+instance : inhabited (class_group R K) := ⟨1⟩
+
+variables {R}
+
+/-- Send a nonzero integral ideal to an invertible fractional ideal. -/
+@[simps]
+noncomputable def fractional_ideal.mk0 [is_dedekind_domain R] :
+  (ideal R)⁰ →* units (fractional_ideal R⁰ K) :=
+{ to_fun := λ I, units.mk0 I ((fractional_ideal.coe_to_fractional_ideal_ne_zero (le_refl R⁰)).mpr
+    (mem_non_zero_divisors_iff_ne_zero.mp I.2)),
+  map_one' := by simp,
+  map_mul' := λ x y, by simp }
+
+/-- Send a nonzero ideal to the corresponding class in the class group. -/
+@[simps]
+noncomputable def class_group.mk0 [is_dedekind_domain R] :
+  (ideal R)⁰ →* class_group R K :=
+(quotient_group.mk' _).comp (fractional_ideal.mk0 K)
+
+variables {K}
+
+lemma quotient_group.mk'_eq_mk' {G : Type*} [group G] {N : subgroup G} [hN : N.normal] {x y : G} :
+  quotient_group.mk' N x = quotient_group.mk' N y ↔ ∃ z ∈ N, x * z = y :=
+(@quotient.eq _ (quotient_group.left_rel _) _ _).trans
+  ⟨λ (h : x⁻¹ * y ∈ N), ⟨_, h, by rw [← mul_assoc, mul_right_inv, one_mul]⟩,
+   λ ⟨z, z_mem, eq_y⟩,
+     by { rw ← eq_y, show x⁻¹ * (x * z) ∈ N, rwa [← mul_assoc, mul_left_inv, one_mul] }⟩
+
+lemma class_group.mk0_eq_mk0_iff_exists_fraction_ring [is_dedekind_domain R] {I J : (ideal R)⁰} :
+  class_group.mk0 K I = class_group.mk0 K J ↔
+    ∃ (x ≠ (0 : K)), span_singleton R⁰ x * I = J :=
+begin
+  simp only [class_group.mk0, monoid_hom.comp_apply, quotient_group.mk'_eq_mk'],
+  split,
+  { rintros ⟨_, ⟨x, rfl⟩, hx⟩,
+    refine ⟨x, x.ne_zero, _⟩,
+    simpa only [mul_comm, coe_mk0, monoid_hom.to_fun_eq_coe, coe_to_principal_ideal, units.coe_mul]
+      using congr_arg (coe : _ → fractional_ideal R⁰ K) hx },
+  { rintros ⟨x, hx, eq_J⟩,
+    refine ⟨_, ⟨units.mk0 x hx, rfl⟩, units.ext _⟩,
+    simpa only [fractional_ideal.mk0_apply, units.coe_mk0, mul_comm, coe_to_principal_ideal,
+        coe_coe, units.coe_mul] using eq_J }
+end
+
+lemma class_group.mk0_eq_mk0_iff [is_dedekind_domain R] {I J : (ideal R)⁰} :
+  class_group.mk0 K I = class_group.mk0 K J ↔
+    ∃ (x y : R) (hx : x ≠ 0) (hy : y ≠ 0), ideal.span {x} * (I : ideal R) = ideal.span {y} * J :=
+begin
+  refine class_group.mk0_eq_mk0_iff_exists_fraction_ring.trans ⟨_, _⟩,
+  { rintros ⟨z, hz, h⟩,
+    obtain ⟨x, ⟨y, hy⟩, rfl⟩ := is_localization.mk'_surjective R⁰ z,
+    refine ⟨x, y, _, mem_non_zero_divisors_iff_ne_zero.mp hy, _⟩,
+    { rintro hx, apply hz,
+      rw [hx, is_fraction_ring.mk'_eq_div, (algebra_map R K).map_zero, zero_div] },
+    { exact (fractional_ideal.mk'_mul_coe_ideal_eq_coe_ideal K hy).mp h } },
+  { rintros ⟨x, y, hx, hy, h⟩,
+    have hy' : y ∈ R⁰ := mem_non_zero_divisors_iff_ne_zero.mpr hy,
+    refine ⟨is_localization.mk' K x ⟨y, hy'⟩, _, _⟩,
+    { contrapose! hx,
+      rwa [is_localization.mk'_eq_iff_eq_mul, zero_mul, ← (algebra_map R K).map_zero,
+           (is_fraction_ring.injective R K).eq_iff] at hx },
+    { exact (fractional_ideal.mk'_mul_coe_ideal_eq_coe_ideal K hy').mpr h } },
+end
+
+lemma class_group.mk0_surjective [is_dedekind_domain R] :
+  function.surjective (class_group.mk0 K : (ideal R)⁰ → class_group R K) :=
+begin
+  rintros ⟨I⟩,
+  obtain ⟨a, a_ne_zero', ha⟩ := I.1.2,
+  have a_ne_zero := mem_non_zero_divisors_iff_ne_zero.mp a_ne_zero',
+  have fa_ne_zero : (algebra_map R K) a ≠ 0 :=
+    is_fraction_ring.to_map_ne_zero_of_mem_non_zero_divisors a_ne_zero',
+  refine ⟨⟨{ carrier := { x | (algebra_map R K a)⁻¹ * algebra_map R K x ∈ I.1 }, .. }, _⟩, _⟩,
+  { simp only [ring_hom.map_zero, set.mem_set_of_eq, mul_zero, ring_hom.map_mul],
+    exact submodule.zero_mem I },
+  { simp only [ring_hom.map_add, set.mem_set_of_eq, mul_zero, ring_hom.map_mul, mul_add],
+    exact λ _ _ ha hb, submodule.add_mem I ha hb },
+  { intros c _ hb,
+    simp only [smul_eq_mul, set.mem_set_of_eq, mul_zero, ring_hom.map_mul, mul_add,
+               mul_left_comm ((algebra_map R K) a)⁻¹],
+    rw ← algebra.smul_def c,
+    exact submodule.smul_mem I c hb },
+  { rw [mem_non_zero_divisors_iff_ne_zero, submodule.zero_eq_bot, submodule.ne_bot_iff],
+    obtain ⟨x, x_ne, x_mem⟩ := exists_ne_zero_mem_is_integer I.ne_zero,
+    refine ⟨a * x, _, mul_ne_zero a_ne_zero x_ne⟩,
+    change ((algebra_map R K) a)⁻¹ * (algebra_map R K) (a * x) ∈ I.1,
+    rwa [ring_hom.map_mul, ← mul_assoc, inv_mul_cancel fa_ne_zero, one_mul] },
+  { symmetry,
+    apply quotient.sound,
+    refine ⟨units.mk0 (algebra_map R K a) fa_ne_zero, _⟩,
+    apply @mul_left_cancel _ _ I,
+    rw [← mul_assoc, mul_right_inv, one_mul, eq_comm, mul_comm I],
+    apply units.ext,
+    simp only [monoid_hom.coe_mk, subtype.coe_mk, ring_hom.map_mul, coe_coe,
+               units.coe_mul, coe_to_principal_ideal, coe_mk0,
+               fractional_ideal.eq_span_singleton_mul],
+    split,
+    { intros zJ' hzJ',
+      obtain ⟨zJ, hzJ : (algebra_map R K a)⁻¹ * algebra_map R K zJ ∈ ↑I, rfl⟩ :=
+        (mem_coe_ideal R⁰).mp hzJ',
+      refine ⟨_, hzJ, _⟩,
+      rw [← mul_assoc, mul_inv_cancel fa_ne_zero, one_mul] },
+    { intros zI' hzI',
+      obtain ⟨y, hy⟩ := ha zI' hzI',
+      rw [← algebra.smul_def, fractional_ideal.mk0_apply, coe_mk0, coe_coe, mem_coe_ideal],
+      refine ⟨y, _, hy⟩,
+      show (algebra_map R K a)⁻¹ * algebra_map R K y ∈ (I : fractional_ideal R⁰ K),
+      rwa [hy, algebra.smul_def, ← mul_assoc, inv_mul_cancel fa_ne_zero, one_mul] } }
+end
+
+end
+
+lemma class_group.mk_eq_one_iff
+  {I : units (fractional_ideal R⁰ K)} :
+  quotient_group.mk' (to_principal_ideal R K).range I = 1 ↔
+    (I : submodule R K).is_principal :=
+begin
+  rw [← (quotient_group.mk' _).map_one, eq_comm, quotient_group.mk'_eq_mk'],
+  simp only [exists_prop, one_mul, exists_eq_right, to_principal_ideal_eq_iff,
+             monoid_hom.mem_range, coe_coe],
+  refine ⟨λ ⟨x, hx⟩, ⟨⟨x, by rw [← hx, coe_span_singleton]⟩⟩, _⟩,
+  unfreezingI { intros hI },
+  obtain ⟨x, hx⟩ := @submodule.is_principal.principal _ _ _ _ _ _ hI,
+  have hx' : (I : fractional_ideal R⁰ K) = span_singleton R⁰ x,
+  { apply subtype.coe_injective, rw [hx, coe_span_singleton] },
+  refine ⟨units.mk0 x _, _⟩,
+  { intro x_eq, apply units.ne_zero I, simp [hx', x_eq] },
+  simp [hx']
+end
+
+lemma class_group.mk0_eq_one_iff [is_dedekind_domain R]
+  {I : ideal R} (hI : I ∈ (ideal R)⁰) :
+  class_group.mk0 K ⟨I, hI⟩ = 1 ↔ I.is_principal :=
+class_group.mk_eq_one_iff.trans (coe_submodule_is_principal R K)
+
+/-- The class group of principal ideal domain is finite (in fact a singleton).
+TODO: generalize to Dedekind domains -/
+instance [is_principal_ideal_ring R] :
+  fintype (class_group R K) :=
+{ elems := {1},
+  complete :=
+  begin
+    rintros ⟨I⟩,
+    rw [finset.mem_singleton],
+    exact class_group.mk_eq_one_iff.mpr (I : fractional_ideal R⁰ K).is_principal
+  end }
+
+/-- The class number of a principal ideal domain is `1`. -/
+lemma card_class_group_eq_one [is_principal_ideal_ring R] :
+  fintype.card (class_group R K) = 1 :=
+begin
+  rw fintype.card_eq_one_iff,
+  use 1,
+  rintros ⟨I⟩,
+  exact class_group.mk_eq_one_iff.mpr (I : fractional_ideal R⁰ K).is_principal
+end
+
+/-- The class number is `1` iff the ring of integers is a principal ideal domain. -/
+lemma card_class_group_eq_one_iff [is_dedekind_domain R] [fintype (class_group R K)] :
+  fintype.card (class_group R K) = 1 ↔ is_principal_ideal_ring R :=
+begin
+  split, swap, { introsI, convert card_class_group_eq_one, assumption },
+  rw fintype.card_eq_one_iff,
+  rintros ⟨I, hI⟩,
+  have eq_one : ∀ J : class_group R K, J = 1 := λ J, trans (hI J) (hI 1).symm,
+  refine ⟨λ I, _⟩,
+  by_cases hI : I = ⊥,
+  { rw hI, exact bot_is_principal },
+  exact (class_group.mk0_eq_one_iff (mem_non_zero_divisors_iff_ne_zero.mpr hI)).mp (eq_one _),
+end
+
+end integral_domain

src/ring_theory/dedekind_domain.lean

@@ -46,7 +46,7 @@ dedekind domain, dedekind ring
 
 variables (R A K : Type*) [comm_ring R] [integral_domain A] [field K]
 
-local notation R`⁰`:9000 := non_zero_divisors R
+open_locale non_zero_divisors
 
 /-- A ring `R` has Krull dimension at most one if all nonzero prime ideals are maximal. -/
 def ring.dimension_le_one : Prop :=

src/ring_theory/fractional_ideal.lean

@@ -66,7 +66,7 @@ fractional ideal, fractional ideals, invertible ideal
 open is_localization
 open_locale pointwise
 
-local notation R`⁰`:9000 := non_zero_divisors R
+open_locale non_zero_divisors
 
 section defs
 

src/ring_theory/localization.lean

@@ -266,6 +266,16 @@ lemma mk'_spec' (x) (y : M) :
   algebra_map R S y * mk' S x y = algebra_map R S x :=
 (to_localization_map M S).mk'_spec' _ _
 
+@[simp]
+lemma mk'_spec_mk (x) (y : R) (hy : y ∈ M) :
+  mk' S x ⟨y, hy⟩ * algebra_map R S y = algebra_map R S x :=
+mk'_spec S x ⟨y, hy⟩
+
+@[simp]
+lemma mk'_spec'_mk (x) (y : R) (hy : y ∈ M) :
+  algebra_map R S y * mk' S x ⟨y, hy⟩ = algebra_map R S x :=
+mk'_spec' S x ⟨y, hy⟩
+
 variables {S}
 
 theorem eq_mk'_iff_mul_eq {x} {y : M} {z} :
@@ -1502,10 +1512,15 @@ lemma mk'_mk_eq_div {r s} (hs : s ∈ non_zero_divisors A) :
 mk'_eq_iff_eq_mul.2 $ (div_mul_cancel (algebra_map A K r)
     (is_fraction_ring.to_map_ne_zero_of_mem_non_zero_divisors hs)).symm
 
-lemma mk'_eq_div {r} (s : non_zero_divisors A) :
+@[simp] lemma mk'_eq_div {r} (s : non_zero_divisors A) :
   mk' K r s = algebra_map A K r / algebra_map A K s :=
 mk'_mk_eq_div s.2
 
+lemma div_surjective (z : K) : ∃ (x y : A) (hy : y ∈ non_zero_divisors A),
+  algebra_map _ _ x / algebra_map _ _ y = z :=
+let ⟨x, ⟨y, hy⟩, h⟩ := mk'_surjective (non_zero_divisors A) z
+in ⟨x, y, hy, by rwa mk'_eq_div at h⟩
+
 lemma is_unit_map_of_injective (hg : function.injective g)
   (y : non_zero_divisors A) : is_unit (g y) :=
 is_unit.mk0 (g y) $ show g.to_monoid_with_zero_hom y ≠ 0,
@@ -1518,19 +1533,21 @@ such that `z = f x * (f y)⁻¹`. -/
 noncomputable def lift (hg : injective g) : K →+* L :=
 lift $ λ (y : non_zero_divisors A), is_unit_map_of_injective hg y
 
+/-- Given an integral domain `A` with field of fractions `K`,
+and an injective ring hom `g : A →+* L` where `L` is a field,
+the field hom induced from `K` to `L` maps `x` to `g x` for all
+`x : A`. -/
+@[simp] lemma lift_algebra_map (hg : injective g) (x) :
+  lift hg (algebra_map A K x) = g x :=
+lift_eq _ _
+
 /-- Given an integral domain `A` with field of fractions `K`,
 and an injective ring hom `g : A →+* L` where `L` is a field,
 field hom induced from `K` to `L` maps `f x / f y` to `g x / g y` for all
 `x : A, y ∈ non_zero_divisors A`. -/
-@[simp] lemma lift_mk' (hg : injective g) (x) (y : non_zero_divisors A) :
+lemma lift_mk' (hg : injective g) (x) (y : non_zero_divisors A) :
   lift hg (mk' K x y) = g x / g y :=
-begin
-  erw lift_mk' (is_unit_map_of_injective hg),
-  erw submonoid.localization_map.mul_inv_left
-  (λ y : non_zero_divisors A, show is_unit (g.to_monoid_hom y), from
-    is_unit_map_of_injective hg y),
-  exact (mul_div_cancel' _ (g.map_ne_zero_of_mem_non_zero_divisors hg y.2)).symm,
-end
+by simp only [mk'_eq_div, ring_hom.map_div, lift_algebra_map]
 
 /-- Given integral domains `A, B` with fields of fractions `K`, `L`
 and an injective ring hom `j : A →+* B`, we get a field hom