Finiteness conditions in commutative algebra #
In this file we define several notions of finiteness that are common in commutative algebra.
Main declarations #
AlgHom.Finiteall of these express that some object is finitely generated as module over some base ring.
AlgHom.FiniteTypeall of these express that some object is finitely generated as algebra over some base ring.
AlgHom.FinitePresentationall of these express that some object is finitely presented as algebra over some base ring.
The quotient of a finitely presented algebra by a finitely generated ideal is finitely presented.
f : A →ₐ[R] B is surjective with finitely generated kernel and
A is finitely presented,
then so is
An algebra is finitely presented if and only if it is a quotient of a polynomial ring whose variables are indexed by a fintype by a finitely generated ideal.
A is a finitely presented
MvPolynomial (Fin n) A is finitely presented
A is an
S is an
A-algebra, both finitely presented, then
finitely presented as
This is used to prove the strictly stronger
ker_fg_of_surjective. Use it instead.
f : A →ₐ[R] B is a surjection between finitely-presented
R-algebras, then the kernel of
f is finitely generated.
An algebra morphism
A →ₐ[R] B is of
AlgHom.FinitePresentation if it is of finite
presentation as ring morphism. In other words, if
B is finitely presented as