Local criterion for flatness

In algebra, the local criterion for flatness gives conditions one can check to show flatness of a module.
Statement.
Given a commutative ring "A", an ideal "I" and an "A"-module "M", suppose either
or
Then the following are equivalent:
The assumption that “"A" is a Noetherian ring” is used to invoke the Artin–Rees lemma and can be weakened; see 
Proof.
Following SGA 1, Exposé IV, we first prove a few lemmas, which are interesting themselves. (See also this blog post by Akhil Mathew for a proof of a special case.)
"Proof": The equivalence of the first two can be seen by studying the Tor spectral sequence. Here is a direct proof: if 1. is valid and formula_3 is an injection of formula_4-modules with cokernel "C", then, as "A"-modules,
Since formula_6 and the same for formula_7, this proves 2. Conversely, considering formula_8 where "F" is "B"-free, we get:
Here, the last map is injective by flatness and that gives us 1. To see the "Moreover" part, if 1. is valid, then formula_10 and so
By descending induction, this implies 3. The converse is trivial. formula_12
"Proof": The assumption implies that formula_13 and so, since tensor product commutes with base extension,
For the second part, let formula_15 denote the exact sequence formula_16 and formula_17. Consider the exact sequence of complexes:
Then formula_19 (it is so for large formula_20 and then use descending induction). 3. of Lemma 1 then implies that formula_21 is flat. formula_12
"Proof of the main statement".
formula_23: If formula_24 is nilpotent, then, by Lemma 1, formula_25 and formula_21 is flat over formula_27. Thus, assume that the first assumption is valid. Let formula_28 be an ideal and we shall show formula_29 is injective. For an integer formula_30, consider the exact sequence
Since formula_32 by Lemma 1 (note formula_33 kills formula_34), tensoring the above with formula_21, we get:
Tensoring formula_21 with formula_38, we also have:
We combine the two to get the exact sequence:
Now, if formula_41 is in the kernel of formula_29, then, a fortiori, formula_41 is in formula_44. By the Artin–Rees lemma, given formula_45, we can find formula_30 such that formula_47. Since formula_48, we conclude formula_49.
formula_50 follows from Lemma 2.
formula_51: Since formula_52, the condition 4. is still valid with formula_53 replaced by formula_54. Then Lemma 2 says that formula_55 is flat over formula_56.
formula_57 Tensoring formula_58 with "M", we see formula_59 is the kernel of formula_60. Thus, the implication is established by an argument similar to that of formula_23formula_12
Application: characterization of an étale morphism.
The local criterion can be used to prove the following:
"Proof": Assume that formula_63 is an isomorphism and we show "f" is étale. First, since formula_64 is faithfully flat (in particular is a pure subring), we have:
Hence, formula_66 is unramified (separability is trivial). Now, that formula_67 is flat follows from (1) the assumption that the induced map on completion is flat and (2) the fact that flatness descends under faithfully flat base change (it shouldn’t be hard to make sense of (2)).
Next, we show the converse: by the local criterion, for each "n", the natural map formula_68
is an isomorphism. By induction and the five lemma, this implies formula_69 is an isomorphism for each "n". Passing to limit, we get the asserted isomorphism. formula_12
Mumford’s Red Book gives an extrinsic proof of the above fact (Ch. III, § 5, Theorem 3).
Miracle flatness theorem.
B. Conrad calls the next theorem "the miracle flatness theorem".