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.FiniteTypeall of these express that some object is finitely generated as algebra over some base ring.
An algebra over a commutative semiring is of FiniteType if it is finitely generated
over the base ring as algebra.
- out : ⊤.FG
Instances
An algebra is finitely generated if and only if it is a quotient of a free algebra whose variables are indexed by a finset.
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.
An algebra is finitely generated if and only if it is a quotient of a polynomial ring whose variables are indexed by a fintype.
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.
A commutative algebra is finitely generated if and only if it is a quotient of a polynomial ring
in n variables.
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
Alias of RingHom.FiniteType.of_finite.
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
An element of R[M] is in the subalgebra generated by its support.
If a set S generates, as algebra, R[M], then the set of supports of
elements of S generates R[M].
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].
If R[M] is of finite type, then there is a G : Finset M such that its
image generates, as algebra, R[M].
The image of an element m : M in R[M] belongs the submodule generated by
S : Set M if and only if m ∈ 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.
If a set S generates an additive monoid M, then the image of M generates, as algebra,
R[M].
If a set S generates an additive monoid M, then the image of M generates, as algebra,
R[M].
If an additive monoid M is finitely generated then R[M] is of finite
type.
An additive monoid M is finitely generated if and only if R[M] is of
finite type.
If R[M] is of finite type then M is finitely generated.
An additive group G is finitely generated if and only if R[G] is of
finite type.
An element of MonoidAlgebra R M is in the subalgebra generated by its support.
If a set S generates, as algebra, MonoidAlgebra R M, then the set of supports of elements
of S generates MonoidAlgebra R M.
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.
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.
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.
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.
If a set S generates a monoid M, then the image of M generates, as algebra,
MonoidAlgebra R M.
If a set S generates an additive monoid M, then the image of M generates, as algebra,
R[M].
If a monoid M is finitely generated then MonoidAlgebra R M is of finite type.
A monoid M is finitely generated if and only if MonoidAlgebra R M is of finite type.
If MonoidAlgebra R M is of finite type then M is finitely generated.
A group G is finitely generated if and only if R[G] is of finite type.
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 [Orz71].
A theorem by Vasconcelos, given a finite module M over a commutative ring, any
surjective endomorphism of M is also injective.
It is a consequence of the fact CommRing.orzechProperty
that any commutative ring R satisfies the OrzechProperty;
please use OrzechProperty.injective_of_surjective_endomorphism instead.
This is similar to IsNoetherian.injective_of_surjective_endomorphism but only applies in the
commutative case, but does not use a Noetherian hypothesis.