Flat and finitely presented modules

Stream: mathlib4

[Mitchell Lee]

It is a classic result of commutative algebra that if $M$ is a finitely presented module over a commutative ring $R$, then $M$ is flat over $R$ if and only if $M$ is locally free over $R$ (https://stacks.math.columbia.edu/tag/00NV). This result is part of the blueprint for Fermat's last theorem (https://imperialcollegelondon.github.io/FLT/blueprint/sect0003.html#finite_flat_group_scheme).

Note: The blueprint for FLT only uses this result in the case that $R$ is Noetherian and $M$ is a finite Hopf algebra over $R$. But I think it isn't any more difficult to prove it in greater generality than that. I am not going to worry, for now, about proving that a finitely presented flat module is projective.

I opened a pull request to the FLT repository that states this result (https://github.com/ImperialCollegeLondon/FLT/pull/32/files). However, I now think that it would be better to close that pull request and try to add this result to mathlib directly. My current idea is to start by defining a version of docs#LocalizationPreserves for modules instead of algebras, and then to define what it means for a predicate on modules to hold locally at a prime $\mathfrak{p}$, locally, or stalkwise.

However, I am very unfamiliar with the commutative algebra and algebraic geometry part of mathlib, so I would welcome some advice.

Here is my outline in way too much detail. For now, it seems best to entirely avoid category theory.

Outline

• Define FinitelyPresented as a predicate.
• Define localization of a homomorphism of $R$-modules.
• Let f be a homomorphism of $R$-modules. Then the kernel of its localization equals the localization of its kernel. (This is really an equality and not just an isomorphism. The "localization" on the right hand side of this equation is docs#Submodule.localized.)
• Also, the image of its localization equals the localization of its image. (Again, this is really an equality.)
• Localization of tensor product is tensor product of localizations. (I am not sure how best to even state this.)
• Make a version of docs#LocalizationPreserves for modules instead of algebras.
• Localization preserves Trivial.
• Localization preserves Free.
• Localization preserves Flat.
• Localization preserves Finite.
• Localization preserves FinitelyPresented.
• For any predicate P on modules, let us say that Locally P R M if there is an open cover of $\operatorname{Spec}(R)$ by basic open sets $D(f_i)$ such that for all $i$, we have that $M_{f_i}$ satisfies the predicate P as an $R_{f_i}$-module.
• Equivalently, every prime ideal $\mathfrak{p}$ is contained in a basic open set $D(f_i)$ such that $M_{f_i}$ satisfies the predicate P as an $R_{f_i}$-module.
• For any predicate P on modules, let us say that Stalkwise P R M if $M_{\mathfrak{p}}$ satisfies the predicate P as a $R_{\mathfrak{p}}$-module for all $\mathfrak{p} \in \operatorname{Spec}(R)$.
• Also make a predicate similar to the above that only deals with the localization at maximal ideals. Not sure what to call it.
• If localizations preserve a predicate P, then P implies Locally P which implies Stalkwise P.
• Stalkwise (P ∧ Q) is equivalent to Stalkwise P ∧ Stalkwise Q.
• If localizations preserve P and Q, then Locally (P ∧ Q) is equivalent to Locally P ∧ Locally Q.
• Stalkwise Trivial implies Trivial.
• Stalkwise Finite implies Finite.
• Stalkwise FinitelyPresented implies FinitelyPresented.
• Stalkwise Flat implies Flat.
• If $M$ is finite and $M_{\mathfrak{p}} = 0$, then there exists a basic open set $D(f) \ni \mathfrak{p}$ such that $M_{f} = 0$.
• A homomorphism $R^{\oplus m}_{\mathfrak{p}} \to M_{\mathfrak{p}}$ can be lifted to a basic open neighborhood of $\mathfrak{p}$.
• FinitelyPresented and Stalkwise Free imply Locally Free
• In a local ring, Flat and Finite imply Free.

[Antoine Chambert-Loir]

(step -4 seems to require that $M$ is finitely generated)

[Mitchell Lee]

Yes, thanks.

[Antoine Chambert-Loir]

Iirc, the analogue of stalkwise for maximal ideals is sometimes called punctually. (Eg, by Daniel Lazard)

[Antoine Chambert-Loir]

One thing that might being worthwhile is stating/proving this result in the language of algebraic geometry, to make use (and simultaneously develop) the API for schemes. In this direction, step -3 says something about morphisms of of quasi coherent sheaves.

[Antoine Chambert-Loir]

But one can wish to go in the opposite direction and prove these results as fast as possible.

[Antoine Chambert-Loir]

In a yet different direction, thinking of including the noncommutative case is also interesting (and possibly enlightening).

[Mitchell Lee]

Do you have a reference for the noncommutative case?

[Antoine Chambert-Loir]

I'd have a look at Lam's book.

[Mitchell Lee]

Also, I mostly just figured that you had to prove most of this stuff for modules over a ring first, and then you can deduce the corresponding facts about quasicoherent sheaves from that. But maybe that's not true.

[Antoine Chambert-Loir]

There is a way to take opportunity of the language of schemes to prove the results for rings. I don't know whether mathlib knows about qcoh sheaves yet, even on affine schemes.

[Joël Riou]

I think that the focus could be first on the equivalence between flat + finitely presented and projective. (And for this, the standard proof uses the Hom(-, Q/Z) duality.) Then, of course, the stabilitiy of these notions with localization is important, as well as flat iff the stalks are flat. Yet, some of the statement should be formulated in the language of schemes (but we do not have the API for this yet).

[Christian Merten]

For the first two bullet points: see docs#Module.FinitePresentation and docs#IsLocalizedModule.map. For localizations and tensorproduct there is docs#isLocalizedModule_iff_isBaseChange which might cover some of what you want and might serve as an example how to state it.

[Christian Merten]

Joël Riou said:

I think that the focus could be first on the equivalence between flat + finitely presented and projective. (And for this, the standard proof uses the Hom(-, Q/Z) duality.) Then, of course, the stabilitiy of these notions with localization is important, as well as flat iff the stalks are flat. Yet, some of the statement should be formulated in the language of schemes (but we do not have the API for this yet).

Is there anything general to say about when a property of a morphism of schemes (say defined in terms of docs#AlgebraicGeometry.affineLocally) can be checked on stalks?

[Mitchell Lee]

Joël Riou said:

I think that the focus could be first on the equivalence between flat + finitely presented and projective. (And for this, the standard proof uses the Hom(-, Q/Z) duality.) Then, of course, the stabilitiy of these notions with localization is important, as well as flat iff the stalks are flat. Yet, some of the statement should be formulated in the language of schemes (but we do not have the API for this yet).

Rather than prove that flat and finitely presented implies projective directly, it seems to me that it'd be easier to prove that flat and finitely presented implies locally free, and then prove that locally free implies projective (as the Stacks project does). Is the issue that this doesn't work over a noncommutative ring?

[Kevin Buzzard]

(just to say that it's definitely a good idea to put this directly into mathlib rather than via the FLT repo! I would like to minimise the size of FLT)

[Joël Riou]

Mitchell Lee said:

Rather than prove that flat and finitely presented implies projective directly, it seems to me that it'd be easier to prove that flat and finitely presented implies locally free, and then prove that locally free implies projective (as the Stacks project does). Is the issue that this doesn't work over a noncommutative ring?

I suggest not to follow the Stacks project here (which is consistent with Antoine's suggestion about thinking about the noncommutative case). If we denote * the Pontrjagin duality Hom(-, Q/Z), then if M and N are modules, with M of finite presentation, there is a natural iso $M ⊗ (N^*) ≅ Hom(M,N)^*$. As we want to show M is projective, we need to show that Hom(M,-) is exact, but as Pontrjagin duality reflects exact sequences, it suffices to show $Hom(M,-)^*$ is exact, which follows from the iso, the fact M is flat and the exactness of *.

Then, the rest would fit more in general algebraic geometry statements about quasi-coherent sheaves F: if F is finitely presented and the stalk at x is free, there exists a neighbourhood of x where F identifies to a direct sum of copies of the structure sheaf. (This would follow from a more general statement that if F and G are both finitely presented quasi-coherent sheaves, then an isomorphism between the stalks at x extends to an isomorphism in a neighbourhood of x. This is related to the computation of the stalks of the internal Hom(F,G) sheaf.)

[Andrew Yang]

The criterion "flat iff flat for fg-modules" is proved in mathlib using Pontrjagin duality and baer's criterion so we might have something similar already?

[Mitchell Lee]

One reason I think it could be nice to go from "flat" to "locally free" without going through "projective" first is the following: It can be proved that finite module is flat if and only if it is stalkwise free. There is no need to assume that the module is finitely presented in this step.

[Joël Riou]

If you also show Lazard's theorem (https://stacks.math.columbia.edu/tag/058G) en passant, that would be great.

[Mitchell Lee]

I'll start by showing that a finite flat module over a commutative local ring is free. As far as I can see, this, or something like it, should be necessary regardless of how much scheme theory is used in the rest of the proof.

I'll think about Lazard's theorem.

There already seems to be a PR that includes some homological properties of flat modules (#12438), but I think it's independent for now.

[Mitchell Lee]

After working on this for a few hours, I have realized that it's quite a bit harder to prove that a finite flat module over a local ring is free than to prove that a finitely presented flat module over a local ring is free. But I'm getting there.

[Joël Riou]

Yes, it seems the proof uses the "equational criterion" for flatness. (This is the reason why I asked about Lazard's theorem the proof of which also uses that criteria AFAIK.)

[Mitchell Lee]

I'm very close to proving the equational criterion for flatness. My progress is that I have proved the "equational criterion for vanishing": #12647.

I will try to finish the proof tomorrow.

[Mitchell Lee]

I hope that the proof that a finite flat module over a local ring is free will not take too long after that. Then, I guess the next step, if we want to do everything the "right way", is to define quasicoherent sheaves.

(I think Lazard's theorem should wait for #12438.)

(As for the noncommutative case, unfortunately tensor products of modules over noncommutative rings aren't even defined yet. Should this be a priority?)

[Kevin Buzzard]

I think it's becoming one!

[Mitchell Lee]

I proved the equational criterion for flatness: #12666

[Johan Commelin]

Great! @Mitchell Lee I left some comments on #12647

[Mitchell Lee]

Thank you!

[Junyan Xu]

I found that Section 3 of Facets of module theory over semirings (2024) proves the equational criterion as well as Lazard's theorem over semirings. Instead of "trivial relations" it talks about "rectifiable relations".
image.png
These results were already established in On Flat Semimodules over Semirings (2004) but maybe in a less familiar language.
Definition of flatness and finite presentation in mathlib would need to be modified to state these theorems. Flatness over semirings should say that tensoring preserves equalizers (or pullbacks, or all finite limits, since finite products are always preserved); my naive generalization (preservation of monomorphisms) in #19115 is strictly weaker, and I'll introduce a separate class MonoFlat (terminology in the 2004 paper) for it.
Finite presentation needs to state that the kernel (as an R-additive congruence) is finitely generated. This can be stated as: there is a Finset s such that the docs#addConGen of membership in R • s is the docs#AddCon.ker.