feat(ring_theory/class_group): add class_group.mk_eq_mk (#18034)

src/ring_theory/class_group.lean

@@ -74,19 +74,19 @@ begin
   { exact ⟨x, hx⟩ },
   { refine ⟨units.mk0 x _, hx⟩,
     rintro rfl,
-    simpa [I.ne_zero.symm] using hx },
-
+    simpa [I.ne_zero.symm] using hx }
 end
 
 instance principal_ideals.normal : (to_principal_ideal R K).range.normal :=
 subgroup.normal_of_comm _
+
 end
 
 variables (R) [is_domain R]
 
 /-- The ideal class group of `R` is the group of invertible fractional ideals
 modulo the principal ideals. -/
-@[derive(comm_group)]
+@[derive comm_group]
 def class_group :=
 (fractional_ideal R⁰ (fraction_ring R))ˣ ⧸ (to_principal_ideal R (fraction_ring R)).range
 
@@ -99,6 +99,50 @@ noncomputable def class_group.mk : (fractional_ideal R⁰ K)ˣ →* class_group
 (quotient_group.mk' (to_principal_ideal R (fraction_ring R)).range).comp
   (units.map (fractional_ideal.canonical_equiv R⁰ K (fraction_ring R)))
 
+lemma class_group.mk_eq_mk {I J : (fractional_ideal R⁰ $ fraction_ring R)ˣ} :
+  class_group.mk I = class_group.mk J
+    ↔ ∃ x : (fraction_ring R)ˣ, I * to_principal_ideal R (fraction_ring R) x = J :=
+by { erw [quotient_group.mk'_eq_mk', canonical_equiv_self, units.map_id, set.exists_range_iff],
+     refl }
+
+lemma class_group.mk_eq_mk_of_coe_ideal
+  {I J : (fractional_ideal R⁰ $ fraction_ring R)ˣ} {I' J' : ideal R}
+  (hI : (I : fractional_ideal R⁰ $ fraction_ring R) = I')
+  (hJ : (J : fractional_ideal R⁰ $ fraction_ring R) = J') :
+  class_group.mk I = class_group.mk J
+    ↔ ∃ x y : R, x ≠ 0 ∧ y ≠ 0 ∧ ideal.span {x} * I' = ideal.span {y} * J' :=
+begin
+  rw [class_group.mk_eq_mk],
+  split,
+  { rintro ⟨x, rfl⟩,
+    rw [units.coe_mul, hI, coe_to_principal_ideal, mul_comm,
+        span_singleton_mul_coe_ideal_eq_coe_ideal] at hJ,
+    exact ⟨_, _, sec_fst_ne_zero le_rfl x.ne_zero, sec_snd_ne_zero le_rfl ↑x, hJ⟩ },
+  { rintro ⟨x, y, hx, hy, h⟩,
+    split, rw [mul_comm, ← units.eq_iff, units.coe_mul, coe_to_principal_ideal],
+    convert (mk'_mul_coe_ideal_eq_coe_ideal (fraction_ring R) $
+              mem_non_zero_divisors_of_ne_zero hy).2 h,
+    apply (ne.is_unit _).unit_spec,
+    rwa [ne, mk'_eq_zero_iff_eq_zero] }
+end
+
+lemma class_group.mk_eq_one_of_coe_ideal {I : (fractional_ideal R⁰ $ fraction_ring R)ˣ}
+  {I' : ideal R} (hI : (I : fractional_ideal R⁰ $ fraction_ring R) = I') :
+  class_group.mk I = 1 ↔ ∃ x : R, x ≠ 0 ∧ I' = ideal.span {x} :=
+begin
+  rw [← map_one class_group.mk, class_group.mk_eq_mk_of_coe_ideal hI (_ : _ = ↑⊤)],
+  any_goals { refl },
+  split,
+  { rintro ⟨x, y, hx, hy, h⟩,
+    rw [ideal.mul_top] at h,
+    rcases ideal.mem_span_singleton_mul.mp ((ideal.span_singleton_le_iff_mem _).mp h.ge)
+      with ⟨i, hi, rfl⟩,
+    rw [← ideal.span_singleton_mul_span_singleton, ideal.span_singleton_mul_right_inj hx] at h,
+    exact ⟨i, right_ne_zero_of_mul hy, h⟩ },
+  { rintro ⟨x, hx, rfl⟩,
+    exact ⟨1, x, one_ne_zero, hx, by rw [ideal.span_singleton_one, ideal.top_mul, ideal.mul_top]⟩ }
+end
+
 variables (K)
 
 /-- Induction principle for the class group: to show something holds for all `x : class_group R`,

src/ring_theory/dedekind_domain/ideal.lean

@@ -138,7 +138,7 @@ lemma span_singleton_div_self {x : K} (hx : x ≠ 0) :
 by rw [span_singleton_div_span_singleton, div_self hx, span_singleton_one]
 
 lemma coe_ideal_span_singleton_div_self {x : R₁} (hx : x ≠ 0) :
-  ((ideal.span {x} : ideal R₁) : fractional_ideal R₁⁰ K) / (ideal.span {x} : ideal R₁) = 1 :=
+  (ideal.span ({x} : set R₁) : fractional_ideal R₁⁰ K) / ideal.span ({x} : set R₁) = 1 :=
 by rw [coe_ideal_span_singleton, span_singleton_div_self K $
         (map_ne_zero_iff _ $ no_zero_smul_divisors.algebra_map_injective R₁ K).mpr hx]
 
@@ -147,7 +147,7 @@ lemma span_singleton_mul_inv {x : K} (hx : x ≠ 0) :
 by rw [span_singleton_inv, span_singleton_mul_span_singleton, mul_inv_cancel hx, span_singleton_one]
 
 lemma coe_ideal_span_singleton_mul_inv {x : R₁} (hx : x ≠ 0) :
-  ((ideal.span {x} : ideal R₁) : fractional_ideal R₁⁰ K) * (ideal.span {x} : ideal R₁)⁻¹ = 1 :=
+  (ideal.span ({x} : set R₁) : fractional_ideal R₁⁰ K) * (ideal.span ({x} : set R₁))⁻¹ = 1 :=
 by rw [coe_ideal_span_singleton, span_singleton_mul_inv K $
         (map_ne_zero_iff _ $ no_zero_smul_divisors.algebra_map_injective R₁ K).mpr hx]
 
@@ -156,7 +156,7 @@ lemma span_singleton_inv_mul {x : K} (hx : x ≠ 0) :
 by rw [mul_comm, span_singleton_mul_inv K hx]
 
 lemma coe_ideal_span_singleton_inv_mul {x : R₁} (hx : x ≠ 0) :
-  ((ideal.span {x} : ideal R₁) : fractional_ideal R₁⁰ K)⁻¹ * (ideal.span {x} : ideal R₁) = 1 :=
+  (ideal.span ({x} : set R₁) : fractional_ideal R₁⁰ K)⁻¹ * ideal.span ({x} : set R₁) = 1 :=
 by rw [mul_comm, coe_ideal_span_singleton_mul_inv K hx]
 
 lemma mul_generator_self_inv {R₁ : Type*} [comm_ring R₁] [algebra R₁ K] [is_localization R₁⁰ K]