# mathlibdocumentation

ring_theory.finiteness

# 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.
@[class]
structure module.finite (R : Type u_1) (M : Type u_4) [semiring R] [ M] :
Prop

A module over a semiring is finite if it is finitely generated as a module.

Instances of this typeclass
Instances of other typeclasses for module.finite
@[class]
structure algebra.finite_type (R : Type u_1) (A : Type u_2) [semiring A] [ A] :
Prop

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

Instances of this typeclass
def algebra.finite_presentation (R : Type u_1) (A : Type u_2) [semiring A] [ A] :
Prop

An algebra over a commutative semiring is finite_presentation if it is the quotient of a polynomial ring in n variables by a finitely generated ideal.

Equations
theorem module.finite_def {R : Type u_1} {M : Type u_2} [semiring R] [ M] :
@[protected, instance]
def module.is_noetherian.finite (R : Type u_1) (M : Type u_4) [semiring R] [ M] [ M] :
theorem module.finite.iff_add_monoid_fg {M : Type u_1}  :
theorem module.finite.iff_add_group_fg {G : Type u_1}  :
theorem module.finite.exists_fin {R : Type u_1} {M : Type u_4} [semiring R] [ M] [ M] :
∃ (n : ) (s : fin n → M), (set.range s) =
theorem module.finite.of_surjective {R : Type u_1} {M : Type u_4} {N : Type u_5} [semiring R] [ M] [ N] [hM : M] (f : M →ₗ[R] N) (hf : function.surjective f) :
theorem module.finite.of_injective {R : Type u_1} {M : Type u_4} {N : Type u_5} [semiring R] [ M] [ N] [ N] (f : M →ₗ[R] N) (hf : function.injective f) :
@[protected, instance]
def module.finite.self (R : Type u_1) [semiring R] :
theorem module.finite.of_restrict_scalars_finite (R : Type u_1) (A : Type u_2) (M : Type u_3) [semiring A] [ M] [ M] [ A] [ M] [hM : M] :
@[protected, instance]
def module.finite.prod {R : Type u_1} {M : Type u_4} {N : Type u_5} [semiring R] [ M] [ N] [hM : M] [hN : N] :
(M × N)
@[protected, instance]
def module.finite.pi {R : Type u_1} [semiring R] {ι : Type u_2} {M : ι → Type u_3} [fintype ι] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] [h : ∀ (i : ι), (M i)] :
(Π (i : ι), M i)
theorem module.finite.equiv {R : Type u_1} {M : Type u_4} {N : Type u_5} [semiring R] [ M] [ N] [hM : M] (e : M ≃ₗ[R] N) :
theorem module.finite.trans {R : Type u_1} (A : Type u_2) (B : Type u_3) [ A] [semiring B] [ B] [ B] [ B] [ A] [ B] :
@[protected, instance]
def module.finite.finite_type {R : Type u_1} (A : Type u_2) [semiring A] [ A] [hRA : A] :
@[protected, instance]
def module.finite.base_change (R : Type u_1) (A : Type u_2) (M : Type u_4) [semiring A] [ A] [ M] [h : M] :
A M)
@[protected, instance]
def module.finite.tensor_product (R : Type u_1) (M : Type u_4) (N : Type u_5) [ M] [ N] [hM : M] [hN : N] :
M N)
theorem algebra.finite_type.self (R : Type u_1) [comm_ring R] :
@[protected]
theorem algebra.finite_type.polynomial (R : Type u_1) [comm_ring R] :
@[protected]
theorem algebra.finite_type.mv_polynomial (R : Type u_1) [comm_ring R] (ι : Type u_2) [fintype ι] :
R)
theorem algebra.finite_type.of_restrict_scalars_finite_type (R : Type u_1) (A : Type u_2) (B : Type u_3) [comm_ring R] [comm_ring A] [ A] [comm_ring B] [ B] [ B] [ B] [hB : B] :
theorem algebra.finite_type.of_surjective {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [ A] [comm_ring B] [ B] (hRA : A) (f : A →ₐ[R] B) (hf : function.surjective f) :
theorem algebra.finite_type.equiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [ A] [comm_ring B] [ B] (hRA : A) (e : A ≃ₐ[R] B) :
theorem algebra.finite_type.trans {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [ A] [comm_ring B] [ B] [ B] [ B] (hRA : A) (hAB : B) :
theorem algebra.finite_type.iff_quotient_mv_polynomial {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] :
∃ (s : finset A) (f : mv_polynomial {x // x s} R →ₐ[R] A),

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

theorem algebra.finite_type.iff_quotient_mv_polynomial' {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] :
∃ (ι : Type u_2) (_x : fintype ι) (f : →ₐ[R] A),

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

theorem algebra.finite_type.iff_quotient_mv_polynomial'' {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] :
∃ (n : ) (f : mv_polynomial (fin n) R →ₐ[R] A),

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

theorem algebra.finite_type.of_finite_presentation {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] :

A finitely presented algebra is of finite type.

@[protected, instance]
def algebra.finite_type.prod {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [ A] [comm_ring B] [ B] [hA : A] [hB : B] :
(A × B)
theorem algebra.finite_type.is_noetherian_ring (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] [h : S]  :
theorem subalgebra.fg_iff_finite_type {R : Type u_1} {A : Type u_2} [semiring A] [ A] (S : A) :
S.fg
theorem algebra.finite_presentation.of_finite_type {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A]  :

An algebra over a Noetherian ring is finitely generated if and only if it is finitely presented.

theorem algebra.finite_presentation.equiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [ A] [comm_ring B] [ B] (hfp : A) (e : A ≃ₐ[R] B) :

If e : A ≃ₐ[R] B and A is finitely presented, then so is B.

@[protected]
theorem algebra.finite_presentation.mv_polynomial (R : Type u_1) [comm_ring R] (ι : Type u_2) [fintype ι] :

The ring of polynomials in finitely many variables is finitely presented.

theorem algebra.finite_presentation.self (R : Type u_1) [comm_ring R] :

R is finitely presented as R-algebra.

theorem algebra.finite_presentation.polynomial (R : Type u_1) [comm_ring R] :

R[X] is finitely presented as R-algebra.

@[protected]
theorem algebra.finite_presentation.quotient {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {I : ideal A} (h : I.fg) (hfp : A) :
(A I)

The quotient of a finitely presented algebra by a finitely generated ideal is finitely presented.

theorem algebra.finite_presentation.of_surjective {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [ A] [comm_ring B] [ B] {f : A →ₐ[R] B} (hf : function.surjective f) (hker : .fg) (hfp : A) :

If f : A →ₐ[R] B is surjective with finitely generated kernel and A is finitely presented, then so is B.

theorem algebra.finite_presentation.iff {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] :
∃ (n : ) (I : ideal (mv_polynomial (fin n) R)) (e : (mv_polynomial (fin n) R I) ≃ₐ[R] A), I.fg
theorem algebra.finite_presentation.iff_quotient_mv_polynomial' {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] :
∃ (ι : Type u_2) (_x : fintype ι) (f : →ₐ[R] A),

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.

theorem algebra.finite_presentation.mv_polynomial_of_finite_presentation {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] (hfp : A) (ι : Type u_3) [fintype ι] :

If A is a finitely presented R-algebra, then mv_polynomial (fin n) A is finitely presented as R-algebra.

theorem algebra.finite_presentation.trans {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [ A] [comm_ring B] [ B] [ B] [ B] (hfpA : A) (hfpB : B) :

If A is an R-algebra and S is an A-algebra, both finitely presented, then S is finitely presented as R-algebra.

def ring_hom.finite {A : Type u_1} {B : Type u_2} [comm_ring A] [comm_ring B] (f : A →+* B) :
Prop

A ring morphism A →+* B is finite if B is finitely generated as A-module.

Equations
def ring_hom.finite_type {A : Type u_1} {B : Type u_2} [comm_ring A] [comm_ring B] (f : A →+* B) :
Prop

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

Equations
def ring_hom.finite_presentation {A : Type u_1} {B : Type u_2} [comm_ring A] [comm_ring B] (f : A →+* B) :
Prop

A ring morphism A →+* B is of finite_presentation if B is finitely presented as A-algebra.

Equations
theorem ring_hom.finite.id (A : Type u_1) [comm_ring A] :
theorem ring_hom.finite.of_surjective {A : Type u_1} {B : Type u_2} [comm_ring A] [comm_ring B] (f : A →+* B) (hf : function.surjective f) :
theorem ring_hom.finite.comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [comm_ring A] [comm_ring B] [comm_ring C] {g : B →+* C} {f : A →+* B} (hg : g.finite) (hf : f.finite) :
(g.comp f).finite
theorem ring_hom.finite.finite_type {A : Type u_1} {B : Type u_2} [comm_ring A] [comm_ring B] {f : A →+* B} (hf : f.finite) :
theorem ring_hom.finite.of_comp_finite {A : Type u_1} {B : Type u_2} {C : Type u_3} [comm_ring A] [comm_ring B] [comm_ring C] {f : A →+* B} {g : B →+* C} (h : (g.comp f).finite) :
theorem ring_hom.finite_type.id (A : Type u_1) [comm_ring A] :
theorem ring_hom.finite_type.comp_surjective {A : Type u_1} {B : Type u_2} {C : Type u_3} [comm_ring A] [comm_ring B] [comm_ring C] {f : A →+* B} {g : B →+* C} (hf : f.finite_type) (hg : function.surjective g) :
theorem ring_hom.finite_type.of_surjective {A : Type u_1} {B : Type u_2} [comm_ring A] [comm_ring B] (f : A →+* B) (hf : function.surjective f) :
theorem ring_hom.finite_type.comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [comm_ring A] [comm_ring B] [comm_ring C] {g : B →+* C} {f : A →+* B} (hg : g.finite_type) (hf : f.finite_type) :
theorem ring_hom.finite_type.of_finite {A : Type u_1} {B : Type u_2} [comm_ring A] [comm_ring B] {f : A →+* B} (hf : f.finite) :
theorem ring_hom.finite.to_finite_type {A : Type u_1} {B : Type u_2} [comm_ring A] [comm_ring B] {f : A →+* B} (hf : f.finite) :

Alias of ring_hom.finite_type.of_finite.

theorem ring_hom.finite_type.of_finite_presentation {A : Type u_1} {B : Type u_2} [comm_ring A] [comm_ring B] {f : A →+* B} (hf : f.finite_presentation) :
theorem ring_hom.finite_type.of_comp_finite_type {A : Type u_1} {B : Type u_2} {C : Type u_3} [comm_ring A] [comm_ring B] [comm_ring C] {f : A →+* B} {g : B →+* C} (h : (g.comp f).finite_type) :
theorem ring_hom.finite_presentation.id (A : Type u_1) [comm_ring A] :
theorem ring_hom.finite_presentation.comp_surjective {A : Type u_1} {B : Type u_2} {C : Type u_3} [comm_ring A] [comm_ring B] [comm_ring C] {f : A →+* B} {g : B →+* C} (hf : f.finite_presentation) (hg : function.surjective g) (hker : (ring_hom.ker g).fg) :
theorem ring_hom.finite_presentation.of_surjective {A : Type u_1} {B : Type u_2} [comm_ring A] [comm_ring B] (f : A →+* B) (hf : function.surjective f) (hker : (ring_hom.ker f).fg) :
theorem ring_hom.finite_presentation.of_finite_type {A : Type u_1} {B : Type u_2} [comm_ring A] [comm_ring B] {f : A →+* B} :
theorem ring_hom.finite_presentation.comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [comm_ring A] [comm_ring B] [comm_ring C] {g : B →+* C} {f : A →+* B} (hg : g.finite_presentation) (hf : f.finite_presentation) :
def alg_hom.finite {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [ A] [ B] (f : A →ₐ[R] B) :
Prop

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
def alg_hom.finite_type {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [ A] [ B] (f : A →ₐ[R] B) :
Prop

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
def alg_hom.finite_presentation {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [ A] [ B] (f : A →ₐ[R] B) :
Prop

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.

Equations
theorem alg_hom.finite.id (R : Type u_1) (A : Type u_2) [comm_ring R] [comm_ring A] [ A] :
A).finite
theorem alg_hom.finite.comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_ring R] [comm_ring A] [comm_ring B] [comm_ring C] [ A] [ B] [ C] {g : B →ₐ[R] C} {f : A →ₐ[R] B} (hg : g.finite) (hf : f.finite) :
(g.comp f).finite
theorem alg_hom.finite.of_surjective {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [ A] [ B] (f : A →ₐ[R] B) (hf : function.surjective f) :
theorem alg_hom.finite.finite_type {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [ A] [ B] {f : A →ₐ[R] B} (hf : f.finite) :
theorem alg_hom.finite.of_comp_finite {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_ring R] [comm_ring A] [comm_ring B] [comm_ring C] [ A] [ B] [ C] {f : A →ₐ[R] B} {g : B →ₐ[R] C} (h : (g.comp f).finite) :
theorem alg_hom.finite_type.id (R : Type u_1) (A : Type u_2) [comm_ring R] [comm_ring A] [ A] :
theorem alg_hom.finite_type.comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_ring R] [comm_ring A] [comm_ring B] [comm_ring C] [ A] [ B] [ C] {g : B →ₐ[R] C} {f : A →ₐ[R] B} (hg : g.finite_type) (hf : f.finite_type) :
theorem alg_hom.finite_type.comp_surjective {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_ring R] [comm_ring A] [comm_ring B] [comm_ring C] [ A] [ B] [ C] {f : A →ₐ[R] B} {g : B →ₐ[R] C} (hf : f.finite_type) (hg : function.surjective g) :
theorem alg_hom.finite_type.of_surjective {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [ A] [ B] (f : A →ₐ[R] B) (hf : function.surjective f) :
theorem alg_hom.finite_type.of_finite_presentation {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [ A] [ B] {f : A →ₐ[R] B} (hf : f.finite_presentation) :
theorem alg_hom.finite_type.of_comp_finite_type {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_ring R] [comm_ring A] [comm_ring B] [comm_ring C] [ A] [ B] [ C] {f : A →ₐ[R] B} {g : B →ₐ[R] C} (h : (g.comp f).finite_type) :
theorem alg_hom.finite_presentation.id (R : Type u_1) (A : Type u_2) [comm_ring R] [comm_ring A] [ A] :
theorem alg_hom.finite_presentation.comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_ring R] [comm_ring A] [comm_ring B] [comm_ring C] [ A] [ B] [ C] {g : B →ₐ[R] C} {f : A →ₐ[R] B} (hg : g.finite_presentation) (hf : f.finite_presentation) :
theorem alg_hom.finite_presentation.comp_surjective {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_ring R] [comm_ring A] [comm_ring B] [comm_ring C] [ A] [ B] [ C] {f : A →ₐ[R] B} {g : B →ₐ[R] C} (hf : f.finite_presentation) (hg : function.surjective g) (hker : .fg) :
theorem alg_hom.finite_presentation.of_surjective {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [ A] [ B] (f : A →ₐ[R] B) (hf : function.surjective f) (hker : .fg) :
theorem alg_hom.finite_presentation.of_finite_type {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [ A] [ B] {f : A →ₐ[R] B} :

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

theorem add_monoid_algebra.support_gen_of_gen {R : Type u_1} {M : Type u_2} [add_monoid M] {S : set M)} (hS : = ) :
(⋃ (f : (H : f S), '' (f.support)) =

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

theorem add_monoid_algebra.support_gen_of_gen' {R : Type u_1} {M : Type u_2} [add_monoid M] {S : set M)} (hS : = ) :
'' ⋃ (f : (H : f S), (f.support)) =

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

theorem add_monoid_algebra.exists_finset_adjoin_eq_top {R : Type u_1} {M : Type u_2} [comm_ring R] [h : M)] :
∃ (G : finset M), '' G) =

If add_monoid_algebra R M is of finite type, there there is a G : finset M such that its image generates, as algera, add_monoid_algebra R M.

theorem add_monoid_algebra.of'_mem_span {R : Type u_1} {M : Type u_2} [comm_ring R] [nontrivial R] {m : M} {S : set M} :
'' S) m S

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

theorem add_monoid_algebra.mem_closure_of_mem_span_closure {R : Type u_1} {M : Type u_2} [comm_ring R] [nontrivial R] {m : M} {S : set M} (h : (submonoid.closure '' S))) :

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

theorem add_monoid_algebra.mv_polynomial_aeval_of_surjective_of_closure {R : Type u_1} {M : Type u_2} {S : set M} (hS : = ) :

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

@[protected, instance]
def add_monoid_algebra.finite_type_of_fg (R : Type u_1) (M : Type u_2) [comm_ring R] [h : add_monoid.fg M] :

If an additive monoid M is finitely generated then add_monoid_algebra R M is of finite type.

theorem add_monoid_algebra.finite_type_iff_fg {R : Type u_1} {M : Type u_2} [comm_ring R] [nontrivial R] :

An additive monoid M is finitely generated if and only if add_monoid_algebra R M is of finite type.

theorem add_monoid_algebra.fg_of_finite_type {R : Type u_1} {M : Type u_2} [comm_ring R] [nontrivial R] [h : M)] :

If add_monoid_algebra R M is of finite type then M is finitely generated.

theorem add_monoid_algebra.finite_type_iff_group_fg {R : Type u_1} {G : Type u_2} [comm_ring R] [nontrivial R] :

An additive group G is finitely generated if and only if add_monoid_algebra R G is of finite type.

theorem monoid_algebra.mem_adjoin_support {R : Type u_1} {M : Type u_2} [monoid M] (f : M) :
f ( M) '' (f.support))

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

theorem monoid_algebra.support_gen_of_gen {R : Type u_1} {M : Type u_2} [monoid M] {S : set M)} (hS : = ) :
(⋃ (f : M) (H : f S), M) '' (f.support)) =

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

theorem monoid_algebra.support_gen_of_gen' {R : Type u_1} {M : Type u_2} [monoid M] {S : set M)} (hS : = ) :
( M) '' ⋃ (f : M) (H : f S), (f.support)) =

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

theorem monoid_algebra.exists_finset_adjoin_eq_top {R : Type u_1} {M : Type u_2} [comm_ring R] [comm_monoid M] [h : M)] :
∃ (G : finset M), ( M) '' G) =

If monoid_algebra R M is of finite type, there there is a G : finset M such that its image generates, as algera, monoid_algebra R M.

theorem monoid_algebra.of_mem_span_of_iff {R : Type u_1} {M : Type u_2} [comm_ring R] [comm_monoid M] [nontrivial R] {m : M} {S : set M} :
M) m ( M) '' S) m S

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

theorem monoid_algebra.mem_closure_of_mem_span_closure {R : Type u_1} {M : Type u_2} [comm_ring R] [comm_monoid M] [nontrivial R] {m : M} {S : set M} (h : M) m (submonoid.closure ( M) '' S))) :

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

theorem monoid_algebra.mv_polynomial_aeval_of_surjective_of_closure {R : Type u_1} {M : Type u_2} [comm_monoid M] {S : set M} (hS : = ) :

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

@[protected, instance]
def monoid_algebra.finite_type_of_fg {R : Type u_1} {M : Type u_2} [comm_monoid M] [comm_ring R] [monoid.fg M] :

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

theorem monoid_algebra.finite_type_iff_fg {R : Type u_1} {M : Type u_2} [comm_monoid M] [comm_ring R] [nontrivial R] :

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

theorem monoid_algebra.fg_of_finite_type {R : Type u_1} {M : Type u_2} [comm_monoid M] [comm_ring R] [nontrivial R] [h : M)] :

If monoid_algebra R M is of finite type then M is finitely generated.

theorem monoid_algebra.finite_type_iff_group_fg {R : Type u_1} {G : Type u_2} [comm_group G] [comm_ring R] [nontrivial R] :

A group G is finitely generated if and only if add_monoid_algebra R G is of finite type.

noncomputable def module_polynomial_of_endo {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] (f : M →ₗ[R] M) :

The structure of a module M over a ring R as a module over polynomial R when given a choice of how X acts by choosing a linear map f : M →ₗ[R] M

Equations
theorem module_polynomial_of_endo_smul_def {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] (f : M →ₗ[R] M) (n : polynomial R) (a : M) :
n a = ( n) a
theorem module_polynomial_of_endo.is_scalar_tower {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] (f : M →ₗ[R] M) :
M
theorem module.finite.injective_of_surjective_endomorphism {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] (f : M →ₗ[R] M) [hfg : M] (f_surj : function.surjective f) :

A theorem/proof by Vasconcelos, given a finite module M over a commutative ring, any surjective endomorphism of M is also injective. Based on, https://math.stackexchange.com/a/239419/31917, https://www.ams.org/journals/tran/1969-138-00/S0002-9947-1969-0238839-5/. This is similar to is_noetherian.injective_of_surjective_endomorphism but only applies in the commutative case, but does not use a Noetherian hypothesis.