The goal of this Master's thesis is to present the theory of Gröbner bases of ideals in the ring of non-commutative polynomials, and the three main algorithms for computing them, Buchberger's algorithm and Faugère's $F_4$ and $F_5$ algorithms. We start with the basic theory of non-commutative polynomials, present the division algorithm, define Gröbner bases of ideals of non-commutative polynomials, and prove some of their fundamental properties. We continue with the classical Buchberger's algorithm, introduce the concept of obstruction sets, and follow the steps of Teo Mora to the non-commutative version of the algorithm. Doing so, we use Dickson's lemma to show that the original Buchberger's algorithm terminates, and we prove the non-commutative version of Bucherger's Criterion and correctness of the non-commutative version of Buchberger's algorithm. We show how to transform sets of polynomials into matrices, and simultaneously formulate the commutative and non-commutative $F_4$ algorithm. We prove the correctness of the $F_4$ algorithm, and we prove it terminates if a finite Gröbner basis exists for the given ideal. For a finite set of polynomials, we define the syzygy module and prove some of its basic properties. We lift Buchberger's theory into a free module over the ring of commutative polynomials and define polynomial signatures. We present the principal representative of the family of signature-based algorithms and prove its correctness and termination. We introduce the $F_5$ Criterion and use the signature-based algorithm to formulate the $F_5$ algorithm. We conclude by repeating the previous steps to arrive at a non-commutative signature-based algorithm and show the correctness of the non-commutative version of the $F_5$ algorithm. We prove this algorithm terminates if a finite Gröbner bases exists for the given ideal.
|
