feat(RingTheory/Flat): flat is stable under base change (#11614)

Shows that `Module.Flat` is stable under arbitrary base change of rings. Also adds the corresponding version for `Algebra.Flat`.

Author: chrisflav

Mathlib/RingTheory/Flat/Algebra.lean

@@ -37,14 +37,26 @@ attribute [instance] out
 instance self (R : Type u) [CommRing R] : Algebra.Flat R R where
   out := Module.Flat.self R
 
-variable (R : Type u) (S : Type v) (T : Type w) [CommRing R] [CommRing S] [CommRing T]
+variable (R : Type u) (S : Type v) [CommRing R] [CommRing S]
 
 /-- If `T` is a flat `S`-algebra and `S` is a flat `R`-algebra,
 then `T` is a flat `R`-algebra. -/
-theorem comp [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T]
-    [Algebra.Flat R S] [Algebra.Flat S T] : Algebra.Flat R T where
+theorem comp (T : Type w) [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T]
+    [IsScalarTower R S T] [Algebra.Flat R S] [Algebra.Flat S T] : Algebra.Flat R T where
   out := Module.Flat.comp R S T
 
+/-- If `S` is a flat `R`-algebra and `T` is any `R`-algebra,
+then `T ⊗[R] S` is a flat `T`-algebra. -/
+instance baseChange (T : Type w) [CommRing T] [Algebra R S] [Algebra R T] [Algebra.Flat R S] :
+    Algebra.Flat T (T ⊗[R] S) where
+  out := Module.Flat.baseChange R T S
+
+/-- A base change of a flat algebra is flat. -/
+theorem isBaseChange [Algebra R S] (R' : Type w) (S' : Type t) [CommRing R'] [CommRing S']
+    [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S']
+    [IsScalarTower R S S'] [h : IsPushout R S R' S'] [Algebra.Flat R R'] : Algebra.Flat S S' where
+  out := Module.Flat.isBaseChange R S R' S' h.out
+
 end Algebra.Flat
 
 /-- A `RingHom` is flat if `R` is flat as an `S` algebra. -/

Mathlib/RingTheory/Flat/Stability.lean

@@ -4,26 +4,24 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Christian Merten
 -/
 import Mathlib.RingTheory.Flat.Basic
+import Mathlib.RingTheory.IsTensorProduct
 import Mathlib.LinearAlgebra.TensorProduct.Tower
 
 /-!
 # Flatness is stable under composition and base change
 
-We show that flatness is stable under composition and base change. The latter is not formalized yet.
+We show that flatness is stable under composition and base change.
 
 ## Main theorems
 
 * `Module.Flat.comp`: if `S` is a flat `R`-algebra and `M` is a flat `S`-module,
                       then `M` is a flat `R`-module
-
-## TODO
-
-* Show that flatness is stable under base change, i.e. if `S` is any `R`-algebra and `M` is a flat
-  `R`-module, then `M ⊗[R] S` is a flat `S`-module.
+* `Module.Flat.baseChange`: if `M` is a flat `R`-module and `S` is any `R`-algebra,
+                            then `S ⊗[R] M` is `S`-flat.
 
 -/
 
-universe u v w
+universe u v w t
 
 open Function (Injective Surjective)
 
@@ -33,6 +31,8 @@ open TensorProduct
 
 namespace Module.Flat
 
+section Composition
+
 /-! ### Composition
 
 Let `R` be a ring, `S` a flat `R`-algebra and `M` a flat `S`-module. To show that `M` is flat
@@ -93,4 +93,56 @@ theorem comp [Module.Flat R S] [Module.Flat S M] : Module.Flat R M := by
     LinearEquiv.coe_coe, EquivLike.comp_injective, EquivLike.injective_comp]
   exact (Module.Flat.iff_lTensor_injective' S M).mp inferInstance _
 
+end Composition
+
+section BaseChange
+
+/-! ### Base change
+
+Let `R` be a ring, `M` a flat `R`-module and `S` an `R`-algebra. To show that
+`S ⊗[R] M` is `S`-flat, we consider for an ideal `I` in `S` the composition of natural maps
+
+`I ⊗[S] (S ⊗[R] M) ≃ I ⊗[R] M → S ⊗[R] M ≃ S ⊗[S] (S ⊗[R] M)`.
+
+One checks that this composition is precisely the inclusion `I → S` tensored on the right
+with `S ⊗[R] M` and that the former is injective (note that `I ⊗[R] M → S ⊗[R] M` is
+injective, since `M` is `R`-flat).
+
+-/
+
+variable (R : Type u) (S : Type v) (M : Type w)
+  [CommRing R] [CommRing S] [Algebra R S]
+  [AddCommGroup M] [Module R M]
+
+private noncomputable abbrev auxRTensorBaseChange (I : Ideal S) :
+    I ⊗[S] (S ⊗[R] M) →ₗ[S] S ⊗[S] (S ⊗[R] M) :=
+  letI e1 : I ⊗[S] (S ⊗[R] M) ≃ₗ[S] I ⊗[R] M :=
+    AlgebraTensorModule.cancelBaseChange R S S I M
+  letI e2 : S ⊗[S] (S ⊗[R] M) ≃ₗ[S] S ⊗[R] M :=
+    AlgebraTensorModule.cancelBaseChange R S S S M
+  letI f : I ⊗[R] M →ₗ[S] S ⊗[R] M := AlgebraTensorModule.map
+    (Submodule.subtype I) LinearMap.id
+  e2.symm.toLinearMap ∘ₗ f ∘ₗ e1.toLinearMap
+
+private lemma auxRTensorBaseChange_eq (I : Ideal S) :
+    auxRTensorBaseChange R S M I = rTensor (S ⊗[R] M) (Submodule.subtype I) := by
+  ext
+  simp
+
+/-- If `M` is a flat `R`-module and `S` is any `R`-algebra, `S ⊗[R] M` is `S`-flat. -/
+instance baseChange [Module.Flat R M] : Module.Flat S (S ⊗[R] M) := by
+  rw [Module.Flat.iff_rTensor_injective']
+  intro I
+  simp only [← auxRTensorBaseChange_eq, auxRTensorBaseChange, LinearMap.coe_comp,
+    LinearEquiv.coe_coe, EmbeddingLike.comp_injective, EquivLike.injective_comp]
+  exact rTensor_preserves_injective_linearMap (I.subtype : I →ₗ[R] S) Subtype.val_injective
+
+/-- A base change of a flat module is flat. -/
+theorem isBaseChange [Module.Flat R M] (N : Type t) [AddCommGroup N] [Module R N] [Module S N]
+    [IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) :
+    Module.Flat S N :=
+  of_linearEquiv S (S ⊗[R] M) N (IsBaseChange.equiv h).symm
+
+end BaseChange
+
 end Module.Flat