# Documentation

Mathlib.RingTheory.Finiteness

# Finiteness conditions in commutative algebra #

In this file we define a notion of finiteness that is common in commutative algebra.

## Main declarations #

• Submodule.FG, Ideal.FG These express that some object is finitely generated as submodule over some base ring.

• Module.Finite, RingHom.Finite, AlgHom.Finite all of these express that some object is finitely generated as module over some base ring.

## Main results #

• exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul is 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.
def Submodule.FG {R : Type u_1} {M : Type u_2} [] [] [Module R M] (N : ) :

A submodule of M is finitely generated if it is the span of a finite subset of M.

Instances For
theorem Submodule.fg_def {R : Type u_1} {M : Type u_2} [] [] [Module R M] {N : } :
S, = N
theorem Submodule.fg_iff_addSubmonoid_fg {M : Type u_2} [] (P : ) :
theorem Submodule.fg_iff_add_subgroup_fg {G : Type u_3} [] (P : ) :
theorem Submodule.fg_iff_exists_fin_generating_family {R : Type u_1} {M : Type u_2} [] [] [Module R M] {N : } :
n s, = N
theorem Submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul {R : Type u_3} [] {M : Type u_4} [] [Module R M] (I : ) (N : ) (hn : ) (hin : N I N) :
r, r - 1 I ∀ (n : M), n Nr n = 0

Nakayama's Lemma. Atiyah-Macdonald 2.5, Eisenbud 4.7, Matsumura 2.2, Stacks 00DV

theorem Submodule.exists_mem_and_smul_eq_self_of_fg_of_le_smul {R : Type u_3} [] {M : Type u_4} [] [Module R M] (I : ) (N : ) (hn : ) (hin : N I N) :
r, r I ∀ (n : M), n Nr n = n
theorem Submodule.fg_bot {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
theorem Subalgebra.fg_bot_toSubmodule {R : Type u_3} {A : Type u_4} [] [] [Algebra R A] :
Submodule.FG (Subalgebra.toSubmodule )
theorem Submodule.fg_unit {R : Type u_3} {A : Type u_4} [] [] [Algebra R A] (I : ()ˣ) :
theorem Submodule.fg_of_isUnit {R : Type u_3} {A : Type u_4} [] [] [Algebra R A] {I : } (hI : ) :
theorem Submodule.fg_span {R : Type u_1} {M : Type u_2} [] [] [Module R M] {s : Set M} (hs : ) :
theorem Submodule.fg_span_singleton {R : Type u_1} {M : Type u_2} [] [] [Module R M] (x : M) :
theorem Submodule.FG.sup {R : Type u_1} {M : Type u_2} [] [] [Module R M] {N₁ : } {N₂ : } (hN₁ : ) (hN₂ : ) :
Submodule.FG (N₁ N₂)
theorem Submodule.fg_finset_sup {R : Type u_1} {M : Type u_2} [] [] [Module R M] {ι : Type u_3} (s : ) (N : ι) (h : ∀ (i : ι), i sSubmodule.FG (N i)) :
theorem Submodule.fg_biSup {R : Type u_1} {M : Type u_2} [] [] [Module R M] {ι : Type u_3} (s : ) (N : ι) (h : ∀ (i : ι), i sSubmodule.FG (N i)) :
Submodule.FG (⨆ (i : ι) (_ : i s), N i)
theorem Submodule.fg_iSup {R : Type u_1} {M : Type u_2} [] [] [Module R M] {ι : Type u_3} [] (N : ι) (h : ∀ (i : ι), Submodule.FG (N i)) :
theorem Submodule.FG.map {R : Type u_1} {M : Type u_2} [] [] [Module R M] {P : Type u_3} [] [Module R P] (f : M →ₗ[R] P) {N : } (hs : ) :
theorem Submodule.fg_of_fg_map_injective {R : Type u_1} {M : Type u_2} [] [] [Module R M] {P : Type u_3} [] [Module R P] (f : M →ₗ[R] P) (hf : ) {N : } (hfn : ) :
theorem Submodule.fg_of_fg_map {R : Type u_4} {M : Type u_5} {P : Type u_6} [Ring R] [] [Module R M] [] [Module R P] (f : M →ₗ[R] P) (hf : ) {N : } (hfn : ) :
theorem Submodule.fg_top {R : Type u_1} {M : Type u_2} [] [] [Module R M] (N : ) :
theorem Submodule.fg_of_linearEquiv {R : Type u_1} {M : Type u_2} [] [] [Module R M] {P : Type u_3} [] [Module R P] (e : M ≃ₗ[R] P) (h : ) :
theorem Submodule.FG.prod {R : Type u_1} {M : Type u_2} [] [] [Module R M] {P : Type u_3} [] [Module R P] {sb : } {sc : } (hsb : ) (hsc : ) :
theorem Submodule.fg_pi {R : Type u_1} [] {ι : Type u_4} {M : ιType u_5} [] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {p : (i : ι) → Submodule R (M i)} (hsb : ∀ (i : ι), Submodule.FG (p i)) :
theorem Submodule.fg_of_fg_map_of_fg_inf_ker {R : Type u_4} {M : Type u_5} {P : Type u_6} [Ring R] [] [Module R M] [] [Module R P] (f : M →ₗ[R] P) {s : } (hs1 : ) (hs2 : Submodule.FG ()) :

If 0 → M' → M → M'' → 0 is exact and M' and M'' are finitely generated then so is M.

theorem Submodule.fg_induction (R : Type u_4) (M : Type u_5) [] [] [Module R M] (P : Prop) (h₁ : (x : M) → P (Submodule.span R {x})) (h₂ : (M₁ M₂ : ) → P M₁P M₂P (M₁ M₂)) (N : ) (hN : ) :
P N
theorem Submodule.fg_ker_comp {R : Type u_4} {M : Type u_5} {N : Type u_6} {P : Type u_7} [Ring R] [] [Module R M] [] [Module R N] [] [Module R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (hf1 : ) (hf2 : ) (hsur : ) :

The kernel of the composition of two linear maps is finitely generated if both kernels are and the first morphism is surjective.

theorem Submodule.fg_restrictScalars {R : Type u_4} {S : Type u_5} {M : Type u_6} [] [] [Algebra R S] [] [Module S M] [Module R M] [] (N : ) (hfin : ) (h : ) :
theorem Submodule.FG.stablizes_of_iSup_eq {R : Type u_1} {M : Type u_2} [] [] [Module R M] {M' : } (hM' : ) (N : →o ) (H : iSup N = M') :
n, M' = N n
theorem Submodule.fg_iff_compact {R : Type u_1} {M : Type u_2} [] [] [Module R M] (s : ) :

Finitely generated submodules are precisely compact elements in the submodule lattice.

theorem Submodule.FG.map₂ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [] [] [] [] [Module R M] [Module R N] [Module R P] (f : M →ₗ[R] N →ₗ[R] P) {p : } {q : } (hp : ) (hq : ) :
theorem Submodule.FG.mul {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {M : } {N : } (hm : ) (hn : ) :
theorem Submodule.FG.pow {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {M : } (h : ) (n : ) :
def Ideal.FG {R : Type u_1} [] (I : ) :

An ideal of R is finitely generated if it is the span of a finite subset of R.

This is defeq to Submodule.FG, but unfolds more nicely.

Instances For
theorem Ideal.FG.map {R : Type u_3} {S : Type u_4} [] [] {I : } (h : ) (f : R →+* S) :

The image of a finitely generated ideal is finitely generated.

This is the Ideal version of Submodule.FG.map.

theorem Ideal.fg_ker_comp {R : Type u_3} {S : Type u_4} {A : Type u_5} [] [] [] (f : R →+* S) (g : S →+* A) (hf : ) (hg : ) (hsur : ) :
theorem Ideal.exists_radical_pow_le_of_fg {R : Type u_3} [] (I : ) (h : ) :
n, I
class Module.Finite (R : Type u_1) (M : Type u_4) [] [] [Module R M] :
• out :

A module over a semiring is Finite if it is finitely generated as a module.

A module over a semiring is Finite if it is finitely generated as a module.

Instances
theorem Module.finite_def {R : Type u_6} {M : Type u_7} [] [] [Module R M] :
theorem Module.Finite.exists_fin {R : Type u_1} {M : Type u_4} [] [] [Module R M] [] :
n s, =

See also Module.Finite.exists_fin'.

theorem Module.Finite.exists_fin' (R : Type u_6) (M : Type u_7) [] [] [Module R M] [] :
n f,
theorem Module.Finite.of_surjective {R : Type u_1} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] [hM : ] (f : M →ₗ[R] N) (hf : ) :
instance Module.Finite.range {R : Type u_1} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] [] (f : M →ₗ[R] N) :
Module.Finite R { x // }

The range of a linear map from a finite module is finite.

instance Module.Finite.map {R : Type u_1} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] (p : ) [Module.Finite R { x // x p }] (f : M →ₗ[R] N) :
Module.Finite R { x // x }

Pushforwards of finite submodules are finite.

instance Module.Finite.self (R : Type u_1) [] :
theorem Module.Finite.of_restrictScalars_finite (R : Type u_6) (A : Type u_7) (M : Type u_8) [] [] [] [Module R M] [Module A M] [Algebra R A] [] [hM : ] :
instance Module.Finite.prod {R : Type u_1} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] [hM : ] [hN : ] :
instance Module.Finite.pi {R : Type u_1} [] {ι : Type u_6} {M : ιType u_7} [] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [h : ∀ (i : ι), Module.Finite R (M i)] :
Module.Finite R ((i : ι) → M i)
theorem Module.Finite.equiv {R : Type u_1} {M : Type u_4} {N : Type u_5} [] [] [Module R M] [] [Module R N] [] (e : M ≃ₗ[R] N) :
instance Module.Finite.ulift {R : Type u_1} {M : Type u_4} [] [] [Module R M] [] :
theorem Module.Finite.trans {R : Type u_6} (A : Type u_7) (M : Type u_8) [] [] [Algebra R A] [] [Module R M] [Module A M] [] [] [] :

Instances For
instance Module.Finite.base_change (R : Type u_1) (A : Type u_2) (M : Type u_4) [] [] [Algebra R A] [] [Module R M] [h : ] :
instance Module.Finite.tensorProduct (R : Type u_1) (M : Type u_4) (N : Type u_5) [] [] [Module R M] [] [Module R N] [hM : ] [hN : ] :
def RingHom.Finite {A : Type u_1} {B : Type u_2} [] [] (f : A →+* B) :

A ring morphism A →+* B is Finite if B is finitely generated as A-module.

Instances For
theorem RingHom.Finite.id (A : Type u_1) [] :
theorem RingHom.Finite.of_surjective {A : Type u_1} {B : Type u_2} [] [] (f : A →+* B) (hf : ) :
theorem RingHom.Finite.comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [] [] [] {g : B →+* C} {f : A →+* B} (hg : ) (hf : ) :
theorem RingHom.Finite.of_comp_finite {A : Type u_1} {B : Type u_2} {C : Type u_3} [] [] [] {f : A →+* B} {g : B →+* C} (h : ) :
def AlgHom.Finite {R : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :

An algebra morphism A →ₐ[R] B is finite if it is finite as ring morphism. In other words, if B is finitely generated as A-module.

Instances For
theorem AlgHom.Finite.id (R : Type u_1) (A : Type u_2) [] [] [Algebra R A] :
theorem AlgHom.Finite.comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [] [] [] [] [Algebra R A] [Algebra R B] [Algebra R C] {g : B →ₐ[R] C} {f : A →ₐ[R] B} (hg : ) (hf : ) :
theorem AlgHom.Finite.of_surjective {R : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : ) :
theorem AlgHom.Finite.of_comp_finite {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [] [] [] [] [Algebra R A] [Algebra R B] [Algebra R C] {f : A →ₐ[R] B} {g : B →ₐ[R] C} (h : AlgHom.Finite ()) :