Free modules with an exhaustive filtration by free subquotients #
Let N 0 ≤ N 1 ≤ ⋯ be an increasing sequence of submodules of M, starting at ⊥ and with
supremum ⊤. If every subquotient N (j + 1) ⧸ N j is free, then M is free. Splitting each
subquotient off N (j + 1) identifies M with the direct sum of the subquotients.
No finiteness is assumed: this is the form needed when a module that is not finitely generated over the base, such as a polynomial ring, is filtered by degree.
Main declarations #
Module.Free.of_filtration: a module with an exhaustive filtration by free subquotients is free.
theorem
Module.Free.of_filtration
{R : Type u_1}
{M : Type u_2}
[Ring R]
[AddCommGroup M]
[Module R M]
(N : ℕ → Submodule R M)
(hN : Monotone N)
(h0 : N 0 = ⊥)
(htop : ⨆ (j : ℕ), N j = ⊤)
(hfree : ∀ (j : ℕ), Free R (↥(N (j + 1)) ⧸ (N j).submoduleOf (N (j + 1))))
:
Free R M
A module with an exhaustive increasing filtration ⊥ = N 0 ≤ N 1 ≤ ⋯, all of whose
subquotients N (j + 1) ⧸ N j are free, is free.