The limit theorem for flatness at a finite stage

The ordinary-ring case of the limit theorem for flatness (EGA IV, 11.2.6.1): when R is a directed colimit of commutative rings Rᵢ and a finitely presented flat R-module arises by base change from a stage i₀, the base change to some finite stage j ≥ i₀ is already flat.

We work with the matrix form of Lazard's equational criterion. A finitely presented module is the cokernel of a presentation matrix K : Matrix (Fin n) (Fin m) A; such a cokernel is projective — equivalently flat, see the bridge below — precisely when K admits a certificate: a matrix T with K * T * K = K (projective_of_matrix_certificate and matrix_certificate_of_projective). A certificate is a finite system of ring equations, so it descends along a directed colimit of rings (exists_stage_matrix_certificate); the headline statement is exists_stage_projective.

The colimit is presented abstractly by DirectedColimitPresentation: a compatible cocone gᵢ : Rᵢ →+* R which is jointly surjective and detects equalities at a finite stage. Ring.DirectLimit provides these data via Ring.DirectLimit.exists_of and Ring.DirectLimit.of.zero_exact (module Mathlib.Algebra.Colimit.Ring, outside our import funnel), so the statements here apply to it directly.

The flatness bridge

Module.Flat lives in Mathlib.RingTheory.Flat.Basic, which is not reachable through RS.Common.MathlibDeps, so the statements here are phrased with Module.Projective. The translation to flatness is a pair of Mathlib lemmas for the consumer:

• Module.Flat.of_projective (Mathlib.RingTheory.Flat.Basic): projective modules are flat;
• Module.Flat.projective_of_finitePresentation (Mathlib.RingTheory.Flat.EquationalCriterion): a finitely presented flat module is projective.

With these, exists_stage_projective is the flatness statement: a finitely presented flat R-module presented by the base change of a stage-i₀ matrix is projective, its certificate descends to a stage j, and every module presented over Rⱼ by the pushed matrix — in particular the base change Rⱼ ⊗_{R_{i₀}} M_{i₀} — is projective, hence flat.

Lazard certificates

A module presented by the matrix K — the cokernel of K.mulVecLin : A^m →ₗ A^n — is projective exactly when K admits a matrix T with K * T * K = K. The two directions are projective_of_matrix_certificate and matrix_certificate_of_projective.

theorem RS.FlatLimit.matrix_eq_of_mulVecLin_eq {A : Type u_1} [CommRing A] {p q : ℕ} {K L : Matrix (Fin p) (Fin q) A} (h : K.mulVecLin = L.mulVecLin) : K = L

Matrices inducing the same linear map are equal.

theorem RS.FlatLimit.mulVecLin_ofCols_single {A : Type u_1} [CommRing A] {p q : ℕ} (t : Fin q → Fin p → A) (j : Fin q) : (Matrix.of fun (a : Fin p) (b : Fin q) => t b a).mulVecLin (Pi.single j 1) = t j

The matrix assembled from the prescribed columns t 0, …, t (q-1) sends the j-th basis vector to t j.

theorem RS.FlatLimit.projective_of_matrix_certificate {A : Type u_1} [CommRing A] {m n : ℕ} {M : Type u_2} [AddCommGroup M] [Module A M] {K : Matrix (Fin n) (Fin m) A} {π : (Fin n → A) →ₗ[A] M} (hsurj : Function.Surjective ⇑π) (hker : π.ker = K.mulVecLin.range) {T : Matrix (Fin m) (Fin n) A} (hT : K * T * K = K) : Module.Projective A M

One half of the matrix form of Lazard's criterion: a certificate K * T * K = K splits the presentation, so any module presented by K is a direct summand of A ^ n and therefore projective. Combined with Module.Flat.of_projective (outside the funnel) this shows certified modules are flat.

theorem RS.FlatLimit.matrix_certificate_of_projective {A : Type u_1} [CommRing A] {m n : ℕ} {M : Type u_2} [AddCommGroup M] [Module A M] [Module.Projective A M] {K : Matrix (Fin n) (Fin m) A} {π : (Fin n → A) →ₗ[A] M} (hsurj : Function.Surjective ⇑π) (hker : π.ker = K.mulVecLin.range) : ∃ (T : Matrix (Fin m) (Fin n) A), K * T * K = K

The other half of the matrix form of Lazard's criterion: a projective module presented by K yields a certificate K * T * K = K. Via Module.Flat.projective_of_finitePresentation (outside the funnel) the hypothesis holds for any finitely presented flat module.

Directed colimit presentations of a ring

The colimit R = colim Rᵢ enters only through three properties of the cocone gᵢ : Rᵢ →+* R: compatibility with the transition maps, joint surjectivity, and detection of equalities at a finite stage. Ring.DirectLimit satisfies all three.

structure RS.FlatLimit.DirectedColimitPresentation {ι : Type u_1} [Preorder ι] {F : ι → Type u_2} [(i : ι) → CommRing (F i)] (f : ⦃i j : ι⦄ → i ≤ j → F i →+* F j) (R : Type u_3) [CommRing R] : Type (max (max u_1 u_2) u_3)

A presentation of the commutative ring R as the directed colimit of the system F with transition maps f: a compatible cocone which is jointly surjective and detects equalities at a finite stage. These are the only properties of a filtered colimit of rings used by the limit theorem.

• toColim (i : ι) : F i →+* R

  The cocone maps from the stages to the colimit.

• compat ⦃i j : ι⦄ (h : i ≤ j) (x : F i) : (self.toColim j) ((f h) x) = (self.toColim i) x

  The cocone commutes with the transition maps.

• exhaustive (x : R) : ∃ (i : ι) (y : F i), (self.toColim i) y = x

  Every element of the colimit comes from some stage.

• eventuallyEq (i : ι) (x y : F i) : (self.toColim i) x = (self.toColim i) y → ∃ (j : ι) (h : i ≤ j), (f h) x = (f h) y

  An equality in the colimit holds at some later stage.

theorem RS.FlatLimit.DirectedColimitPresentation.exists_stage_family {ι : Type u_1} [Preorder ι] {F : ι → Type u_2} [(i : ι) → CommRing (F i)] [Nonempty ι] [IsDirectedOrder ι] {f : ⦃i j : ι⦄ → i ≤ j → F i →+* F j} {R : Type u_3} [CommRing R] (P : DirectedColimitPresentation f R) {κ : Type u_4} [Finite κ] (x : κ → R) : ∃ (i : ι) (y : κ → F i), ∀ (k : κ), (P.toColim i) (y k) = x k

Every finite family of elements of the colimit lifts jointly to a single stage.

theorem RS.FlatLimit.DirectedColimitPresentation.exists_stage_eq {ι : Type u_1} [Preorder ι] {F : ι → Type u_2} [(i : ι) → CommRing (F i)] [Nonempty ι] [IsDirectedOrder ι] {f : ⦃i j : ι⦄ → i ≤ j → F i →+* F j} {R : Type u_3} [CommRing R] (P : DirectedColimitPresentation f R) (hDS : DirectedSystem F fun (x x_1 : ι) (h : x ≤ x_1) => ⇑(f h)) {κ : Type u_4} [Finite κ] {i : ι} {a b : κ → F i} (hab : ∀ (k : κ), (P.toColim i) (a k) = (P.toColim i) (b k)) : ∃ (j : ι) (h : i ≤ j), ∀ (k : κ), (f h) (a k) = (f h) (b k)

Finitely many equalities holding in the colimit hold simultaneously at some common later stage.

theorem RS.FlatLimit.DirectedColimitPresentation.exists_stage_matrix {ι : Type u_1} [Preorder ι] {F : ι → Type u_2} [(i : ι) → CommRing (F i)] [Nonempty ι] [IsDirectedOrder ι] {f : ⦃i j : ι⦄ → i ≤ j → F i →+* F j} {R : Type u_3} [CommRing R] (P : DirectedColimitPresentation f R) {p q : ℕ} (X : Matrix (Fin p) (Fin q) R) : ∃ (i : ι) (Y : Matrix (Fin p) (Fin q) (F i)), Y.map ⇑(P.toColim i) = X

Every matrix over the colimit lifts to a matrix at some stage.

theorem RS.FlatLimit.DirectedColimitPresentation.exists_stage_matrix_eq {ι : Type u_1} [Preorder ι] {F : ι → Type u_2} [(i : ι) → CommRing (F i)] [Nonempty ι] [IsDirectedOrder ι] {f : ⦃i j : ι⦄ → i ≤ j → F i →+* F j} {R : Type u_3} [CommRing R] (P : DirectedColimitPresentation f R) (hDS : DirectedSystem F fun (x x_1 : ι) (h : x ≤ x_1) => ⇑(f h)) {p q : ℕ} {i : ι} {Xa Xb : Matrix (Fin p) (Fin q) (F i)} (h : Xa.map ⇑(P.toColim i) = Xb.map ⇑(P.toColim i)) : ∃ (j : ι) (hij : i ≤ j), Xa.map ⇑(f hij) = Xb.map ⇑(f hij)

An equality of matrices in the colimit holds at some later stage.

The limit theorem

theorem RS.FlatLimit.DirectedColimitPresentation.exists_stage_matrix_certificate {ι : Type u_1} [Preorder ι] [Nonempty ι] [IsDirectedOrder ι] {F : ι → Type u_2} [(i : ι) → CommRing (F i)] {f : ⦃i j : ι⦄ → i ≤ j → F i →+* F j} {R : Type u_3} [CommRing R] (P : DirectedColimitPresentation f R) (hDS : DirectedSystem F fun (x x_1 : ι) (h : x ≤ x_1) => ⇑(f h)) {m n : ℕ} {i₀ : ι} (K₀ : Matrix (Fin n) (Fin m) (F i₀)) (T : Matrix (Fin m) (Fin n) R) (hT : K₀.map ⇑(P.toColim i₀) * T * K₀.map ⇑(P.toColim i₀) = K₀.map ⇑(P.toColim i₀)) : ∃ (j : ι) (hij : i₀ ≤ j) (Tj : Matrix (Fin m) (Fin n) (F j)), K₀.map ⇑(f hij) * Tj * K₀.map ⇑(f hij) = K₀.map ⇑(f hij)

Certificates descend to a finite stage: when the base change to the colimit of a stage-i₀ presentation matrix admits a certificate over R, its base change to some finite stage j ≥ i₀ admits a certificate over F j. This is the equational heart of the limit theorem for flatness: the certificate is a finite system of ring equations, its entries live at a finite stage, and the equations hold at a further stage.

theorem RS.FlatLimit.DirectedColimitPresentation.exists_stage_projective {ι : Type u_1} [Preorder ι] [Nonempty ι] [IsDirectedOrder ι] {F : ι → Type u_2} [(i : ι) → CommRing (F i)] {f : ⦃i j : ι⦄ → i ≤ j → F i →+* F j} {R : Type u_3} [CommRing R] (P : DirectedColimitPresentation f R) (hDS : DirectedSystem F fun (x x_1 : ι) (h : x ≤ x_1) => ⇑(f h)) {m n : ℕ} {i₀ : ι} (K₀ : Matrix (Fin n) (Fin m) (F i₀)) {M : Type u_4} [AddCommGroup M] [Module R M] [Module.Projective R M] {π : (Fin n → R) →ₗ[R] M} (hsurj : Function.Surjective ⇑π) (hker : π.ker = (K₀.map ⇑(P.toColim i₀)).mulVecLin.range) : ∃ (j : ι) (hij : i₀ ≤ j), ∀ (N : Type u_5) [inst : AddCommGroup N] [inst_1 : Module (F j) N] (ρ : (Fin n → F j) →ₗ[F j] N), Function.Surjective ⇑ρ → ρ.ker = (K₀.map ⇑(f hij)).mulVecLin.range → Module.Projective (F j) N

The limit theorem for flatness, projective form (the ordinary-ring case of EGA IV, 11.2.6.1). Let R be a directed colimit of the commutative rings F i and let M be a projective R-module presented by the base change of a stage-i₀ matrix K₀ — for instance a finitely presented flat module arising by base change from a finitely presented module at stage i₀, via Module.Flat.projective_of_finitePresentation. Then there is a stage j ≥ i₀ at which every module presented by the pushed matrix K₀.map (f hij) — in particular the base change F j ⊗_{F i₀} M_{i₀}, whose presentation matrix it is by right exactness of the tensor product — is projective, hence flat via Module.Flat.of_projective.