TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A Sylvester equation is uniquely solvable exactly when the spectra are disjoint

Statement

Let $F \in {R, C}$ , $m, n \geq 1$ , $A \in F^{m \times m}$ and $B \in F^{n \times n}$ . Spectra of real matrices are taken over $C$ . The map $S_{A, B}$ of Sylvester operator and Frobenius separation number is invertible if and only if

σ (A) \cap (- σ (B)) = \emptyset .

Equivalently, for every $C \in F^{m \times n}$ , the equation $A X + X B = C$ has a unique solution if and only if this spectral condition holds. The same condition is equivalent to $sep (A, - B) > 0$ .

Facts & Assumptions

Given: The fields, dimensions and matrices in the statement.

[F1]

Column vectorization is an isometry and represents the Sylvester map by a Kronecker sum: $vec (A X + X B) = (I_{n} \otimes A + B^{T} \otimes I_{m}) vec (X)$ , and $vec$ preserves the Frobenius norm.

[F2]

If the characteristic polynomial of an endomorphism splits, some orthonormal basis makes its matrix upper triangular: If a finite-dimensional complex endomorphism has a characteristic polynomial that splits, an orthonormal basis makes its matrix upper triangular.

[F3]

Sylvester operator and Frobenius separation number: $sep (A, - B)$ is the smallest singular value of $S_{A, B}$ under the Frobenius inner product.

[F4]

Every linear map between finite-dimensional real or complex inner product spaces admits a singular value decomposition: A linear map between finite-dimensional inner product spaces has orthonormal singular directions; its smallest singular value is positive exactly when its kernel is zero.

[F5]

The characteristic polynomial of a block upper- or lower-triangular matrix is the product of the characteristic polynomials of its diagonal blocks: The characteristic polynomial of a block-triangular matrix is the product of the characteristic polynomials of its diagonal blocks.

[F6]

For $A \in M_{n} (F)$ , the characteristic polynomial is $χ_{A} (x) = \det (x I_{n} - A)$ when $n \geq 1$ , with $χ_{A} (x) = 1$ for the unique $0 \times 0$ matrix: $χ_{L} (x) = \det (x I - L)$ for a finite square matrix $L$ .

[F7]

For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix: The determinant is the signed Leibniz sum, so for a $d \times d$ matrix $L$ , $\det (- L) = (- 1)^{d} \det (L)$ .

[F8]

A finite-dimensional linear operator over a field is invertible if and only if its determinant is nonzero: A finite-dimensional square operator is invertible exactly when its determinant is nonzero.

[F9]

The determinant of a triangular matrix is the product of its diagonal entries: The determinant of a triangular matrix is the product of its diagonal entries.

[F10]

The complex numbers are algebraically closed: Every nonconstant complex polynomial splits over $C$ .

Proof

1.1givenF2F10constructalgebra

First let $F = C$ . The characteristic polynomials of $A$ and $B$ split by [F10], so [F2] gives unitary $U, V$ and upper triangular $T, S$ with $A = U T U^{*}$ and $B = V S V^{*}$ . Set $Y = U^{*} X V$ and $D = U^{*} C V$ ; multiplying $A X + X B = C$ on the left by $U^{*}$ and right by $V$ gives $T Y + Y S = D$ , and this change of variables is invertible.

1.2F1F5F6F7F8F9algebra

By [F1], the vectorized map for $Y \mapsto T Y + Y S$ is $K = I_{n} \otimes T + S^{T} \otimes I_{m}$ . Viewed in $m$ -entry column blocks, $K$ is block lower triangular because $S^{T}$ is lower triangular; its $j$ th diagonal block is $K_{j} = T + s_{j j} I_{m}$ , which is upper triangular with diagonal entries $t_{i i} + s_{j j}$ . Recursively applying [F5] to the first diagonal block and the remaining block gives $χ_{K} (x) = \prod_{j = 1}^{n} χ_{K_{j}} (x)$ . At $x = 0$ , [F6] and [F7] give $(- 1)^{m n} \det K = \prod_{j = 1}^{n} ((- 1)^{m} \det K_{j})$ , so $\det K = \prod_{j = 1}^{n} \det K_{j}$ . By [F8], $K$ is invertible exactly when every $K_{j}$ is invertible. Each $K_{j}$ is triangular, so [F9] and [F8] show it is invertible exactly when every diagonal entry $t_{i i} + s_{j j}$ is nonzero.

2.1F8F9step 1.2algebra

Since $A = U T U^{*}$ and $B = V S V^{*}$ with $U, V$ unitary, $A - λ I = U (T - λ I) U^{*}$ and $B - λ I = V (S - λ I) V^{*}$ ; these factors are invertible exactly when the corresponding middle factor is, so $σ (A) = σ (T)$ and $σ (B) = σ (S)$ . By [F9], $\det (T - λ I) = \prod_{i} (t_{i i} - λ)$ and $\det (S - λ I) = \prod_{j} (s_{j j} - λ)$ ; [F8] therefore gives $σ (A) = {t_{i i}}$ and $σ (B) = {s_{j j}}$ . Thus step 1.2 says that $S_{A, B}$ is invertible exactly when $σ (A) \cap (- σ (B)) = \emptyset$ .

3.1F1step 2.1algebra

For real $A, B$ , the matrix $K = I_{n} \otimes A + B^{T} \otimes I_{m}$ has real entries, and its real determinant is nonzero exactly when it is nonzero over $C$ . Applying the complex criterion from step 2.1 to this same real matrix viewed over $C$ therefore gives the same spectral condition for invertibility over $R$ .

4.1F3F4step 2.1step 3.1algebra∎

A square finite-dimensional linear map is bijective exactly when every right-hand side has one solution. By [F3] and [F4], its smallest singular value is positive exactly when it is invertible. This proves all equivalences.

Depends on

Used by

Dependency tree · two levels

54 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Valeria Simoncini, Computational Methods for Linear Matrix Equations, SIAM Review 58(3), 2016 (standard reference, not scraped)
Elias Jarlebring, Numerical Methods for Lyapunov Equations, lecture notes in numerical linear algebra, 2017 (standard reference, not scraped)