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
    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] :
    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
    • =
    theorem Subalgebra.fg_iff_finiteType {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
    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 : 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) :

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

        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 (fS, 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 '' fS, 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 (fS, (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) '' fS, 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.

        @[instance 100]

        Any commutative ring R satisfies the OrzechProperty, that is, for any finitely generated R-module M, any surjective homomorphism f : N →ₗ[R] M from a submodule N of M to M is injective.

        This is a consequence of Noetherian case (IsNoetherian.injective_of_surjective_of_injective), which requires that M is a Noetherian module, but allows R to be non-commutative. The reduction of this result to Noetherian case is adapted from https://math.stackexchange.com/a/1066110: suppose { m_j } is a finite set of generator of M, for any n : N one can write i n = ∑ j, b_j * m_j for { b_j } in R, here i : N →ₗ[R] M is the standard inclusion. We can choose { n_j } which are preimages of { m_j } under f, and can choose { c_jl } in R such that i n_j = ∑ l, c_jl * m_l for each j. Now let A be the subring of R generated by { b_j } and { c_jl }, then it is Noetherian. Let N' be the A-submodule of N generated by n and { n_j }, M' be the A-submodule of M generated by { m_j }, then it's easy to see that i and f restrict to N' →ₗ[A] M', and the restricted version of f is surjective, hence by Noetherian case, it is also injective, in particular, if f n = 0, then n = 0.

        See also Orzech's original paper: Onto endomorphisms are isomorphisms [orzech1971].

        Equations
        • =
        @[deprecated OrzechProperty.injective_of_surjective_endomorphism]

        A theorem by Vasconcelos, given a finite module M over a commutative ring, any surjective endomorphism of M is also injective. It is a consequence of the fact CommRing.orzechProperty that any commutative ring R satisfies the OrzechProperty; please use OrzechProperty.injective_of_surjective_endomorphism instead. This is similar to IsNoetherian.injective_of_surjective_endomorphism but only applies in the commutative case, but does not use a Noetherian hypothesis.