# mathlib3documentation

ring_theory.finiteness

# Finiteness conditions in commutative algebra #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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, ring_hom.finite, alg_hom.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} [semiring R] [ M] (N : M) :
Prop

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

Equations
theorem submodule.fg_def {R : Type u_1} {M : Type u_2} [semiring R] [ M] {N : M} :
N.fg (S : set M), S.finite = N
theorem submodule.fg_iff_add_submonoid_fg {M : Type u_2} (P : M) :
theorem submodule.fg_iff_exists_fin_generating_family {R : Type u_1} {M : Type u_2} [semiring R] [ M] {N : M} :
N.fg (n : ) (s : fin n M), (set.range s) = N
theorem submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] (I : ideal R) (N : M) (hn : N.fg) (hin : N I N) :
(r : R), r - 1 I (n : M), n N r 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_1} [comm_ring R] {M : Type u_2} [ M] (I : ideal R) (N : M) (hn : N.fg) (hin : N I N) :
(r : R) (H : r I), (n : M), n N r n = n
theorem submodule.fg_bot {R : Type u_1} {M : Type u_2} [semiring R] [ M] :
theorem subalgebra.fg_bot_to_submodule {R : Type u_1} {A : Type u_2} [semiring A] [ A] :
theorem submodule.fg_unit {R : Type u_1} {A : Type u_2} [semiring A] [ A] (I : A)ˣ) :
theorem submodule.fg_of_is_unit {R : Type u_1} {A : Type u_2} [semiring A] [ A] {I : A} (hI : is_unit I) :
I.fg
theorem submodule.fg_span {R : Type u_1} {M : Type u_2} [semiring R] [ M] {s : set M} (hs : s.finite) :
s).fg
theorem submodule.fg_span_singleton {R : Type u_1} {M : Type u_2} [semiring R] [ M] (x : M) :
{x}).fg
theorem submodule.fg.sup {R : Type u_1} {M : Type u_2} [semiring R] [ M] {N₁ N₂ : M} (hN₁ : N₁.fg) (hN₂ : N₂.fg) :
(N₁ N₂).fg
theorem submodule.fg_finset_sup {R : Type u_1} {M : Type u_2} [semiring R] [ M] {ι : Type u_3} (s : finset ι) (N : ι M) (h : (i : ι), i s (N i).fg) :
(s.sup N).fg
theorem submodule.fg_bsupr {R : Type u_1} {M : Type u_2} [semiring R] [ M] {ι : Type u_3} (s : finset ι) (N : ι M) (h : (i : ι), i s (N i).fg) :
( (i : ι) (H : i s), N i).fg
theorem submodule.fg_supr {R : Type u_1} {M : Type u_2} [semiring R] [ M] {ι : Type u_3} [finite ι] (N : ι M) (h : (i : ι), (N i).fg) :
(supr N).fg
theorem submodule.fg.map {R : Type u_1} {M : Type u_2} [semiring R] [ M] {P : Type u_3} [ P] (f : M →ₗ[R] P) {N : M} (hs : N.fg) :
N).fg
theorem submodule.fg_of_fg_map_injective {R : Type u_1} {M : Type u_2} [semiring R] [ M] {P : Type u_3} [ P] (f : M →ₗ[R] P) (hf : function.injective f) {N : M} (hfn : N).fg) :
N.fg
theorem submodule.fg_of_fg_map {R : Type u_1} {M : Type u_2} {P : Type u_3} [ring R] [ M] [ P] (f : M →ₗ[R] P) (hf : = ) {N : M} (hfn : N).fg) :
N.fg
theorem submodule.fg_top {R : Type u_1} {M : Type u_2} [semiring R] [ M] (N : M) :
theorem submodule.fg_of_linear_equiv {R : Type u_1} {M : Type u_2} [semiring R] [ M] {P : Type u_3} [ P] (e : M ≃ₗ[R] P) (h : .fg) :
theorem submodule.fg.prod {R : Type u_1} {M : Type u_2} [semiring R] [ M] {P : Type u_3} [ P] {sb : M} {sc : P} (hsb : sb.fg) (hsc : sc.fg) :
(sb.prod sc).fg
theorem submodule.fg_pi {R : Type u_1} [semiring R] {ι : Type u_2} {M : ι Type u_3} [finite ι] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] {p : Π (i : ι), (M i)} (hsb : (i : ι), (p i).fg) :
theorem submodule.fg_of_fg_map_of_fg_inf_ker {R : Type u_1} {M : Type u_2} {P : Type u_3} [ring R] [ M] [ P] (f : M →ₗ[R] P) {s : M} (hs1 : s).fg) (hs2 : (s .fg) :
s.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_1) (M : Type u_2) [semiring R] [ M] (P : M Prop) (h₁ : (x : M), P {x})) (h₂ : (M₁ M₂ : M), P M₁ P M₂ P (M₁ M₂)) (N : M) (hN : N.fg) :
P N
theorem submodule.fg_ker_comp {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [ring R] [ M] [ N] [ P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (hf1 : .fg) (hf2 : .fg) (hsur : function.surjective f) :

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_restrict_scalars {R : Type u_1} {S : Type u_2} {M : Type u_3} [semiring S] [ S] [ M] [ M] [ M] (N : M) (hfin : N.fg) (h : function.surjective S)) :
theorem submodule.fg.stablizes_of_supr_eq {R : Type u_1} {M : Type u_2} [semiring R] [ M] {M' : M} (hM' : M'.fg) (N : →o M) (H : = M') :
(n : ), M' = N n
theorem submodule.fg_iff_compact {R : Type u_1} {M : Type u_2} [semiring R] [ M] (s : M) :

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} [ M] [ N] [ P] (f : M →ₗ[R] N →ₗ[R] P) {p : M} {q : N} (hp : p.fg) (hq : q.fg) :
p q).fg
theorem submodule.fg.mul {R : Type u_1} {A : Type u_2} [semiring A] [ A] {M N : A} (hm : M.fg) (hn : N.fg) :
(M * N).fg
theorem submodule.fg.pow {R : Type u_1} {A : Type u_2} [semiring A] [ A] {M : A} (h : M.fg) (n : ) :
(M ^ n).fg
def ideal.fg {R : Type u_1} [semiring R] (I : ideal R) :
Prop

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.

Equations
theorem ideal.fg.map {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] {I : ideal R} (h : I.fg) (f : R →+* S) :
I).fg

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_1} {S : Type u_2} {A : Type u_3} [comm_ring R] [comm_ring S] [comm_ring A] (f : R →+* S) (g : S →+* A) (hf : (ring_hom.ker f).fg) (hg : (ring_hom.ker g).fg) (hsur : function.surjective f) :
theorem ideal.exists_radical_pow_le_of_fg {R : Type u_1} (I : ideal R) (h : I.radical.fg) :
(n : ), I.radical ^ n I
@[class]
structure module.finite (R : Type u_1) (M : Type u_4) [semiring R] [ M] :
Prop

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

Instances of this typeclass
Instances of other typeclasses for module.finite
theorem module.finite_def {R : Type u_1} {M : Type u_2} [semiring R] [ M] :
theorem module.finite.exists_fin {R : Type u_1} {M : Type u_4} [semiring R] [ M] [ M] :
(n : ) (s : fin n M), (set.range s) =
theorem module.finite.of_surjective {R : Type u_1} {M : Type u_4} {N : Type u_5} [semiring R] [ M] [ N] [hM : M] (f : M →ₗ[R] N) (hf : function.surjective f) :
@[protected, instance]
def module.finite.range {R : Type u_1} {M : Type u_4} {N : Type u_5} [semiring R] [ M] [ N] [ M] (f : M →ₗ[R] N) :

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

@[protected, instance]
def module.finite.map {R : Type u_1} {M : Type u_4} {N : Type u_5} [semiring R] [ M] [ N] (p : M) [ p] (f : M →ₗ[R] N) :
p)

Pushforwards of finite submodules are finite.

@[protected, instance]
def module.finite.self (R : Type u_1) [semiring R] :
theorem module.finite.of_restrict_scalars_finite (R : Type u_1) (A : Type u_2) (M : Type u_3) [semiring A] [ M] [ M] [ A] [ M] [hM : M] :
@[protected, instance]
def module.finite.prod {R : Type u_1} {M : Type u_4} {N : Type u_5} [semiring R] [ M] [ N] [hM : M] [hN : N] :
(M × N)
@[protected, instance]
def module.finite.pi {R : Type u_1} [semiring R] {ι : Type u_2} {M : ι Type u_3} [finite ι] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] [h : (i : ι), (M i)] :
(Π (i : ι), M i)
theorem module.finite.equiv {R : Type u_1} {M : Type u_4} {N : Type u_5} [semiring R] [ M] [ N] [hM : M] (e : M ≃ₗ[R] N) :
theorem module.finite.trans {R : Type u_1} (A : Type u_2) (M : Type u_3) [semiring A] [ A] [ M] [ M] [ M] [ A] [ M] :
@[protected, instance]
def module.finite.base_change (R : Type u_1) (A : Type u_2) (M : Type u_4) [semiring A] [ A] [ M] [h : M] :
A M)
@[protected, instance]
def module.finite.tensor_product (R : Type u_1) (M : Type u_4) (N : Type u_5) [ M] [ N] [hM : M] [hN : N] :
M N)
def ring_hom.finite {A : Type u_1} {B : Type u_2} [comm_ring A] [comm_ring B] (f : A →+* B) :
Prop

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

Equations
theorem ring_hom.finite.id (A : Type u_1) [comm_ring A] :
theorem ring_hom.finite.of_surjective {A : Type u_1} {B : Type u_2} [comm_ring A] [comm_ring B] (f : A →+* B) (hf : function.surjective f) :
theorem ring_hom.finite.comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [comm_ring A] [comm_ring B] [comm_ring C] {g : B →+* C} {f : A →+* B} (hg : g.finite) (hf : f.finite) :
(g.comp f).finite
theorem ring_hom.finite.of_comp_finite {A : Type u_1} {B : Type u_2} {C : Type u_3} [comm_ring A] [comm_ring B] [comm_ring C] {f : A →+* B} {g : B →+* C} (h : (g.comp f).finite) :
def alg_hom.finite {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [ A] [ B] (f : A →ₐ[R] B) :
Prop

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.

Equations
theorem alg_hom.finite.id (R : Type u_1) (A : Type u_2) [comm_ring R] [comm_ring A] [ A] :
A).finite
theorem alg_hom.finite.comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_ring R] [comm_ring A] [comm_ring B] [comm_ring C] [ A] [ B] [ C] {g : B →ₐ[R] C} {f : A →ₐ[R] B} (hg : g.finite) (hf : f.finite) :
(g.comp f).finite
theorem alg_hom.finite.of_surjective {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [ A] [ B] (f : A →ₐ[R] B) (hf : function.surjective f) :
theorem alg_hom.finite.of_comp_finite {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_ring R] [comm_ring A] [comm_ring B] [comm_ring C] [ A] [ B] [ C] {f : A →ₐ[R] B} {g : B →ₐ[R] C} (h : (g.comp f).finite) :