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.FiniteType all of these express that some object is finitely generated as algebra over some base ring.

class Algebra.FiniteType (R : Type uR) (A : Type uA) [CommSemiring R] [Semiring A] [Algebra R A] : Prop

• out : Subalgebra.FG ⊤

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

instance Module.Finite.finiteType {R : Type u_1} (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [hRA : Module.Finite R A] : Algebra.FiniteType R A

Equations

• @Module.Finite.finiteType = @Module.Finite.finiteType.proof_1

theorem Algebra.FiniteType.self (R : Type uR) [CommSemiring R] : Algebra.FiniteType R R

theorem Algebra.FiniteType.polynomial (R : Type uR) [CommSemiring R] : Algebra.FiniteType R (Polynomial R)

theorem Algebra.FiniteType.freeAlgebra (R : Type uR) [CommSemiring R] (ι : Type u_1) [Finite ι] : Algebra.FiniteType R (FreeAlgebra R ι)

theorem Algebra.FiniteType.mvPolynomial (R : Type uR) [CommSemiring R] (ι : Type u_1) [Finite ι] : Algebra.FiniteType R (MvPolynomial ι R)

theorem Algebra.FiniteType.of_restrictScalars_finiteType (R : Type uR) (S : Type uS) (A : Type uA) [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [hA : Algebra.FiniteType R A] : Algebra.FiniteType S A

theorem Algebra.FiniteType.of_surjective {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (hRA : Algebra.FiniteType R A) (f : A →ₐ[R] B) (hf : Function.Surjective ↑f) : Algebra.FiniteType R B

theorem Algebra.FiniteType.equiv {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (hRA : Algebra.FiniteType R A) (e : A ≃ₐ[R] B) : Algebra.FiniteType R B

theorem Algebra.FiniteType.trans {R : Type uR} {S : Type uS} {A : Type uA} [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] (hRS : Algebra.FiniteType R S) (hSA : Algebra.FiniteType S A) : Algebra.FiniteType R A

theorem Algebra.FiniteType.iff_quotient_freeAlgebra {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] : Algebra.FiniteType R A ↔ ∃ s f, Function.Surjective ↑f

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

theorem Algebra.FiniteType.iff_quotient_mvPolynomial {R : Type uR} {S : Type uS} [CommSemiring R] [CommSemiring S] [Algebra R S] : Algebra.FiniteType R S ↔ ∃ s f, Function.Surjective ↑f

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.

theorem Algebra.FiniteType.iff_quotient_freeAlgebra' {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] : Algebra.FiniteType R A ↔ ∃ ι x f, 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.

theorem Algebra.FiniteType.iff_quotient_mvPolynomial' {R : Type uR} {S : Type uS} [CommSemiring R] [CommSemiring S] [Algebra R S] : Algebra.FiniteType R S ↔ ∃ ι x f, Function.Surjective ↑f

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.

theorem Algebra.FiniteType.iff_quotient_mvPolynomial'' {R : Type uR} {S : Type uS} [CommSemiring R] [CommSemiring S] [Algebra R S] : Algebra.FiniteType R S ↔ ∃ n f, Function.Surjective ↑f

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

instance Algebra.FiniteType.prod {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [hA : Algebra.FiniteType R A] [hB : Algebra.FiniteType R B] : Algebra.FiniteType R (A × B)

Equations

• @Algebra.FiniteType.prod = @Algebra.FiniteType.prod.proof_1

theorem Algebra.FiniteType.isNoetherianRing (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [h : Algebra.FiniteType R S] [IsNoetherianRing R] : IsNoetherianRing S

theorem Subalgebra.fg_iff_finiteType {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : Subalgebra.FG S ↔ Algebra.FiniteType R { x // x ∈ S }

def RingHom.FiniteType {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (f : A →+* B) : Prop

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

Equations

• RingHom.FiniteType f = Algebra.FiniteType A B

theorem RingHom.Finite.finiteType {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] {f : A →+* B} (hf : RingHom.Finite f) : RingHom.FiniteType f

theorem RingHom.FiniteType.id (A : Type u_1) [CommRing A] : RingHom.FiniteType (RingHom.id A)

theorem RingHom.FiniteType.comp_surjective {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommRing A] [CommRing B] [CommRing C] {f : A →+* B} {g : B →+* C} (hf : RingHom.FiniteType f) (hg : Function.Surjective ↑g) : RingHom.FiniteType (RingHom.comp g f)

theorem RingHom.FiniteType.of_surjective {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (f : A →+* B) (hf : Function.Surjective ↑f) : RingHom.FiniteType f

theorem RingHom.FiniteType.comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommRing A] [CommRing B] [CommRing C] {g : B →+* C} {f : A →+* B} (hg : RingHom.FiniteType g) (hf : RingHom.FiniteType f) : RingHom.FiniteType (RingHom.comp g f)

theorem RingHom.FiniteType.of_finite {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] {f : A →+* B} (hf : RingHom.Finite f) : RingHom.FiniteType f

theorem RingHom.Finite.to_finiteType {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] {f : A →+* B} (hf : RingHom.Finite f) : RingHom.FiniteType f

Alias of RingHom.FiniteType.of_finite.

theorem RingHom.FiniteType.of_comp_finiteType {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommRing A] [CommRing B] [CommRing C] {f : A →+* B} {g : B →+* C} (h : RingHom.FiniteType (RingHom.comp g f)) : RingHom.FiniteType g

def AlgHom.FiniteType {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) : Prop

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

• AlgHom.FiniteType f = RingHom.FiniteType ↑f

theorem AlgHom.Finite.finiteType {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] {f : A →ₐ[R] B} (hf : AlgHom.Finite f) : AlgHom.FiniteType f

theorem AlgHom.FiniteType.id (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Algebra R A] : AlgHom.FiniteType (AlgHom.id R A)

theorem AlgHom.FiniteType.comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [CommRing A] [CommRing B] [CommRing C] [Algebra R A] [Algebra R B] [Algebra R C] {g : B →ₐ[R] C} {f : A →ₐ[R] B} (hg : AlgHom.FiniteType g) (hf : AlgHom.FiniteType f) : AlgHom.FiniteType (AlgHom.comp g f)

theorem AlgHom.FiniteType.comp_surjective {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [CommRing A] [CommRing B] [CommRing C] [Algebra R A] [Algebra R B] [Algebra R C] {f : A →ₐ[R] B} {g : B →ₐ[R] C} (hf : AlgHom.FiniteType f) (hg : Function.Surjective ↑g) : AlgHom.FiniteType (AlgHom.comp g f)

theorem AlgHom.FiniteType.of_surjective {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : Function.Surjective ↑f) : AlgHom.FiniteType f

theorem AlgHom.FiniteType.of_comp_finiteType {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [CommRing A] [CommRing B] [CommRing C] [Algebra R A] [Algebra R B] [Algebra R C] {f : A →ₐ[R] B} {g : B →ₐ[R] C} (h : AlgHom.FiniteType (AlgHom.comp g f)) : AlgHom.FiniteType g

theorem AddMonoidAlgebra.mem_adjoin_support {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddMonoid M] (f : AddMonoidAlgebra R M) : f ∈ Algebra.adjoin R (AddMonoidAlgebra.of' R M '' ↑f.support)

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

theorem AddMonoidAlgebra.support_gen_of_gen {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddMonoid M] {S : Set (AddMonoidAlgebra R M)} (hS : Algebra.adjoin R S = ⊤) : Algebra.adjoin R (⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), AddMonoidAlgebra.of' R M '' ↑f.support) = ⊤

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

theorem AddMonoidAlgebra.support_gen_of_gen' {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddMonoid M] {S : Set (AddMonoidAlgebra R M)} (hS : Algebra.adjoin R S = ⊤) : Algebra.adjoin R (AddMonoidAlgebra.of' R M '' ⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), ↑f.support) = ⊤

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].

theorem AddMonoidAlgebra.exists_finset_adjoin_eq_top {R : Type u_1} {M : Type u_2} [CommRing R] [AddMonoid M] [h : Algebra.FiniteType R (AddMonoidAlgebra R M)] : ∃ G, Algebra.adjoin R (AddMonoidAlgebra.of' R M '' ↑G) = ⊤

If R[M] is of finite type, then there is a G : Finset M such that its image generates, as algebra, R[M].

theorem AddMonoidAlgebra.of'_mem_span {R : Type u_1} {M : Type u_2} [CommRing R] [AddMonoid M] [Nontrivial R] {m : M} {S : Set M} : AddMonoidAlgebra.of' R M m ∈ Submodule.span R (AddMonoidAlgebra.of' R M '' S) ↔ m ∈ S

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

theorem AddMonoidAlgebra.mem_closure_of_mem_span_closure {R : Type u_1} {M : Type u_2} [CommRing R] [AddMonoid M] [Nontrivial R] {m : M} {S : Set M} (h : AddMonoidAlgebra.of' R M m ∈ Submodule.span R ↑(Submonoid.closure (AddMonoidAlgebra.of' R M '' S))) : m ∈ AddSubmonoid.closure 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.

theorem AddMonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure {R : Type u_1} {M : Type u_2} [AddCommMonoid M] [CommSemiring R] {S : Set M} (hS : AddSubmonoid.closure S = ⊤) : Function.Surjective ↑(MvPolynomial.aeval fun s => AddMonoidAlgebra.of' R M ↑s)

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

theorem AddMonoidAlgebra.freeAlgebra_lift_of_surjective_of_closure {R : Type u_1} {M : Type u_2} [AddMonoid M] [CommSemiring R] {S : Set M} (hS : AddSubmonoid.closure S = ⊤) : Function.Surjective ↑(↑(FreeAlgebra.lift R) fun s => AddMonoidAlgebra.of' R M ↑s)

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

instance AddMonoidAlgebra.finiteType_of_fg (R : Type u_1) (M : Type u_2) [AddMonoid M] [CommRing R] [h : AddMonoid.FG M] : Algebra.FiniteType R (AddMonoidAlgebra R M)

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

Equations

• AddMonoidAlgebra.finiteType_of_fg = AddMonoidAlgebra.finiteType_of_fg.proof_1

theorem AddMonoidAlgebra.finiteType_iff_fg {R : Type u_1} {M : Type u_2} [AddMonoid M] [CommRing R] [Nontrivial R] : Algebra.FiniteType R (AddMonoidAlgebra R M) ↔ AddMonoid.FG M

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

theorem AddMonoidAlgebra.fg_of_finiteType {R : Type u_1} {M : Type u_2} [AddMonoid M] [CommRing R] [Nontrivial R] [h : Algebra.FiniteType R (AddMonoidAlgebra R M)] : AddMonoid.FG M

If R[M] is of finite type then M is finitely generated.

theorem AddMonoidAlgebra.finiteType_iff_group_fg {R : Type u_1} {G : Type u_3} [AddCommGroup G] [CommRing R] [Nontrivial R] : Algebra.FiniteType R (AddMonoidAlgebra R G) ↔ AddGroup.FG G

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

theorem MonoidAlgebra.mem_adjoin_support {R : Type u_1} {M : Type u_2} [CommSemiring R] [Monoid M] (f : MonoidAlgebra R M) : f ∈ Algebra.adjoin R (↑(MonoidAlgebra.of R M) '' ↑f.support)

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

theorem MonoidAlgebra.support_gen_of_gen {R : Type u_1} {M : Type u_2} [CommSemiring R] [Monoid M] {S : Set (MonoidAlgebra R M)} (hS : Algebra.adjoin R S = ⊤) : Algebra.adjoin R (⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑(MonoidAlgebra.of R M) '' ↑f.support) = ⊤

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

theorem MonoidAlgebra.support_gen_of_gen' {R : Type u_1} {M : Type u_2} [CommSemiring R] [Monoid M] {S : Set (MonoidAlgebra R M)} (hS : Algebra.adjoin R S = ⊤) : Algebra.adjoin R (↑(MonoidAlgebra.of R M) '' ⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑f.support) = ⊤

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.

theorem MonoidAlgebra.exists_finset_adjoin_eq_top {R : Type u_1} {M : Type u_2} [CommRing R] [Monoid M] [h : Algebra.FiniteType R (MonoidAlgebra R M)] : ∃ G, Algebra.adjoin R (↑(MonoidAlgebra.of R M) '' ↑G) = ⊤

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.

theorem MonoidAlgebra.of_mem_span_of_iff {R : Type u_1} {M : Type u_2} [CommRing R] [Monoid M] [Nontrivial R] {m : M} {S : Set M} : ↑(MonoidAlgebra.of R M) m ∈ Submodule.span R (↑(MonoidAlgebra.of R M) '' S) ↔ m ∈ S

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.

theorem MonoidAlgebra.mem_closure_of_mem_span_closure {R : Type u_1} {M : Type u_2} [CommRing R] [Monoid M] [Nontrivial R] {m : M} {S : Set M} (h : ↑(MonoidAlgebra.of R M) m ∈ Submodule.span R ↑(Submonoid.closure (↑(MonoidAlgebra.of R M) '' S))) : m ∈ Submonoid.closure 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.

theorem MonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure {R : Type u_1} {M : Type u_2} [CommMonoid M] [CommSemiring R] {S : Set M} (hS : Submonoid.closure S = ⊤) : Function.Surjective ↑(MvPolynomial.aeval fun s => ↑(MonoidAlgebra.of R M) ↑s)

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

theorem MonoidAlgebra.freeAlgebra_lift_of_surjective_of_closure {R : Type u_1} {M : Type u_2} [Monoid M] [CommSemiring R] {S : Set M} (hS : Submonoid.closure S = ⊤) : Function.Surjective ↑(↑(FreeAlgebra.lift R) fun s => ↑(MonoidAlgebra.of R M) ↑s)

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

instance MonoidAlgebra.finiteType_of_fg {R : Type u_1} {M : Type u_2} [Monoid M] [CommRing R] [Monoid.FG M] : Algebra.FiniteType R (MonoidAlgebra R M)

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

Equations

• @MonoidAlgebra.finiteType_of_fg = @MonoidAlgebra.finiteType_of_fg.proof_1

theorem MonoidAlgebra.finiteType_iff_fg {R : Type u_1} {M : Type u_2} [Monoid M] [CommRing R] [Nontrivial R] : Algebra.FiniteType R (MonoidAlgebra R M) ↔ Monoid.FG M

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

theorem MonoidAlgebra.fg_of_finiteType {R : Type u_1} {M : Type u_2} [Monoid M] [CommRing R] [Nontrivial R] [h : Algebra.FiniteType R (MonoidAlgebra R M)] : Monoid.FG M

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

theorem MonoidAlgebra.finiteType_iff_group_fg {R : Type u_1} {G : Type u_3} [Group G] [CommRing R] [Nontrivial R] : Algebra.FiniteType R (MonoidAlgebra R G) ↔ Group.FG G

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

def modulePolynomialOfEndo {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup 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

• modulePolynomialOfEndo f = Module.compHom M ↑(Polynomial.aeval f)

theorem modulePolynomialOfEndo_smul_def {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (f : M →ₗ[R] M) (n : Polynomial R) (a : M) : n • a = ↑(↑(Polynomial.aeval f) n) a

theorem modulePolynomialOfEndo.isScalarTower {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (f : M →ₗ[R] M) : IsScalarTower R (Polynomial R) M

theorem Module.Finite.injective_of_surjective_endomorphism {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup 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 IsNoetherian.injective_of_surjective_endomorphism but only applies in the commutative case, but does not use a Noetherian hypothesis.