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.
A submodule of M
is finitely generated if it is the span of a finite subset of M
.
Instances For
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.
Equations
Instances For
A module over a semiring is Module.Finite
if it is finitely generated as a module.
A module over a semiring is
Module.Finite
if it is finitely generated as a module.
Instances
See also Module.Finite.exists_fin'
.
A ring morphism A →+* B
is RingHom.Finite
if B
is finitely generated as A
-module.