# Finiteness conditions in commutative algebra #

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

## Main declarations #

- `Algebra.FiniteType`, `RingHom.FiniteType`, `AlgHom.FiniteType` all of these express that some object is finitely generated as algebra over some base ring.

source
class Algebra.FiniteType (R : Type uR) (A : Type uA) [CommSemiring R] [Semiring A] [Algebra R A] :
Prop

An algebra over a commutative semiring is of `FiniteType` if it is finitely generated over the base ring as algebra.

- out : ⊤.FG

Instances

source
@[instance 100]
instance Module.Finite.finiteType {R : Type u_1} (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [hRA : Module.Finite R A] :
Algebra.FiniteType R A
source
@[deprecated inferInstance (since := "2025-07-12")]
theorem Algebra.FiniteType.self (R : Type uR) [CommSemiring R] :
FiniteType R R
source
theorem Algebra.FiniteType.of_restrictScalars_finiteType (R : Type uR) (S : Type uS) (A : Type uA) [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [hA : FiniteType R A] :
FiniteType S A
source
theorem Algebra.FiniteType.of_surjective {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [FiniteType R A] (f : A →ₐ[R] B) (hf : Function.Surjective ⇑f) :
FiniteType R B
source
theorem Algebra.FiniteType.equiv {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (hRA : FiniteType R A) (e : A ≃ₐ[R] B) :
FiniteType R B
source
theorem Algebra.FiniteType.trans {R : Type uR} {S : Type uS} {A : Type uA} [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] (hRS : FiniteType R S) (hSA : FiniteType S A) :
FiniteType R A
source
instance Algebra.FiniteType.quotient (R : Type u_1) {S : Type u_2} [CommSemiring R] [CommRing S] [Algebra R S] (I : Ideal S) [h : FiniteType R S] :
FiniteType R (S ⧸ I)
source
instance Algebra.FiniteType.instPolynomial {R : Type uR} {S : Type uS} [CommSemiring R] [CommSemiring S] [Algebra R S] [FiniteType R S] :
FiniteType R (Polynomial S)
source
@[deprecated inferInstance (since := "2025-07-12")]
theorem Algebra.FiniteType.polynomial {R : Type uR} [CommSemiring R] :
FiniteType R (Polynomial R)
source
instance Algebra.FiniteType.instMvPolynomialOfFinite {R : Type uR} {S : Type uS} [CommSemiring R] [CommSemiring S] [Algebra R S] {ι : Type u_1} [Finite ι] [FiniteType R S] :
FiniteType R (MvPolynomial ι S)
source
@[deprecated inferInstance (since := "2025-07-12")]
theorem Algebra.FiniteType.mvPolynomial {R : Type uR} [CommSemiring R] (ι : Type u_1) [Finite ι] :
FiniteType R (MvPolynomial ι R)
source
instance Algebra.FiniteType.instFreeAlgebraOfFinite {R : Type uR} {S : Type uS} [CommSemiring R] [CommSemiring S] [Algebra R S] {ι : Type u_1} [Finite ι] [FiniteType R S] :
FiniteType R (FreeAlgebra S ι)
source
@[deprecated inferInstance (since := "2025-07-12")]
theorem Algebra.FiniteType.freeAlgebra {R : Type uR} [CommSemiring R] (ι : Type u_1) [Finite ι] :
FiniteType R (FreeAlgebra R ι)
source
theorem Algebra.FiniteType.iff_quotient_freeAlgebra {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] :
FiniteType R A ↔ ∃ (s : Finset A) (f : FreeAlgebra R ↥s →ₐ[R] A), Function.Surjective ⇑f

An algebra is finitely generated if and only if it is a quotient of a free algebra whose variables are indexed by a finset.

source
theorem Algebra.FiniteType.iff_quotient_mvPolynomial {R : Type uR} {S : Type uS} [CommSemiring R] [CommSemiring S] [Algebra R S] :
FiniteType R S ↔ ∃ (s : Finset S) (f : MvPolynomial { x : S // x ∈ s } R →ₐ[R] S), Function.Surjective ⇑f

A commutative algebra is finitely generated if and only if it is a quotient of a polynomial ring whose variables are indexed by a finset.

source
theorem Algebra.FiniteType.iff_quotient_freeAlgebra' {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] :
FiniteType R A ↔ ∃ (ι : Type uA) (x : Fintype ι) (f : FreeAlgebra R ι →ₐ[R] A), Function.Surjective ⇑f

An algebra is finitely generated if and only if it is a quotient of a polynomial ring whose variables are indexed by a fintype.

source
theorem Algebra.FiniteType.iff_quotient_mvPolynomial' {R : Type uR} {S : Type uS} [CommSemiring R] [CommSemiring S] [Algebra R S] :
FiniteType R S ↔ ∃ (ι : Type uS) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] S), Function.Surjective ⇑f

A commutative algebra is finitely generated if and only if it is a quotient of a polynomial ring whose variables are indexed by a fintype.

source
theorem Algebra.FiniteType.iff_quotient_mvPolynomial'' {R : Type uR} {S : Type uS} [CommSemiring R] [CommSemiring S] [Algebra R S] :
FiniteType R S ↔ ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S), Function.Surjective ⇑f

A commutative algebra is finitely generated if and only if it is a quotient of a polynomial ring in `n` variables.

source
instance Algebra.FiniteType.prod {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [hA : FiniteType R A] [hB : FiniteType R B] :
FiniteType R (A × B)
source
theorem Algebra.FiniteType.isNoetherianRing (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [h : FiniteType R S] [IsNoetherianRing R] :
IsNoetherianRing S
source
theorem Subalgebra.fg_iff_finiteType {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
S.FG ↔ Algebra.FiniteType R ↥S
source
theorem Algebra.FiniteType.adjoin_of_finite {R : Type uR} [CommSemiring R] {A : Type u_1} [CommSemiring A] [Algebra R A] {t : Set A} (h : t.Finite) :
FiniteType R ↥(adjoin R t)
source
def RingHom.FiniteType {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (f : A →+* B) :
Prop

A ring morphism `A →+* B` is of `FiniteType` if `B` is finitely generated as `A`-algebra.

Equations

- f.FiniteType = Algebra.FiniteType A B

Instances For

source
theorem RingHom.finiteType_algebraMap {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] :
(algebraMap A B).FiniteType ↔ Algebra.FiniteType A B
source
theorem RingHom.Finite.finiteType {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] {f : A →+* B} (hf : f.Finite) :
f.FiniteType
source
theorem RingHom.FiniteType.id (A : Type u_1) [CommRing A] :
(RingHom.id A).FiniteType
source
theorem RingHom.FiniteType.comp_surjective {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommRing A] [CommRing B] [CommRing C] {f : A →+* B} {g : B →+* C} (hf : f.FiniteType) (hg : Function.Surjective ⇑g) :
(g.comp f).FiniteType
source
theorem RingHom.FiniteType.of_surjective {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (f : A →+* B) (hf : Function.Surjective ⇑f) :
f.FiniteType
source
theorem RingHom.FiniteType.comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommRing A] [CommRing B] [CommRing C] {g : B →+* C} {f : A →+* B} (hg : g.FiniteType) (hf : f.FiniteType) :
(g.comp f).FiniteType
source
theorem RingHom.FiniteType.of_finite {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] {f : A →+* B} (hf : f.Finite) :
f.FiniteType
source
theorem RingHom.Finite.to_finiteType {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] {f : A →+* B} (hf : f.Finite) :
f.FiniteType

Alias of `RingHom.FiniteType.of_finite`.

source
theorem RingHom.FiniteType.of_comp_finiteType {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommRing A] [CommRing B] [CommRing C] {f : A →+* B} {g : B →+* C} (h : (g.comp f).FiniteType) :
g.FiniteType
source
def AlgHom.FiniteType {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 of `FiniteType` if it is of finite type as ring morphism. In other words, if `B` is finitely generated as `A`-algebra.

Equations

- f.FiniteType = f.FiniteType

Instances For

source
theorem AlgHom.Finite.finiteType {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} (hf : f.Finite) :
f.FiniteType
source
theorem AlgHom.FiniteType.id (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Algebra R A] :
(AlgHom.id R A).FiniteType
source
theorem AlgHom.FiniteType.comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [CommRing A] [CommRing B] [CommRing C] [Algebra R A] [Algebra R B] [Algebra R C] {g : B →ₐ[R] C} {f : A →ₐ[R] B} (hg : g.FiniteType) (hf : f.FiniteType) :
(g.comp f).FiniteType
source
theorem AlgHom.FiniteType.comp_surjective {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [CommRing A] [CommRing B] [CommRing C] [Algebra R A] [Algebra R B] [Algebra R C] {f : A →ₐ[R] B} {g : B →ₐ[R] C} (hf : f.FiniteType) (hg : Function.Surjective ⇑g) :
(g.comp f).FiniteType
source
theorem AlgHom.FiniteType.of_surjective {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) (hf : Function.Surjective ⇑f) :
f.FiniteType
source
theorem AlgHom.FiniteType.of_comp_finiteType {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [CommRing A] [CommRing B] [CommRing C] [Algebra R A] [Algebra R B] [Algebra R C] {f : A →ₐ[R] B} {g : B →ₐ[R] C} (h : (g.comp f).FiniteType) :
g.FiniteType
source
@[deprecated RingHom.finiteType_algebraMap (since := "2025-08-12")]
theorem algebraMap_finiteType_iff_algebra_finiteType {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] :
(algebraMap A B).FiniteType ↔ Algebra.FiniteType A B

Alias of `RingHom.finiteType_algebraMap`.

source
theorem AddMonoidAlgebra.mem_adjoin_support {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddMonoid M] (f : AddMonoidAlgebra R M) :
f ∈ Algebra.adjoin R (of' R M '' ↑f.support)

An element of `R[M]` is in the subalgebra generated by its support.

source
theorem AddMonoidAlgebra.support_gen_of_gen {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddMonoid M] {S : Set (AddMonoidAlgebra R M)} (hS : Algebra.adjoin R S = ⊤) :
Algebra.adjoin R (⋃ f ∈ S, of' R M '' ↑f.support) = ⊤

If a set `S` generates, as algebra, `R[M]`, then the set of supports of elements of `S` generates `R[M]`.

source
theorem AddMonoidAlgebra.support_gen_of_gen' {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddMonoid M] {S : Set (AddMonoidAlgebra R M)} (hS : Algebra.adjoin R S = ⊤) :
Algebra.adjoin R (of' R M '' ⋃ f ∈ S, ↑f.support) = ⊤

If a set `S` generates, as algebra, `R[M]`, then the image of the union of the supports of elements of `S` generates `R[M]`.

source
theorem AddMonoidAlgebra.exists_finset_adjoin_eq_top {R : Type u_1} {M : Type u_2} [CommRing R] [AddMonoid M] [h : Algebra.FiniteType R (AddMonoidAlgebra R M)] :
∃ (G : Finset M), Algebra.adjoin R (of' R M '' ↑G) = ⊤

If `R[M]` is of finite type, then there is a `G : Finset M` such that its image generates, as algebra, `R[M]`.

source
theorem AddMonoidAlgebra.of'_mem_span {R : Type u_1} {M : Type u_2} [CommRing R] [AddMonoid M] [Nontrivial R] {m : M} {S : Set M} :
of' R M m ∈ Submodule.span R (of' R M '' S) ↔ m ∈ S

The image of an element `m : M` in `R[M]` belongs the submodule generated by `S : Set M` if and only if `m ∈ S`.

source
theorem AddMonoidAlgebra.mem_closure_of_mem_span_closure {R : Type u_1} {M : Type u_2} [CommRing R] [AddMonoid M] [Nontrivial R] {m : M} {S : Set M} (h : of' R M m ∈ Submodule.span R ↑(Submonoid.closure (of' R M '' S))) :
m ∈ AddSubmonoid.closure S

If the image of an element `m : M` in `R[M]` belongs the submodule generated by the closure of some `S : Set M` then `m ∈ closure S`.

source
theorem AddMonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure {R : Type u_1} {M : Type u_2} [AddCommMonoid M] [CommSemiring R] {S : Set M} (hS : AddSubmonoid.closure S = ⊤) :
Function.Surjective ⇑(MvPolynomial.aeval fun (s : ↑S) => of' R M ↑s)

If a set `S` generates an additive monoid `M`, then the image of `M` generates, as algebra, `R[M]`.

source
theorem AddMonoidAlgebra.freeAlgebra_lift_of_surjective_of_closure {R : Type u_1} {M : Type u_2} [AddMonoid M] [CommSemiring R] {S : Set M} (hS : AddSubmonoid.closure S = ⊤) :
Function.Surjective ⇑((FreeAlgebra.lift R) fun (s : ↑S) => of' R M ↑s)

If a set `S` generates an additive monoid `M`, then the image of `M` generates, as algebra, `R[M]`.

source
instance AddMonoidAlgebra.finiteType_of_fg (R : Type u_1) (M : Type u_2) [AddMonoid M] [CommRing R] [h : AddMonoid.FG M] :
Algebra.FiniteType R (AddMonoidAlgebra R M)

If an additive monoid `M` is finitely generated then `R[M]` is of finite type.

source
theorem AddMonoidAlgebra.finiteType_iff_fg {R : Type u_1} {M : Type u_2} [AddMonoid M] [CommRing R] [Nontrivial R] :
Algebra.FiniteType R (AddMonoidAlgebra R M) ↔ AddMonoid.FG M

An additive monoid `M` is finitely generated if and only if `R[M]` is of finite type.

source
theorem AddMonoidAlgebra.fg_of_finiteType {R : Type u_1} {M : Type u_2} [AddMonoid M] [CommRing R] [Nontrivial R] [h : Algebra.FiniteType R (AddMonoidAlgebra R M)] :
AddMonoid.FG M

If `R[M]` is of finite type then `M` is finitely generated.

source
theorem AddMonoidAlgebra.finiteType_iff_group_fg {R : Type u_1} {G : Type u_3} [AddGroup G] [CommRing R] [Nontrivial R] :
Algebra.FiniteType R (AddMonoidAlgebra R G) ↔ AddGroup.FG G

An additive group `G` is finitely generated if and only if `R[G]` is of finite type.

source
theorem MonoidAlgebra.mem_adjoin_support {R : Type u_1} {M : Type u_2} [CommSemiring R] [Monoid M] (f : MonoidAlgebra R M) :
f ∈ Algebra.adjoin R (⇑(of R M) '' ↑f.support)

An element of `MonoidAlgebra R M` is in the subalgebra generated by its support.

source
theorem MonoidAlgebra.support_gen_of_gen {R : Type u_1} {M : Type u_2} [CommSemiring R] [Monoid M] {S : Set (MonoidAlgebra R M)} (hS : Algebra.adjoin R S = ⊤) :
Algebra.adjoin R (⋃ f ∈ S, ⇑(of R M) '' ↑f.support) = ⊤

If a set `S` generates, as algebra, `MonoidAlgebra R M`, then the set of supports of elements of `S` generates `MonoidAlgebra R M`.

source
theorem MonoidAlgebra.support_gen_of_gen' {R : Type u_1} {M : Type u_2} [CommSemiring R] [Monoid M] {S : Set (MonoidAlgebra R M)} (hS : Algebra.adjoin R S = ⊤) :
Algebra.adjoin R (⇑(of R M) '' ⋃ f ∈ S, ↑f.support) = ⊤

If a set `S` generates, as algebra, `MonoidAlgebra R M`, then the image of the union of the supports of elements of `S` generates `MonoidAlgebra R M`.

source
theorem MonoidAlgebra.exists_finset_adjoin_eq_top {R : Type u_1} {M : Type u_2} [CommRing R] [Monoid M] [h : Algebra.FiniteType R (MonoidAlgebra R M)] :
∃ (G : Finset M), Algebra.adjoin R (⇑(of R M) '' ↑G) = ⊤

If `MonoidAlgebra R M` is of finite type, then there is a `G : Finset M` such that its image generates, as algebra, `MonoidAlgebra R M`.

source
theorem MonoidAlgebra.of_mem_span_of_iff {R : Type u_1} {M : Type u_2} [CommRing R] [Monoid M] [Nontrivial R] {m : M} {S : Set M} :
(of R M) m ∈ Submodule.span R (⇑(of R M) '' S) ↔ m ∈ S

The image of an element `m : M` in `MonoidAlgebra R M` belongs the submodule generated by `S : Set M` if and only if `m ∈ S`.

source
theorem MonoidAlgebra.mem_closure_of_mem_span_closure {R : Type u_1} {M : Type u_2} [CommRing R] [Monoid M] [Nontrivial R] {m : M} {S : Set M} (h : (of R M) m ∈ Submodule.span R ↑(Submonoid.closure (⇑(of R M) '' S))) :
m ∈ Submonoid.closure S

If the image of an element `m : M` in `MonoidAlgebra R M` belongs the submodule generated by the closure of some `S : Set M` then `m ∈ closure S`.

source
theorem MonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure {R : Type u_1} {M : Type u_2} [CommMonoid M] [CommSemiring R] {S : Set M} (hS : Submonoid.closure S = ⊤) :
Function.Surjective ⇑(MvPolynomial.aeval fun (s : ↑S) => (of R M) ↑s)

If a set `S` generates a monoid `M`, then the image of `M` generates, as algebra, `MonoidAlgebra R M`.

source
theorem MonoidAlgebra.freeAlgebra_lift_of_surjective_of_closure {R : Type u_1} {M : Type u_2} [Monoid M] [CommSemiring R] {S : Set M} (hS : Submonoid.closure S = ⊤) :
Function.Surjective ⇑((FreeAlgebra.lift R) fun (s : ↑S) => (of R M) ↑s)

If a set `S` generates an additive monoid `M`, then the image of `M` generates, as algebra, `R[M]`.

source
instance MonoidAlgebra.finiteType_of_fg {R : Type u_1} {M : Type u_2} [Monoid M] [CommRing R] [Monoid.FG M] :
Algebra.FiniteType R (MonoidAlgebra R M)

If a monoid `M` is finitely generated then `MonoidAlgebra R M` is of finite type.

source
theorem MonoidAlgebra.finiteType_iff_fg {R : Type u_1} {M : Type u_2} [Monoid M] [CommRing R] [Nontrivial R] :
Algebra.FiniteType R (MonoidAlgebra R M) ↔ Monoid.FG M

A monoid `M` is finitely generated if and only if `MonoidAlgebra R M` is of finite type.

source
theorem MonoidAlgebra.fg_of_finiteType {R : Type u_1} {M : Type u_2} [Monoid M] [CommRing R] [Nontrivial R] [h : Algebra.FiniteType R (MonoidAlgebra R M)] :
Monoid.FG M

If `MonoidAlgebra R M` is of finite type then `M` is finitely generated.

source
theorem MonoidAlgebra.finiteType_iff_group_fg {R : Type u_1} {G : Type u_3} [Group G] [CommRing R] [Nontrivial R] :
Algebra.FiniteType R (MonoidAlgebra R G) ↔ Group.FG G

A group `G` is finitely generated if and only if `R[G]` is of finite type.

source
@[instance 100]
instance CommRing.orzechProperty (R : Type u_1) [CommRing R] :
OrzechProperty R

Any commutative ring `R` satisfies the `OrzechProperty`, that is, for any finitely generated `R`-module `M`, any surjective homomorphism `f : N →ₗ[R] M` from a submodule `N` of `M` to `M` is injective.

This is a consequence of Noetherian case (`IsNoetherian.injective_of_surjective_of_injective`), which requires that `M` is a Noetherian module, but allows `R` to be non-commutative. The reduction of this result to Noetherian case is adapted from https://math.stackexchange.com/a/1066110: suppose `{ m_j }` is a finite set of generator of `M`, for any `n : N` one can write `i n = ∑ j, b_j * m_j` for `{ b_j }` in `R`, here `i : N →ₗ[R] M` is the standard inclusion. We can choose `{ n_j }` which are preimages of `{ m_j }` under `f`, and can choose `{ c_jl }` in `R` such that `i n_j = ∑ l, c_jl * m_l` for each `j`. Now let `A` be the subring of `R` generated by `{ b_j }` and `{ c_jl }`, then it is Noetherian. Let `N'` be the `A`-submodule of `N` generated by `n` and `{ n_j }`, `M'` be the `A`-submodule of `M` generated by `{ m_j }`, then it's easy to see that `i` and `f` restrict to `N' →ₗ[A] M'`, and the restricted version of `f` is surjective, hence by Noetherian case, it is also injective, in particular, if `f n = 0`, then `n = 0`.

See also Orzech's original paper: Onto endomorphisms are isomorphisms [orzech1971].