Matrix-J-unitary non-commutative rational formal power series

In this paper, a theory of realization and minimal factorization of rational matrix-valued functions which are $J$-unitary on the imaginary line or on the unit circle is extended to the setting of non-commutative rational formal power series. The property of $J$-unitarity holds on $N$-tuples of $n\times n$ skew-Hermitian versus unitary matrices ($n=1,2,...$), and a rational formal power series is called \emph{matrix-$J$-unitary} in this case. The close relationship between minimal realizations and structured Hermitian solutions $H$ of the Lyapunov or Stein equations is established. The results are specialized for the case of \emph{matrix-$J$-inner} rational formal power series. In this case $H>0$, however the proof of that is more elaborated than in the one-variable case and involves a new technique. For the rational \emph{matrix-inner} case, i.e., when $J=I$, the theorem of Ball, Groenewald and Malakorn on unitary realization of a formal power series from the non-commutative Schur--Agler class admits an improvement: its finite-dimensionality and uniqueness up to a unitary similarity is proved. A version of the theory for \emph{matrix-selfadjoint} rational formal power series is also presented. The concept of non-commutative formal reproducing kernel Pontryagin spaces is introduced, and in this framework the backward shift realization of a matrix-$J$-unitary rational formal power series in a finite-dimensional non-commutative de Branges--Rovnyak space is described.