Finiteness conditions in commutative algebra #
In this file we define several notions of finiteness that are common in commutative algebra.
Main declarations #
module.finite
,algebra.finite
,ring_hom.finite
,alg_hom.finite
all of these express that some object is finitely generated as module over some base ring.algebra.finite_type
,ring_hom.finite_type
,alg_hom.finite_type
all of these express that some object is finitely generated as algebra over some base ring.algebra.finite_presentation
,ring_hom.finite_presentation
,alg_hom.finite_presentation
all of these express that some object is finitely presented as algebra over some base ring.
A module over a commutative ring is finite
if it is finitely generated as a module.
Equations
- module.finite R M = ⊤.fg
An algebra over a commutative ring is of finite_type
if it is finitely generated
over the base ring as algebra.
Equations
- algebra.finite_type R A = ⊤.fg
Instances
An algebra over a commutative ring is finite_presentation
if it is the quotient of a
polynomial ring in n
variables by a finitely generated ideal.
Equations
- algebra.finite_presentation R A = ∃ (n : ℕ) (f : mv_polynomial (fin n) R →ₐ[R] A), function.surjective ⇑f ∧ submodule.fg f.to_ring_hom.ker
An algebra is finitely generated if and only if it is a quotient of a polynomial ring whose variables are indexed by a finset.
An algebra is finitely generated if and only if it is a quotient of a polynomial ring whose variables are indexed by a fintype.
An algebra is finitely generated if and only if it is a quotient of a polynomial ring in n
variables.
A finitely presented algebra is of finite type.
An algebra over a Noetherian ring is finitely generated if and only if it is finitely presented.
If e : A ≃ₐ[R] B
and A
is finitely presented, then so is B
.
The ring of polynomials in finitely many variables is finitely presented.
R
is finitely presented as R
-algebra.
The quotient of a finitely presented algebra by a finitely generated ideal is finitely presented.
If f : A →ₐ[R] B
is surjective with finitely generated kernel and A
is finitely presented,
then so is B
.
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 ring morphism A →+* B
is finite
if B
is finitely generated as A
-module.
Equations
- f.finite = let _inst : algebra A B := f.to_algebra in module.finite A B
A ring morphism A →+* B
is of finite_type
if B
is finitely generated as A
-algebra.
Equations
- f.finite_type = algebra.finite_type A B
A ring morphism A →+* B
is of finite_presentation
if B
is finitely presented as
A
-algebra.
Equations
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
- f.finite = f.to_ring_hom.finite
An algebra morphism A →ₐ[R] B
is of finite_type
if it is of finite type as ring morphism.
In other words, if B
is finitely generated as A
-algebra.
Equations
An algebra morphism A →ₐ[R] B
is of finite_presentation
if it is of finite presentation as
ring morphism. In other words, if B
is finitely presented as A
-algebra.