refactor(ring_theory/class_group): redefine class_group without fraction field (#16727)

Although the definition of the class group of a ring `R` involves the field of fractions, the definition does not depend (up to isomorphism) on the choice of field of fractions. This PR proposes to always choose `fraction_ring R` as that field, so that we don't need to carry around the mathematically unnecessary parameters `(K) [field K] [algebra R K] [is_fraction_ring R K]`. Instead, we insert the isomorphism between the definitions of class group at the API boundaries.

This was inspired by our work on quadratic rings: it gets even more annoying when you need to start carrying around a proof that the field of fractions of `ℤ[1/2√-7]` is `ℚ(√-7)`.



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

Author: Vierkantor

src/number_theory/class_number/finite.lean

@@ -292,9 +292,8 @@ include ist iic
 
 /-- Each class in the class group contains an ideal `J`
 such that `M := Π m ∈ finset_approx` is in `J`. -/
-theorem exists_mk0_eq_mk0 [is_dedekind_domain S] [is_fraction_ring S L]
-  (h : algebra.is_algebraic R L) (I : (ideal S)⁰) :
-  ∃ (J : (ideal S)⁰), class_group.mk0 L I = class_group.mk0 L J ∧
+theorem exists_mk0_eq_mk0 [is_dedekind_domain S] (h : algebra.is_algebraic R L) (I : (ideal S)⁰) :
+  ∃ (J : (ideal S)⁰), class_group.mk0 I = class_group.mk0 J ∧
     algebra_map _ _ (∏ m in finset_approx bS adm, m) ∈ (J : ideal S) :=
 begin
   set M := ∏ m in finset_approx bS adm, m with M_eq,
@@ -332,17 +331,16 @@ omit iic ist
 /-- `class_group.mk_M_mem` is a specialization of `class_group.mk0` to (the finite set of)
 ideals that contain `M := ∏ m in finset_approx L f abs, m`.
 By showing this function is surjective, we prove that the class group is finite. -/
-noncomputable def mk_M_mem [is_fraction_ring S L] [is_dedekind_domain S]
+noncomputable def mk_M_mem [is_dedekind_domain S]
   (J : {J : ideal S // algebra_map _ _ (∏ m in finset_approx bS adm, m) ∈ J}) :
-  class_group S L :=
-class_group.mk0 _ ⟨J.1, mem_non_zero_divisors_iff_ne_zero.mpr
+  class_group S :=
+class_group.mk0 ⟨J.1, mem_non_zero_divisors_iff_ne_zero.mpr
   (ne_bot_of_prod_finset_approx_mem bS adm J.1 J.2)⟩
 
 include iic ist
 
-lemma mk_M_mem_surjective [is_fraction_ring S L] [is_dedekind_domain S]
-  (h : algebra.is_algebraic R L) :
-  function.surjective (class_group.mk_M_mem L bS adm) :=
+lemma mk_M_mem_surjective [is_dedekind_domain S] (h : algebra.is_algebraic R L) :
+  function.surjective (class_group.mk_M_mem bS adm) :=
 begin
   intro I',
   obtain ⟨⟨I, hI⟩, rfl⟩ := class_group.mk0_surjective I',
@@ -358,8 +356,8 @@ algebraic extension `L` is finite if there is an admissible absolute value.
 See also `class_group.fintype_of_admissible_of_finite` where `L` is a finite
 extension of `K = Frac(R)`, supplying most of the required assumptions automatically.
 -/
-noncomputable def fintype_of_admissible_of_algebraic [is_fraction_ring S L] [is_dedekind_domain S]
-  (h : algebra.is_algebraic R L) : fintype (class_group S L) :=
+noncomputable def fintype_of_admissible_of_algebraic [is_dedekind_domain S]
+  (h : algebra.is_algebraic R L) : fintype (class_group S) :=
 @fintype.of_surjective _ _ _
   (@fintype.of_equiv _
     {J // J ∣ ideal.span ({algebra_map R S (∏ (m : R) in finset_approx bS adm, m)} : set S)}
@@ -368,9 +366,11 @@ noncomputable def fintype_of_admissible_of_algebraic [is_fraction_ring S L] [is_
             exact prod_finset_approx_ne_zero bS adm }))
     ((equiv.refl _).subtype_equiv (λ I, ideal.dvd_iff_le.trans
       (by rw [equiv.refl_apply, ideal.span_le, set.singleton_subset_iff]))))
-  (class_group.mk_M_mem L bS adm)
+  (class_group.mk_M_mem bS adm)
   (class_group.mk_M_mem_surjective L bS adm h)
 
+include K
+
 /-- The main theorem: the class group of an integral closure `S` of `R` in a
 finite extension `L` of `K = Frac(R)` is finite if there is an admissible
 absolute value.
@@ -379,8 +379,7 @@ See also `class_group.fintype_of_admissible_of_algebraic` where `L` is an
 algebraic extension of `R`, that includes some extra assumptions.
 -/
 noncomputable def fintype_of_admissible_of_finite [is_dedekind_domain R] :
-  fintype (@class_group S L _ _ _
-    (is_integral_closure.is_fraction_ring_of_finite_extension R K L S)) :=
+  fintype (class_group S) :=
 begin
   letI := classical.dec_eq L,
   letI := is_integral_closure.is_fraction_ring_of_finite_extension R K L S,

src/number_theory/class_number/function_field.lean

@@ -33,15 +33,15 @@ namespace ring_of_integers
 
 open function_field
 
-noncomputable instance  : fintype (class_group (ring_of_integers Fq F) F) :=
+noncomputable instance  : fintype (class_group (ring_of_integers Fq F)) :=
 class_group.fintype_of_admissible_of_finite (ratfunc Fq) F
   (polynomial.card_pow_degree_is_admissible : absolute_value.is_admissible
     (polynomial.card_pow_degree : absolute_value Fq[X] ℤ))
 
 end ring_of_integers
 
 /-- The class number in a function field is the (finite) cardinality of the class group. -/
-noncomputable def class_number : ℕ := fintype.card (class_group (ring_of_integers Fq F) F)
+noncomputable def class_number : ℕ := fintype.card (class_group (ring_of_integers Fq F))
 
 /-- The class number of a function field is `1` iff the ring of integers is a PID. -/
 theorem class_number_eq_one_iff :

src/number_theory/number_field/class_number.lean

@@ -25,13 +25,13 @@ variables (K : Type*) [field K] [number_field K]
 
 namespace ring_of_integers
 
-noncomputable instance : fintype (class_group (ring_of_integers K) K) :=
-class_group.fintype_of_admissible_of_finite ℚ _ absolute_value.abs_is_admissible
+noncomputable instance : fintype (class_group (ring_of_integers K)) :=
+class_group.fintype_of_admissible_of_finite ℚ K absolute_value.abs_is_admissible
 
 end ring_of_integers
 
 /-- The class number of a number field is the (finite) cardinality of the class group. -/
-noncomputable def class_number : ℕ := fintype.card (class_group (ring_of_integers K) K)
+noncomputable def class_number : ℕ := fintype.card (class_group (ring_of_integers K))
 
 variables {K}