Extend RingTheory.Flat.iff_rTensor_injective to all ideals (#8494)

Extend `RingTheory.Flat.iff_rTensor_injective` to all ideals

Using an elementary argument after Dummit and Foote (2004, Ex. 10.25)

Mathlib/RingTheory/Finiteness.lean

@@ -417,6 +417,27 @@ theorem fg_iff_compact (s : Submodule R M) : s.FG ↔ CompleteLattice.IsCompactE
       exact ⟨t, ssup⟩
 #align submodule.fg_iff_compact Submodule.fg_iff_compact
 
+open TensorProduct LinearMap in
+/-- Every `x : I ⊗ M` is the image of some `y : J ⊗ M`, where `J ≤ I` is finitely generated,
+under the tensor product of `J.inclusion ‹J ≤ I› : J → I` and the identity `M → M`. -/
+theorem exists_fg_le_eq_rTensor_inclusion {R M N : Type*} [CommRing R] [AddCommGroup M]
+    [AddCommGroup N] [Module R M] [Module R N] {I : Submodule R N} (x : I ⊗ M) :
+      ∃ (J : Submodule R N) (_ : J.FG) (hle : J ≤ I) (y : J ⊗ M),
+        x = rTensor M (J.inclusion hle) y := by
+  induction x using TensorProduct.induction_on with
+  | zero => exact ⟨⊥, fg_bot, zero_le _, 0, rfl⟩
+  | tmul i m => exact ⟨R ∙ i.val, fg_span_singleton i.val,
+      (span_singleton_le_iff_mem _ _).mpr i.property,
+      ⟨i.val, mem_span_singleton_self _⟩ ⊗ₜ[R] m, rfl⟩
+  | add x₁ x₂ ihx₁ ihx₂ =>
+    obtain ⟨J₁, hfg₁, hle₁, y₁, rfl⟩ := ihx₁
+    obtain ⟨J₂, hfg₂, hle₂, y₂, rfl⟩ := ihx₂
+    refine ⟨J₁ ⊔ J₂, hfg₁.sup hfg₂, sup_le hle₁ hle₂,
+      rTensor M (J₁.inclusion (le_sup_left : J₁ ≤ J₁ ⊔ J₂)) y₁ +
+        rTensor M (J₂.inclusion (le_sup_right : J₂ ≤ J₁ ⊔ J₂)) y₂, ?_⟩
+    rewrite [map_add, ← rTensor_comp_apply, ← rTensor_comp_apply]
+    rfl
+
 end Submodule
 
 namespace Submodule

Mathlib/RingTheory/Flat.lean

@@ -93,11 +93,14 @@ instance self (R : Type u) [CommRing R] : Flat R R :=
 
 variable (M : Type v) [AddCommGroup M] [Module R M]
 
+/-- An `R`-module `M` is flat iff for all finitely generated ideals `I` of `R`, the
+tensor product of the inclusion `I → R` and the identity `M → M` is injective. See
+`iff_rTensor_injective'` to extend to all ideals `I`. --/
 lemma iff_rTensor_injective :
-    Flat R M ↔ (∀ ⦃I : Ideal R⦄ (_ : I.FG), Injective (rTensor M I.subtype)) := by
-  have aux : ∀ (I : Ideal R), ((TensorProduct.lid R M).comp (rTensor M I.subtype)) =
-    (TensorProduct.lift ((lsmul R M).comp I.subtype))
-  · intro I; apply TensorProduct.ext'; intro x y; simp
+    Flat R M ↔ ∀ ⦃I : Ideal R⦄ (_ : I.FG), Injective (rTensor M I.subtype) := by
+  have aux : ∀ I : Ideal R, (TensorProduct.lid R M).comp (rTensor M I.subtype) =
+      TensorProduct.lift ((lsmul R M).comp I.subtype) := by
+    intro I; apply TensorProduct.ext'; intro x y; simp
   constructor
   · intro F I hI
     erw [← Equiv.comp_injective _ (TensorProduct.lid R M).toEquiv]
@@ -110,6 +113,21 @@ lemma iff_rTensor_injective :
     rw [← aux]
     simp [h₁ hI]
 
+/-- An `R`-module `M` is flat iff for all ideals `I` of `R`, the tensor product of the
+inclusion `I → R` and the identity `M → M` is injective. See `iff_rTensor_injective` to
+restrict to finitely generated ideals `I`. --/
+theorem iff_rTensor_injective' :
+    Flat R M ↔ ∀ I : Ideal R, Injective (rTensor M I.subtype) := by
+  rewrite [Flat.iff_rTensor_injective]
+  refine ⟨fun h I => ?_, fun h I _ => h I⟩
+  letI : AddCommGroup (I ⊗[R] M) := inferInstance -- Type class reminder
+  rewrite [injective_iff_map_eq_zero]
+  intro x hx₀
+  obtain ⟨J, hfg, hle, y, rfl⟩ := exists_fg_le_eq_rTensor_inclusion x
+  rewrite [← rTensor_comp_apply] at hx₀
+  letI : AddCommGroup (J ⊗[R] M) := inferInstance -- Type class reminder
+  rw [(injective_iff_map_eq_zero _).mp (h hfg) y hx₀, _root_.map_zero]
+
 variable (N : Type w) [AddCommGroup N] [Module R N]
 
 /-- A retract of a flat `R`-module is flat. -/