mathlib3 documentation

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 #

Main results #

def submodule.fg {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (N : submodule R 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] [add_comm_monoid M] [module R M] {N : submodule R M} :
N.fg (S : set M), S.finite submodule.span R S = N
theorem submodule.fg_iff_exists_fin_generating_family {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {N : submodule R M} :
N.fg (n : ) (s : fin n M), submodule.span R (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} [add_comm_group M] [module R M] (I : ideal R) (N : submodule R 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} [add_comm_group M] [module R M] (I : ideal R) (N : submodule R 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] [add_comm_monoid M] [module R M] :
theorem submodule.fg_unit {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (I : (submodule R A)ˣ) :
theorem submodule.fg_of_is_unit {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] {I : submodule R A} (hI : is_unit I) :
I.fg
theorem submodule.fg_span {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {s : set M} (hs : s.finite) :
theorem submodule.fg_span_singleton {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (x : M) :
theorem submodule.fg.sup {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {N₁ N₂ : submodule R 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] [add_comm_monoid M] [module R M] {ι : Type u_3} (s : finset ι) (N : ι submodule R 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] [add_comm_monoid M] [module R M] {ι : Type u_3} (s : finset ι) (N : ι submodule R 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] [add_comm_monoid M] [module R M] {ι : Type u_3} [finite ι] (N : ι submodule R M) (h : (i : ι), (N i).fg) :
(supr N).fg
theorem submodule.fg.map {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {P : Type u_3} [add_comm_monoid P] [module R P] (f : M →ₗ[R] P) {N : submodule R M} (hs : N.fg) :
theorem submodule.fg_of_fg_map_injective {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {P : Type u_3} [add_comm_monoid P] [module R P] (f : M →ₗ[R] P) (hf : function.injective f) {N : submodule R M} (hfn : (submodule.map f N).fg) :
N.fg
theorem submodule.fg_of_fg_map {R : Type u_1} {M : Type u_2} {P : Type u_3} [ring R] [add_comm_group M] [module R M] [add_comm_group P] [module R P] (f : M →ₗ[R] P) (hf : linear_map.ker f = ) {N : submodule R M} (hfn : (submodule.map f N).fg) :
N.fg
theorem submodule.fg_top {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (N : submodule R M) :
theorem submodule.fg_of_linear_equiv {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {P : Type u_3} [add_comm_monoid P] [module R P] (e : M ≃ₗ[R] P) (h : .fg) :
theorem submodule.fg.prod {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {P : Type u_3} [add_comm_monoid P] [module R P] {sb : submodule R M} {sc : submodule R 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 : ι), module R (M i)] {p : Π (i : ι), submodule R (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] [add_comm_group M] [module R M] [add_comm_group P] [module R P] (f : M →ₗ[R] P) {s : submodule R M} (hs1 : (submodule.map f s).fg) (hs2 : (s linear_map.ker f).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] [add_comm_monoid M] [module R M] (P : submodule R M Prop) (h₁ : (x : M), P (submodule.span R {x})) (h₂ : (M₁ M₂ : submodule R M), P M₁ P M₂ P (M₁ M₂)) (N : submodule R 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] [add_comm_group M] [module R M] [add_comm_group N] [module R N] [add_comm_group P] [module R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (hf1 : (linear_map.ker f).fg) (hf2 : (linear_map.ker g).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} [comm_semiring R] [semiring S] [algebra R S] [add_comm_group M] [module S M] [module R M] [is_scalar_tower R S M] (N : submodule S M) (hfin : N.fg) (h : function.surjective (algebra_map R S)) :
theorem submodule.fg.stablizes_of_supr_eq {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {M' : submodule R M} (hM' : M'.fg) (N : →o submodule R M) (H : supr N = M') :
(n : ), M' = N n

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} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (f : M →ₗ[R] N →ₗ[R] P) {p : submodule R M} {q : submodule R N} (hp : p.fg) (hq : q.fg) :
theorem submodule.fg.mul {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] {M N : submodule R A} (hm : M.fg) (hn : N.fg) :
(M * N).fg
theorem submodule.fg.pow {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] {M : submodule R 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) :

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} [comm_semiring R] (I : ideal R) (h : I.radical.fg) :
(n : ), I.radical ^ n I
theorem module.finite_def {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] :
theorem module.finite.exists_fin {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] [module.finite R M] :
(n : ) (s : fin n M), submodule.span R (set.range s) =
theorem module.finite.of_surjective {R : Type u_1} {M : Type u_4} {N : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] [hM : module.finite R 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] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] [module.finite R 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] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] (p : submodule R M) [module.finite R p] (f : M →ₗ[R] N) :

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) [comm_semiring R] [semiring A] [add_comm_monoid M] [module R M] [module A M] [algebra R A] [is_scalar_tower R A M] [hM : module.finite R M] :
@[protected, instance]
def module.finite.prod {R : Type u_1} {M : Type u_4} {N : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] [hM : module.finite R M] [hN : module.finite R 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 : ι), 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} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] [hM : module.finite R M] (e : M ≃ₗ[R] N) :
theorem module.finite.trans {R : Type u_1} (A : Type u_2) (M : Type u_3) [comm_semiring R] [semiring A] [algebra R A] [add_comm_monoid M] [module R M] [module A M] [is_scalar_tower R A M] [module.finite R A] [module.finite A M] :
@[protected, instance]
def module.finite.base_change (R : Type u_1) (A : Type u_2) (M : Type u_4) [comm_semiring R] [semiring A] [algebra R A] [add_comm_monoid M] [module R M] [h : module.finite R M] :
@[protected, instance]
def module.finite.tensor_product (R : Type u_1) (M : Type u_4) (N : Type u_5) [comm_semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] [hM : module.finite R M] [hN : module.finite R 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] [algebra R A] [algebra R 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] [algebra R A] :
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] [algebra R A] [algebra R B] [algebra R 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] [algebra R A] [algebra R 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] [algebra R A] [algebra R B] [algebra R C] {f : A →ₐ[R] B} {g : B →ₐ[R] C} (h : (g.comp f).finite) :