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

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

• out : ⊤.FG

theorem Algebra.FiniteType.out {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] [self : Algebra.FiniteType R A] : ⊤.FG

@[instance 100]

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

• ⋯ = ⋯

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 : Finset A) (f : FreeAlgebra R { x : A // x ∈ s } →ₐ[R] A), 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 : Finset S) (f : MvPolynomial { x : S // x ∈ s } R →ₐ[R] S), 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 ↔ ∃ (ι : Type uA) (x : Fintype ι) (f : FreeAlgebra 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.

theorem Algebra.FiniteType.iff_quotient_mvPolynomial' {R : Type uR} {S : Type uS} [CommSemiring R] [CommSemiring S] [Algebra R S] : Algebra.FiniteType R S ↔ ∃ (ι : Type uS) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] S), 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 : MvPolynomial (Fin n) R →ₐ[R] S), 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

• ⋯ = ⋯

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) : S.FG ↔ Algebra.FiniteType R ↥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

• f.FiniteType = Algebra.FiniteType A B

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

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

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 : f.FiniteType) (hg : Function.Surjective ⇑g) : (g.comp f).FiniteType

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

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 : g.FiniteType) (hf : f.FiniteType) : (g.comp f).FiniteType

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

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

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 : (g.comp f).FiniteType) : g.FiniteType

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

• f.FiniteType = f.FiniteType

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 : f.Finite) : f.FiniteType

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

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 : g.FiniteType) (hf : f.FiniteType) : (g.comp f).FiniteType

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 : f.FiniteType) (hg : Function.Surjective ⇑g) : (g.comp f).FiniteType

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) : f.FiniteType

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 : (g.comp f).FiniteType) : g.FiniteType

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 ∈ 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 ∈ 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 : Finset M), 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 : ↑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 : ↑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

• ⋯ = ⋯

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 ∈ 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 ∈ 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 : Finset M), 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 : ↑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 : ↑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

• ⋯ = ⋯

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.

theorem Module.Finite.injective_of_surjective_endomorphism {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [Module.Finite R M] (f : M →ₗ[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.