Formal proofs of operator identities by a single formal computation
From MaRDI portal
Abstract: A formal computation proving a new operator identity from known ones is, in principle, restricted by domains and codomains of linear operators involved, since not any two operators can be added or composed. Algebraically, identities can be modelled by noncommutative polynomials and such a formal computation proves that the polynomial corresponding to the new identity lies in the ideal generated by the polynomials corresponding to the known identities. In order to prove an operator identity, however, just proving membership of the polynomial in the ideal is not enough, since the ring of noncommutative polynomials ignores domains and codomains. We show that it suffices to additionally verify compatibility of this polynomial and of the generators of the ideal with the labelled quiver that encodes which polynomials can be realized as linear operators. Then, for every consistent representation of such a quiver in a linear category, there exists a computation in the category that proves the corresponding instance of the identity. Moreover, by assigning the same label to several edges of the quiver, the algebraic framework developed allows to model different versions of an operator by the same indeterminate in the noncommutative polynomials.
Recommendations
- Computing elements of certain form in ideals to prove properties of operators
- scientific article; zbMATH DE number 3014016
- Certifying operator identities via noncommutative Gröbner bases
- Computable identities in the algebra of formal matrices
- Compatible rewriting of noncommutative polynomials for proving operator identities
- Identities for a derivation operator and their applications
- Characterizing propositional proofs as noncommutative formulas
Cites work
- scientific article; zbMATH DE number 705057 (Why is no real title available?)
- Algebraic properties of generalized inverses
- An introduction to commutative and noncommutative Gröbner bases
- Bruno Buchberger's PhD thesis 1965: An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal. Translation from the German
- Certifying operator identities via noncommutative Gröbner bases
- Compatible rewriting of noncommutative polynomials for proving operator identities
- Computer assistance for ``discovering formulas in system engineering and operator theory
- Computer simplification of formulas in linear systems theory
- Convergent presentations and polygraphic resolutions of associative algebras
- Formally verifying proofs for algebraic identities of matrices
- Gröbner-Shirshov bases for categories.
- HOMOLOGICAL ALGEBRA OF TWISTED QUIVER BUNDLES
- On Deriving the Inverse of a Sum of Matrices
- Quiver representations.
- Solving polynomial equation systems. Vol. IV. Buchberger theory and beyond
- Standard Gröbner-Shirshov Bases of Free Algebras Over Rings, I
- The diamond lemma for ring theory
- Using noncommutative Gröbner bases in solving partially prescribed matrix inverse completion problems
Cited in
(8)- Certifying operator identities via noncommutative Gröbner bases
- Signature Gröbner bases in free algebras over rings
- Formally verifying proofs for algebraic identities of matrices
- Computing elements of certain form in ideals to prove properties of operators
- Signature Gröbner bases, bases of syzygies and cofactor reconstruction in the free algebra
- Algebraic proof methods for identities of matrices and operators: improvements of Hartwig's triple reverse order law
- How to Automatise Proofs of Operator Statements: Moore–Penrose Inverse; A Case Study
- Short proofs of ideal membership
This page was built for publication: Formal proofs of operator identities by a single formal computation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2223357)
