Topological properties of matrices #
Mathlib gives Matrix m n α the product topology of m → n → α, so for finite index types it is
pseudo-metrizable whenever α is. This makes metrizable-codomain results, such as measurability
of pointwise limits of measurable maps, available for matrix-valued functions without choosing a
matrix norm.
Matrices with countably many rows and columns are second countable when their entries are, and matrices with finitely many rows and columns are σ-compact when their entries are.
Square matrices act jointly continuously on column vectors by Matrix.mulVec, the action of
Mathlib.LinearAlgebra.Matrix.Action; through the unit group, so does GL n R
(Units.continuousSMul).
The same product topology gives entrywise control of a real matrix-valued map near a point of
continuity, again without a matrix norm
(ContinuousAt.exists_ball_subset_forall_abs_sub_le), and the product uniformity gives the
uniform version for uniformly continuous maps (UniformContinuous.exists_pos_forall_abs_sub_le).
Over a topological field, the inverse of a matrix-valued function that is continuous at a point
with invertible value is continuous there (ContinuousAt.matrix_inv), and so are its entries
(ContinuousAt.matrix_inv_apply).
Square matrices over a commutative topological ring R with open units again have open units
(Matrix.instIsOpenUnits). The invertible matrices are the preimage of the open set of units of
R under the continuous determinant, and the inverse A⁻¹ = (det A)⁻¹ • adj A is continuous on
them because the inverse of the determinant is. Over a nonarchimedean local field E, which has
open units because it is a Hausdorff topological field, this says that GL_n(E) with the
topology of the unit group is the open subspace {det ≠ 0} of the matrices M_n(E). The
hypothesis on R cannot be dropped: over the adeles, inversion is not continuous on the units
for the subspace topology, already for n = 1.
Each characteristic coefficient is continuous over a commutative topological ring
(Matrix.continuous_charpoly_coeff). The proof uses Mathlib's universal characteristic polynomial
Matrix.charpoly.univ, whose coefficients are multivariate polynomials in the matrix entries.
The Kronecker product of two continuously varying matrices is continuous in the product topology.
In particular the ⋆-algebra homomorphisms A ↦ A ⊗ₖ 1 and B ↦ 1 ⊗ₖ B are continuous.
The matrices with nonnegative diagonal form a closed set
(Matrix.isClosed_setOfPred_nonneg_diag).
References #
- B. Conrad, Weil and Grothendieck approaches to adelic points, Enseign. Math. (2) 58 (2012), §3, pp. 3–4.
A space of matrices with finitely many rows and columns over a pseudo-metrizable space is pseudo-metrizable.
Matrices with countably many rows and columns over a second-countable space are second countable.
Matrices with finitely many rows and columns over a σ-compact space form a σ-compact space.
Square matrices act jointly continuously on column vectors by Matrix.mulVec.
If a real matrix-valued map a on a pseudo-metric space is continuous at x, then for every
neighbourhood s of x and every ε > 0 there is a ball B(x, r) ⊆ s on which every entry of
a differs from its value at x by at most ε.
If a real matrix-valued map a on a pseudo-metric space is uniformly continuous, then for every
ε > 0 there is r > 0 such that every entry of a varies by at most ε between any two points
at distance less than r.
The inverse of a matrix-valued function is continuous at every point where the function is continuous and its value is invertible.
The entries of the inverse of a matrix-valued function are continuous at every point where the function is continuous and its value is invertible.
Every characteristic coefficient is continuous for the entrywise matrix topology.
Square matrices over a commutative topological ring with open units have open units: the invertible matrices form an open set on which inversion is continuous.
The Kronecker product of two continuous matrix-valued functions is continuous.
The matrices with nonnegative diagonal form a closed set.