feat(RingTheory/Flat): free and projective modules over a CommRing …

…are flat (#7567)

Prove that flat modules are stable under retracts, isomorphisms and direct sums. Use this to deduce that free and projective modules are flat.
 


Co-authored-by: Robin Carlier <robin.carlier@ens-lyon.fr>
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

Mathlib/RingTheory/Flat.lean

@@ -4,6 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
 import Mathlib.RingTheory.Noetherian
+import Mathlib.Algebra.DirectSum.Module
+import Mathlib.Algebra.DirectSum.Finsupp
+import Mathlib.LinearAlgebra.DirectSum.TensorProduct
+import Mathlib.LinearAlgebra.FreeModule.Basic
+import Mathlib.Algebra.Module.Projective
 
 #align_import ring_theory.flat from "leanprover-community/mathlib"@"62c0a4ef1441edb463095ea02a06e87f3dfe135c"
 
@@ -23,6 +28,14 @@ This result is not yet formalised.
 
 * `Module.Flat`: the predicate asserting that an `R`-module `M` is flat.
 
+## Main theorems
+
+* `Module.Flat.of_retract`: retracts of flat modules are flat
+* `Module.Flat.of_linearEquiv`: modules linearly equivalent to a flat modules are flat
+* `Module.Flat.directSum`: arbitrary direct sums of flat modules are flat
+* `Module.Flat.of_free`: free modules are flat
+* `Module.Flat.of_projective`: projective modules are flat
+
 ## TODO
 
 * Show that tensoring with a flat module preserves injective morphisms.
@@ -46,13 +59,13 @@ This result is not yet formalised.
 -/
 
 
-universe u v
+universe u v w
 
 namespace Module
 
-open Function (Injective)
+open Function (Injective Surjective)
 
-open LinearMap (lsmul)
+open LinearMap (lsmul rTensor lTensor)
 
 open TensorProduct
 
@@ -64,7 +77,9 @@ class Flat (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M]
 
 namespace Flat
 
-open TensorProduct LinearMap Submodule
+variable (R : Type u) [CommRing R]
+
+open LinearMap Submodule
 
 instance self (R : Type u) [CommRing R] : Flat R R :=
   ⟨by
@@ -76,6 +91,120 @@ instance self (R : Type u) [CommRing R] : Flat R R :=
       lift.tmul, Submodule.subtype_apply, Algebra.id.smul_eq_mul, lsmul_apply]⟩
 #align module.flat.self Module.Flat.self
 
+variable (M : Type v) [AddCommGroup M] [Module R M]
+
+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
+  constructor
+  · intro F I hI
+    erw [← Equiv.comp_injective _ (TensorProduct.lid R M).toEquiv]
+    have h₁ := F.out hI
+    rw [← aux] at h₁
+    refine h₁
+  · intro h₁
+    constructor
+    intro I hI
+    rw [← aux]
+    simp [h₁ hI]
+
+variable (N : Type w) [AddCommGroup N] [Module R N]
+
+/-- A retract of a flat `R`-module is flat. -/
+lemma of_retract [f : Flat R M] (i : N →ₗ[R] M) (r : M →ₗ[R] N) (h : r.comp i = LinearMap.id) :
+    Flat R N := by
+  rw [iff_rTensor_injective] at *
+  intro I hI
+  have h₁ : Function.Injective (lTensor R i)
+  · apply Function.RightInverse.injective (g := (lTensor R r))
+    intro x
+    rw [← LinearMap.comp_apply, ← lTensor_comp, h]
+    simp
+  rw [← Function.Injective.of_comp_iff h₁ (rTensor N I.subtype), ← LinearMap.coe_comp]
+  rw [LinearMap.lTensor_comp_rTensor, ←LinearMap.rTensor_comp_lTensor]
+  rw [LinearMap.coe_comp, Function.Injective.of_comp_iff (f hI)]
+  apply Function.RightInverse.injective (g := lTensor _ r)
+  intro x
+  rw [← LinearMap.comp_apply, ← lTensor_comp, h]
+  simp
+
+/-- A `R`-module linearly equivalent to a flat `R`-module is flat. -/
+lemma of_linearEquiv [f : Flat R M] (e : N ≃ₗ[R] M) : Flat R N := by
+  have h : e.symm.toLinearMap.comp e.toLinearMap = LinearMap.id := by simp
+  exact of_retract _ _ _ e.toLinearMap e.symm.toLinearMap h
+
+end Flat
+
+namespace Flat
+
+open DirectSum LinearMap Submodule
+
+variable (R : Type u) [CommRing R]
+
+/-- A direct sum of flat `R`-modules is flat. -/
+instance directSum (ι : Type v) (M : ι → Type w) [(i : ι) → AddCommGroup (M i)]
+    [(i : ι) → Module R (M i)] [F : (i : ι) → (Flat R (M i))] : Flat R (⨁ i, M i) := by
+  classical
+  rw [iff_rTensor_injective]
+  intro I hI
+  rw [← Equiv.comp_injective _ (TensorProduct.lid R (⨁ i, M i)).toEquiv]
+  set η₁ := TensorProduct.lid R (⨁ i, M i)
+  set η := (fun i ↦ TensorProduct.lid R (M i))
+  set φ := (fun i ↦ rTensor (M i) I.subtype)
+  set π := (fun i ↦ component R ι (fun j ↦ M j) i)
+  set ψ := (TensorProduct.directSumRight R {x // x ∈ I} (fun i ↦ M i)).symm.toLinearMap with psi_def
+  set ρ := rTensor (⨁ i, M i) I.subtype
+  set τ := (fun i ↦ component R ι (fun j ↦ ({x // x ∈ I} ⊗[R] (M j))) i)
+  rw [← Equiv.injective_comp (TensorProduct.directSumRight _ _ _).symm.toEquiv]
+  rw [LinearEquiv.coe_toEquiv, ← LinearEquiv.coe_coe, ← LinearMap.coe_comp]
+  rw [LinearEquiv.coe_toEquiv, ← LinearEquiv.coe_coe, ← LinearMap.coe_comp]
+  rw [← psi_def, injective_iff_map_eq_zero ((η₁.comp ρ).comp ψ)]
+  have h₁ : ∀ (i : ι), (π i).comp ((η₁.comp ρ).comp ψ) = (η i).comp ((φ i).comp (τ i))
+  · intro i
+    apply DirectSum.linearMap_ext
+    intro j
+    apply TensorProduct.ext'
+    intro a m
+    simp only [coe_comp, LinearEquiv.coe_coe, Function.comp_apply, directSumRight_symm_lof_tmul,
+      rTensor_tmul, coeSubtype, lid_tmul, map_smul]
+    rw [DirectSum.component.of, DirectSum.component.of]
+    by_cases h₂ : j = i
+    · subst j; simp
+    · simp [h₂]
+  intro a ha; rw [DirectSum.ext_iff R]; intro i
+  have f := LinearMap.congr_arg (f:= (π i)) ha
+  erw [LinearMap.congr_fun (h₁ i) a] at f
+  rw [(map_zero (π i) : (π i) 0 = (0 : M i))] at f
+  have h₂ := (F i)
+  rw [iff_rTensor_injective] at h₂
+  have h₃ := h₂ hI
+  simp only [coe_comp, LinearEquiv.coe_coe, Function.comp_apply, AddEquivClass.map_eq_zero_iff,
+    h₃, LinearMap.map_eq_zero_iff] at f
+  simp [f]
+
+/-- Free `R`-modules over discrete types are flat. -/
+instance finsupp (ι : Type v) : Flat R (ι →₀ R) :=
+  let _ := Classical.decEq ι
+  of_linearEquiv R _ _ (finsuppLEquivDirectSum R R ι)
+
+variable (M : Type v) [AddCommGroup M] [Module R M]
+
+instance of_free [Free R M] : Flat R M := of_linearEquiv R _ _ (Free.repr R M)
+
+/-- A projective module with a discrete type of generator is flat -/
+lemma of_projective_surjective (ι : Type w) [Projective R M] (p : (ι →₀ R) →ₗ[R] M)
+    (hp : Surjective p) : Flat R M := by
+  have h := Module.projective_lifting_property p (LinearMap.id) hp
+  cases h with
+    | _ e he => exact of_retract R _ _ _ _ he
+
+instance of_projective [h : Projective R M] : Flat R M := by
+  rw [Module.projective_def'] at h
+  cases h with
+    | _ e he => exact of_retract R _ _ _ _ he
+
 end Flat
 
 end Module