refactor(ring_theory): submodules that are units are finitely generated (#18510)

alreadydone · alreadydone · commit ed90a7d327c3 · 2023-02-28T23:18:52.000Z
+ generalize from fractional_ideal to submodule. + the algebra doesn't have to be commutative. + introduce `fractional_ideal.coe_submodule_hom`. Potential future project: since we have [fractional_ideal.is_fractional_of_fg](https://leanprover-community.github.io/mathlib_docs/ring_theory/fractional_ideal.html#fractional_ideal.is_fractional_of_fg), submodules in a localization that are units are automatically fractional ideals, so [class_group](https://leanprover-community.github.io/mathlib_docs/ring_theory/class_group.html#class_group) could be defined as the invertible submodules in the fraction_ring modulo principal ones, without mentioning `is_fractional`. This might make `class_group` less complicated and therefore faster.
diff --git a/src/ring_theory/finiteness.lean b/src/ring_theory/finiteness.lean
@@ -126,6 +126,22 @@ lemma _root_.subalgebra.fg_bot_to_submodule {R A : Type*}
   (⊥ : subalgebra R A).to_submodule.fg :=
 ⟨{1}, by simp [algebra.to_submodule_bot] ⟩
 
+lemma fg_unit {R A : Type*} [comm_semiring R] [semiring A] [algebra R A]
+  (I : (submodule R A)ˣ) : (I : submodule R A).fg :=
+begin
+  have : (1 : A) ∈ (I * ↑I⁻¹ : submodule R A),
+  { rw I.mul_inv, exact one_le.mp le_rfl },
+  obtain ⟨T, T', hT, hT', one_mem⟩ := mem_span_mul_finite_of_mem_mul this,
+  refine ⟨T, span_eq_of_le _ hT _⟩,
+  rw [← one_mul ↑I, ← mul_one (span R ↑T)],
+  conv_rhs { rw [← I.inv_mul, ← mul_assoc] },
+  refine mul_le_mul_left (le_trans _ $ mul_le_mul_right $ span_le.mpr hT'),
+  rwa [one_le, span_mul_span],
+end
+
+lemma fg_of_is_unit {R A : Type*} [comm_semiring R] [semiring A] [algebra R A]
+  {I : submodule R A} (hI : is_unit I) : I.fg := fg_unit hI.unit
+
 theorem fg_span {s : set M} (hs : s.finite) : fg (span R s) :=
 ⟨hs.to_finset, by rw [hs.coe_to_finset]⟩
 
@@ -534,14 +550,6 @@ instance module.finite.tensor_product [comm_semiring R]
   [hM : module.finite R M] [hN : module.finite R N] : module.finite R (tensor_product R M N) :=
 { out := (tensor_product.map₂_mk_top_top_eq_top R M N).subst (hM.out.map₂ _ hN.out) }
 
-namespace algebra
-
-variables [comm_ring R] [comm_ring A] [algebra R A] [comm_ring B] [algebra R B]
-variables [add_comm_group M] [module R M]
-variables [add_comm_group N] [module R N]
-
-end algebra
-
 end module_and_algebra
 
 namespace ring_hom
diff --git a/src/ring_theory/fractional_ideal.lean b/src/ring_theory/fractional_ideal.lean
@@ -494,6 +494,12 @@ instance : comm_semiring (fractional_ideal S P) :=
 function.injective.comm_semiring coe subtype.coe_injective
   coe_zero coe_one coe_add coe_mul (λ _ _, coe_nsmul _ _) coe_pow coe_nat_cast
 
+variables (S P)
+/-- `fractional_ideal.submodule.has_coe` as a bundled `ring_hom`. -/
+@[simps] def coe_submodule_hom : fractional_ideal S P →+* submodule R P :=
+⟨coe, coe_one, coe_mul, coe_zero, coe_add⟩
+variables {S P}
+
 section order
 
 lemma add_le_add_left {I J : fractional_ideal S P} (hIJ : I ≤ J) (J' : fractional_ideal S P) :
@@ -710,21 +716,11 @@ variables {S}
 
 lemma fg_unit (I : (fractional_ideal S P)ˣ) :
   fg (I : submodule R P) :=
-begin
-  have : (1 : P) ∈ (I * ↑I⁻¹ : fractional_ideal S P),
-  { rw units.mul_inv, exact one_mem_one _ },
-  obtain ⟨T, T', hT, hT', one_mem⟩ := mem_span_mul_finite_of_mem_mul this,
-  refine ⟨T, submodule.span_eq_of_le _ hT _⟩,
-  rw [← one_mul ↑I, ← mul_one (span R ↑T)],
-  conv_rhs { rw [← coe_one, ← units.mul_inv I, coe_mul, mul_comm ↑↑I, ← mul_assoc] },
-  refine submodule.mul_le_mul_left
-    (le_trans _ (submodule.mul_le_mul_right (submodule.span_le.mpr hT'))),
-  rwa [submodule.one_le, submodule.span_mul_span]
-end
+submodule.fg_unit $ units.map (coe_submodule_hom S P).to_monoid_hom I
 
 lemma fg_of_is_unit (I : fractional_ideal S P) (h : is_unit I) :
   fg (I : submodule R P) :=
-by { rcases h with ⟨I, rfl⟩, exact fg_unit I }
+fg_unit h.unit
 
 lemma _root_.ideal.fg_of_is_unit (inj : function.injective (algebra_map R P))
   (I : ideal R) (h : is_unit (I : fractional_ideal S P)) :
