Documentation

Mathlib.RingTheory.FiniteType

Finiteness conditions in commutative algebra #

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

Main declarations #

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

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

Instances
    instance Module.Finite.finiteType {R : Type u_1} (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [hRA : Module.Finite R A] :
    Equations
    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) :
    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) :
    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) :
    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.

    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.

    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] :
    Equations
    def RingHom.FiniteType {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (f : A →+* B) :

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

    Equations
    Instances For
      theorem RingHom.Finite.finiteType {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] {f : A →+* B} (hf : RingHom.Finite f) :
      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) :
      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) :
      theorem RingHom.FiniteType.of_finite {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] {f : A →+* B} (hf : RingHom.Finite f) :
      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)) :
      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) :

      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
      Instances For
        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) :
        theorem AlgHom.FiniteType.id (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Algebra 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) :
        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) :
        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) :
        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)) :

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

        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} :

        The image of an element m : M in R[M] belongs the submodule generated by S : Set M if and only if m ∈ 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.

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

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

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

        Equations

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

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

        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} :

        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.

        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.

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

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

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

        Equations

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

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

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

        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.