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.

def Submodule.FG {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid 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.

theorem Submodule.fg_def {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} : N.FG ↔ ∃ (S : Set M), S.Finite ∧ span R S = N

theorem Submodule.fg_iff_addSubmonoid_fg {M : Type u_2} [AddCommMonoid M] (P : Submodule ℕ M) : P.FG ↔ P.FG

theorem Submodule.fg_iff_addSubgroup_fg {G : Type u_3} [AddCommGroup G] (P : Submodule ℤ G) : P.FG ↔ P.toAddSubgroup.FG

@[deprecated Submodule.fg_iff_addSubgroup_fg (since := "2025-08-20")]

theorem Submodule.fg_iff_add_subgroup_fg {G : Type u_3} [AddCommGroup G] (P : Submodule ℤ G) : P.FG ↔ P.toAddSubgroup.FG

Alias of Submodule.fg_iff_addSubgroup_fg.

theorem Submodule.fg_iff_exists_fin_generating_family {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} : N.FG ↔ ∃ (n : ℕ) (s : Fin n → M), span R (Set.range s) = N

theorem Submodule.fg_iff_exists_finite_generating_family {A : Type u} [Semiring A] {M : Type v} [AddCommMonoid M] [Module A M] {N : Submodule A M} : N.FG ↔ ∃ (G : Type w) (_ : Finite G) (g : G → M), span A (Set.range g) = N

theorem Submodule.fg_span_iff_fg_span_finset_subset {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) : (span R s).FG ↔ ∃ (s' : Finset M), ↑s' ⊆ s ∧ span R s = span R ↑s'

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.

class Module.Finite (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : Prop

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

• of_fg_top :: (
• fg_top : ⊤.FG

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

• )

theorem Module.finite_def {R : Type u_6} {M : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] : Module.Finite R M ↔ ⊤.FG

See also Module.Finite.iff_fg for a version when M is itself a submodule.

theorem Module.Finite.iff_addMonoid_fg {M : Type u_6} [AddCommMonoid M] : Module.Finite ℕ M ↔ AddMonoid.FG M

theorem Module.Finite.iff_addGroup_fg {G : Type u_6} [AddCommGroup G] : Module.Finite ℤ G ↔ AddGroup.FG G

theorem Module.Finite.exists_fin {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] : ∃ (n : ℕ) (s : Fin n → M), Submodule.span R (Set.range s) = ⊤

See also Module.Finite.exists_fin'.

instance AddMonoid.FG.to_moduleFinite_nat {M : Type u_6} [AddCommMonoid M] [FG M] : Module.Finite ℕ M

instance AddMonoid.FG.to_moduleFinite_int {G : Type u_6} [AddCommGroup G] [FG G] : Module.Finite ℤ G

def RingHom.Finite {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (f : A →+* B) : Prop

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

@[simp]

theorem RingHom.finite_algebraMap {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] : (algebraMap A B).Finite ↔ Module.Finite A B

def AlgHom.Finite {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing 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.