mathlib3 documentation

ring_theory.finite_type

Finiteness conditions in commutative algebra #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define a notion of finiteness that is common in commutative algebra.

Main declarations #

source
@[class]
structure algebra.finite_type (R : Type u_1) (A : Type u_2) [comm_semiring R] [semiring A] [algebra R 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
source
@[protected, instance]
def module.finite.finite_type {R : Type u_1} (A : Type u_2) [comm_semiring R] [semiring A] [algebra R A] [hRA : module.finite R A] :
algebra.finite_type R A
source
theorem algebra.finite_type.self (R : Type u_1) [comm_ring R] :
algebra.finite_type R R
source
@[protected]
theorem algebra.finite_type.polynomial (R : Type u_1) [comm_ring R] :
algebra.finite_type R (polynomial R)
source
@[protected]
theorem algebra.finite_type.mv_polynomial (R : Type u_1) [comm_ring R] (ι : Type u_2) [finite ι] :
algebra.finite_type R (mv_polynomial ι R)
source
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] [algebra R A] [comm_ring B] [algebra R B] [algebra A B] [is_scalar_tower R A B] [hB : algebra.finite_type R B] :
algebra.finite_type A B
source
theorem algebra.finite_type.of_surjective {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [algebra R A] [comm_ring B] [algebra R B] (hRA : algebra.finite_type R A) (f : A →ₐ[R] B) (hf : function.surjective ⇑f) :
algebra.finite_type R B
source
theorem algebra.finite_type.equiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [algebra R A] [comm_ring B] [algebra R B] (hRA : algebra.finite_type R A) (e : A ≃ₐ[R] B) :
algebra.finite_type R B
source
theorem algebra.finite_type.trans {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [algebra R A] [comm_ring B] [algebra R B] [algebra A B] [is_scalar_tower R A B] (hRA : algebra.finite_type R A) (hAB : algebra.finite_type A B) :
algebra.finite_type R B
source
theorem algebra.finite_type.iff_quotient_mv_polynomial {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] :
algebra.finite_type R A ↔ ∃ (s : finset A) (f : mv_polynomial {x // x ∈ s} R →ₐ[R] A), function.surjective ⇑f

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

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

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

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

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

source
@[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] [algebra R A] [comm_ring B] [algebra R B] [hA : algebra.finite_type R A] [hB : algebra.finite_type R B] :
algebra.finite_type R (A × B)
source
theorem algebra.finite_type.is_noetherian_ring (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [algebra R S] [h : algebra.finite_type R S] [is_noetherian_ring R] :
is_noetherian_ring S
source
theorem subalgebra.fg_iff_finite_type {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
S.fg ↔ algebra.finite_type R ↥S
source
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
source
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) :
f.finite_type
source
theorem ring_hom.finite_type.id (A : Type u_1) [comm_ring A] :
(ring_hom.id A).finite_type
source
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) :
(g.comp f).finite_type
source
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) :
f.finite_type
source
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) :
(g.comp f).finite_type
source
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) :
f.finite_type
source
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) :
f.finite_type

Alias of ring_hom.finite_type.of_finite.

source
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) :
g.finite_type
source
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] [algebra R A] [algebra R 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
source
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] [algebra R A] [algebra R B] {f : A →ₐ[R] B} (hf : f.finite) :
f.finite_type
source
theorem alg_hom.finite_type.id (R : Type u_1) (A : Type u_2) [comm_ring R] [comm_ring A] [algebra R A] :
(alg_hom.id R A).finite_type
source
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] [algebra R A] [algebra R B] [algebra R C] {g : B →ₐ[R] C} {f : A →ₐ[R] B} (hg : g.finite_type) (hf : f.finite_type) :
(g.comp f).finite_type
source
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] [algebra R A] [algebra R B] [algebra R C] {f : A →ₐ[R] B} {g : B →ₐ[R] C} (hf : f.finite_type) (hg : function.surjective ⇑g) :
(g.comp f).finite_type
source
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] [algebra R A] [algebra R B] (f : A →ₐ[R] B) (hf : function.surjective ⇑f) :
f.finite_type
source
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] [algebra R A] [algebra R B] [algebra R C] {f : A →ₐ[R] B} {g : B →ₐ[R] C} (h : (g.comp f).finite_type) :
g.finite_type
source
theorem add_monoid_algebra.mem_adjoin_support {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_monoid M] (f : add_monoid_algebra R M) :
f ∈ algebra.adjoin R (add_monoid_algebra.of' R M '' ↑(f.support))

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

source
theorem add_monoid_algebra.support_gen_of_gen {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_monoid M] {S : set (add_monoid_algebra R M)} (hS : algebra.adjoin R S = ⊤) :
algebra.adjoin R (⋃ (f : add_monoid_algebra R M) (H : f ∈ S), add_monoid_algebra.of' R M '' ↑(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.

source
theorem add_monoid_algebra.support_gen_of_gen' {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_monoid M] {S : set (add_monoid_algebra R M)} (hS : algebra.adjoin R S = ⊤) :
algebra.adjoin R (add_monoid_algebra.of' R M '' ⋃ (f : add_monoid_algebra R M) (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.

source
theorem add_monoid_algebra.exists_finset_adjoin_eq_top {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_monoid M] [h : algebra.finite_type R (add_monoid_algebra R M)] :
∃ (G : finset M), algebra.adjoin R (add_monoid_algebra.of' R 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.

source
theorem add_monoid_algebra.of'_mem_span {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_monoid M] [nontrivial R] {m : M} {S : set M} :
add_monoid_algebra.of' R M m ∈ submodule.span R (add_monoid_algebra.of' R 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.

source
theorem add_monoid_algebra.mem_closure_of_mem_span_closure {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_monoid M] [nontrivial R] {m : M} {S : set M} (h : add_monoid_algebra.of' R M m ∈ submodule.span R ↑(submonoid.closure (add_monoid_algebra.of' R M '' S))) :
m ∈ add_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.

source
theorem add_monoid_algebra.mv_polynomial_aeval_of_surjective_of_closure {R : Type u_1} {M : Type u_2} [add_comm_monoid M] [comm_semiring R] {S : set M} (hS : add_submonoid.closure S = ⊤) :
function.surjective ⇑(mv_polynomial.aeval (λ (s : ↥S), add_monoid_algebra.of' R M ↑s))

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

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

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

source
theorem add_monoid_algebra.finite_type_iff_fg {R : Type u_1} {M : Type u_2} [add_comm_monoid M] [comm_ring R] [nontrivial R] :
algebra.finite_type R (add_monoid_algebra R M) ↔ add_monoid.fg M

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

source
theorem add_monoid_algebra.fg_of_finite_type {R : Type u_1} {M : Type u_2} [add_comm_monoid M] [comm_ring R] [nontrivial R] [h : algebra.finite_type R (add_monoid_algebra R M)] :
add_monoid.fg M

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

source
theorem add_monoid_algebra.finite_type_iff_group_fg {R : Type u_1} {G : Type u_2} [add_comm_group G] [comm_ring R] [nontrivial R] :
algebra.finite_type R (add_monoid_algebra R G) ↔ add_group.fg G

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

source
theorem monoid_algebra.mem_adjoin_support {R : Type u_1} {M : Type u_2} [comm_semiring R] [monoid M] (f : monoid_algebra R M) :
f ∈ algebra.adjoin R (⇑(monoid_algebra.of R M) '' ↑(f.support))

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

source
theorem monoid_algebra.support_gen_of_gen {R : Type u_1} {M : Type u_2} [comm_semiring R] [monoid M] {S : set (monoid_algebra R M)} (hS : algebra.adjoin R S = ⊤) :
algebra.adjoin R (⋃ (f : monoid_algebra R M) (H : f ∈ S), ⇑(monoid_algebra.of R 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.

source
theorem monoid_algebra.support_gen_of_gen' {R : Type u_1} {M : Type u_2} [comm_semiring R] [monoid M] {S : set (monoid_algebra R M)} (hS : algebra.adjoin R S = ⊤) :
algebra.adjoin R (⇑(monoid_algebra.of R M) '' ⋃ (f : monoid_algebra R 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.

source
theorem monoid_algebra.exists_finset_adjoin_eq_top {R : Type u_1} {M : Type u_2} [comm_ring R] [comm_monoid M] [h : algebra.finite_type R (monoid_algebra R M)] :
∃ (G : finset M), algebra.adjoin R (⇑(monoid_algebra.of R 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.

source
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} :
⇑(monoid_algebra.of R M) m ∈ submodule.span R (⇑(monoid_algebra.of R 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.

source
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 : ⇑(monoid_algebra.of R M) m ∈ submodule.span R ↑(submonoid.closure (⇑(monoid_algebra.of R M) '' S))) :
m ∈ submonoid.closure 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.

source
theorem monoid_algebra.mv_polynomial_aeval_of_surjective_of_closure {R : Type u_1} {M : Type u_2} [comm_monoid M] [comm_semiring R] {S : set M} (hS : submonoid.closure S = ⊤) :
function.surjective ⇑(mv_polynomial.aeval (λ (s : ↥S), ⇑(monoid_algebra.of R M) ↑s))

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

source
@[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] :
algebra.finite_type R (monoid_algebra R M)

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

source
theorem monoid_algebra.finite_type_iff_fg {R : Type u_1} {M : Type u_2} [comm_monoid M] [comm_ring R] [nontrivial R] :
algebra.finite_type R (monoid_algebra R M) ↔ monoid.fg M

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

source
theorem monoid_algebra.fg_of_finite_type {R : Type u_1} {M : Type u_2} [comm_monoid M] [comm_ring R] [nontrivial R] [h : algebra.finite_type R (monoid_algebra R M)] :
monoid.fg M

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

source
theorem monoid_algebra.finite_type_iff_group_fg {R : Type u_1} {G : Type u_2} [comm_group G] [comm_ring R] [nontrivial R] :
algebra.finite_type R (monoid_algebra R G) ↔ group.fg G

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

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

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

Equations
source
theorem module_polynomial_of_endo_smul_def {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] (f : M →ₗ[R] M) (n : polynomial R) (a : M) :
n • a = ⇑(⇑(polynomial.aeval f) n) a
source
theorem module_polynomial_of_endo.is_scalar_tower {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] (f : M →ₗ[R] M) :
is_scalar_tower R (polynomial R) M
source
theorem module.finite.injective_of_surjective_endomorphism {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] (f : M →ₗ[R] M) [hfg : module.finite R M] (f_surj : function.surjective ⇑f) :
function.injective ⇑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.