Finiteness conditions in commutative algebra #
In this file we define a notion of finiteness that is common in commutative algebra.
Main declarations #
Main results #
exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smulis Nakayama's lemma, in the following form: if N is a finitely generated submodule of an ambient R-module M and I is an ideal of R such that N ⊆ IN, then there exists r ∈ 1 + I such that rN = 0.
Nakayama's Lemma. Atiyah-Macdonald 2.5, Eisenbud 4.7, Matsumura 2.2, Stacks 00DV
If 0 → M' → M → M'' → 0 is exact and M' and M'' are finitely generated then so is M.
The kernel of the composition of two linear maps is finitely generated if both kernels are and the first morphism is surjective.
Pushforwards of finite submodules are finite.
Porting note: reminding Lean about this instance for Module.Finite.base_change