A finite product of flat modules is flat, and when it is faithfully flat

Mathlib knows that an arbitrary direct sum of flat modules is flat (Module.Flat.directSum), but ∀ i, M i is not definitionally a direct sum, so nothing fires for a product. Over a finite index the two agree, and this file records the resulting instance together with the criterion that upgrades it to faithful flatness.

Mathlib defines Module.FaithfullyFlat as flatness plus m • ⊤ ≠ ⊤ for every maximal ideal m, so the criterion is about locating a single component that keeps m proper — the factorwise half of that is Ideal.smul_top_eq_top_of_pi, a general ideal-action fact with no flatness or finiteness in it, which lives in TauCeti/RingTheory/Ideal/Operations.lean: a product is faithfully flat as soon as each factor is flat and no maximal ideal expands in every factor at once. Individually the factors may all fail to be faithfully flat.

Main results

• Module.Flat.pi: a finite product of flat modules is flat.
• Module.FaithfullyFlat.pi_of_exists_submodule_ne_top: a finite product of flat modules is faithfully flat as soon as every maximal ideal stays proper in some factor.
• Module.FaithfullyFlat.pi_of_faithfullyFlat: the special case of one distinguished faithfully flat factor.
• Module.FaithfullyFlat.pi: a finite nonempty product of faithfully flat modules.

Implementation notes

Module.FaithfullyFlat.pi asks [Nonempty ι], and that is not slack: for ι empty the product is the trivial module, in which m • ⊤ = ⊤ = ⊥ for every m, so it is faithfully flat over no nonzero ring at all — while ∀ i, FaithfullyFlat R (M i) holds vacuously. Dropping the hypothesis would make the instance false. Flatness has no such caveat: the trivial module is flat.

The finiteness is not an artefact of the comparison used here: by Chase's theorem a ring is coherent exactly when every product of flat modules is flat, so over a non-coherent ring the statement fails outright for a large enough index. Nothing is lost over a noetherian base, but the hypothesis cannot simply be dropped.

instance Module.Flat.pi {R : Type u_1} {ι : Type u_2} {M : ι → Type u_3} [CommSemiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [Finite ι] [∀ (i : ι), Flat R (M i)] : Flat R ((i : ι) → M i)

A finite product of flat modules is flat. The finiteness is essential; see the module docstring.

theorem Module.FaithfullyFlat.pi_of_exists_submodule_ne_top {R : Type u_1} {ι : Type u_2} {M : ι → Type u_3} [CommRing R] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [Finite ι] [∀ (i : ι), Flat R (M i)] (h : ∀ (m : Ideal R), m.IsMaximal → ∃ (i : ι), m • ⊤ ≠ ⊤) : FaithfullyFlat R ((i : ι) → M i)

A finite product of flat modules is faithfully flat as soon as no maximal ideal expands every factor at once. Each individual factor may fail to be faithfully flat; what is needed is that the failures are not simultaneous.

theorem Module.FaithfullyFlat.pi_of_faithfullyFlat {R : Type u_1} {ι : Type u_2} {M : ι → Type u_3} [CommRing R] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [Finite ι] [∀ (i : ι), Flat R (M i)] (j : ι) [FaithfullyFlat R (M j)] : FaithfullyFlat R ((i : ι) → M i)

One faithfully flat factor carries a finite product of flat modules. This is the special case of FaithfullyFlat.pi_of_exists_submodule_ne_top where one fixed index works for every maximal ideal; when no single factor does, that criterion is the one to use.

instance Module.FaithfullyFlat.pi {R : Type u_1} {ι : Type u_2} {M : ι → Type u_3} [CommRing R] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [Nonempty ι] [Finite ι] [∀ (i : ι), FaithfullyFlat R (M i)] : FaithfullyFlat R ((i : ι) → M i)

A finite nonempty product of faithfully flat modules is faithfully flat. The emptiness hypothesis is essential; see the module docstring.