# mathlib3documentation

topology.instances.matrix

# Topological properties of matrices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file is a place to collect topological results about matrices.

## Main definitions: #

• matrix.topological_ring: square matrices form a topological ring

## Main results #

• Continuity:
• continuous.matrix_det: the determinant is continuous over a topological ring.
• continuous.matrix_adjugate: the adjugate is continuous over a topological ring.
• Infinite sums
• matrix.transpose_tsum: transpose commutes with infinite sums
• matrix.diagonal_tsum: diagonal commutes with infinite sums
• matrix.block_diagonal_tsum: block diagonal commutes with infinite sums
• matrix.block_diagonal'_tsum: non-uniform block diagonal commutes with infinite sums
@[protected, instance]
def matrix.topological_space {m : Type u_4} {n : Type u_5} {R : Type u_8}  :
Equations
@[protected, instance]
def matrix.t2_space {m : Type u_4} {n : Type u_5} {R : Type u_8} [t2_space R] :

### Lemmas about continuity of operations #

@[protected, instance]
def matrix.has_continuous_const_smul {α : Type u_2} {m : Type u_4} {n : Type u_5} {R : Type u_8} [ R]  :
(matrix m n R)
@[protected, instance]
def matrix.has_continuous_smul {α : Type u_2} {m : Type u_4} {n : Type u_5} {R : Type u_8} [ R] [ R] :
(matrix m n R)
@[protected, instance]
def matrix.has_continuous_add {m : Type u_4} {n : Type u_5} {R : Type u_8} [has_add R]  :
@[protected, instance]
def matrix.has_continuous_neg {m : Type u_4} {n : Type u_5} {R : Type u_8} [has_neg R]  :
@[protected, instance]
def matrix.topological_add_group {m : Type u_4} {n : Type u_5} {R : Type u_8} [add_group R]  :
@[continuity]
theorem continuous_matrix {α : Type u_2} {m : Type u_4} {n : Type u_5} {R : Type u_8} {f : α n R} (h : (i : m) (j : n), continuous (λ (a : α), f a i j)) :

To show a function into matrices is continuous it suffices to show the coefficients of the resulting matrix are continuous

theorem continuous.matrix_elem {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} {A : X n R} (hA : continuous A) (i : m) (j : n) :
continuous (λ (x : X), A x i j)
@[continuity]
theorem continuous.matrix_map {X : Type u_1} {m : Type u_4} {n : Type u_5} {S : Type u_7} {R : Type u_8} {A : X n S} {f : S R} (hA : continuous A) (hf : continuous f) :
continuous (λ (x : X), (A x).map f)
@[continuity]
theorem continuous.matrix_transpose {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} {A : X n R} (hA : continuous A) :
continuous (λ (x : X), (A x).transpose)
theorem continuous.matrix_conj_transpose {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [has_star R] {A : X n R} (hA : continuous A) :
continuous (λ (x : X), (A x).conj_transpose)
@[protected, instance]
def matrix.has_continuous_star {m : Type u_4} {R : Type u_8} [has_star R]  :
@[continuity]
theorem continuous.matrix_col {X : Type u_1} {n : Type u_5} {R : Type u_8} {A : X n R} (hA : continuous A) :
continuous (λ (x : X), matrix.col (A x))
@[continuity]
theorem continuous.matrix_row {X : Type u_1} {n : Type u_5} {R : Type u_8} {A : X n R} (hA : continuous A) :
continuous (λ (x : X), matrix.row (A x))
@[continuity]
theorem continuous.matrix_diagonal {X : Type u_1} {n : Type u_5} {R : Type u_8} [has_zero R] [decidable_eq n] {A : X n R} (hA : continuous A) :
continuous (λ (x : X), matrix.diagonal (A x))
@[continuity]
theorem continuous.matrix_dot_product {X : Type u_1} {n : Type u_5} {R : Type u_8} [fintype n] [has_mul R] {A B : X n R} (hA : continuous A) (hB : continuous B) :
continuous (λ (x : X), matrix.dot_product (A x) (B x))
@[continuity]
theorem continuous.matrix_mul {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [fintype n] [has_mul R] {A : X n R} {B : X p R} (hA : continuous A) (hB : continuous B) :
continuous (λ (x : X), (A x).mul (B x))

For square matrices the usual continuous_mul can be used.

@[protected, instance]
def matrix.has_continuous_mul {n : Type u_5} {R : Type u_8} [fintype n] [has_mul R]  :
@[protected, instance]
def matrix.topological_semiring {n : Type u_5} {R : Type u_8} [fintype n]  :
@[protected, instance]
def matrix.topological_ring {n : Type u_5} {R : Type u_8} [fintype n]  :
@[continuity]
theorem continuous.matrix_vec_mul_vec {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [has_mul R] {A : X m R} {B : X n R} (hA : continuous A) (hB : continuous B) :
continuous (λ (x : X), matrix.vec_mul_vec (A x) (B x))
@[continuity]
theorem continuous.matrix_mul_vec {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [fintype n] {A : X n R} {B : X n R} (hA : continuous A) (hB : continuous B) :
continuous (λ (x : X), (A x).mul_vec (B x))
@[continuity]
theorem continuous.matrix_vec_mul {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [fintype m] {A : X m R} {B : X n R} (hA : continuous A) (hB : continuous B) :
continuous (λ (x : X), matrix.vec_mul (A x) (B x))
@[continuity]
theorem continuous.matrix_submatrix {X : Type u_1} {l : Type u_3} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} {A : X n R} (hA : continuous A) (e₁ : m l) (e₂ : p n) :
continuous (λ (x : X), (A x).submatrix e₁ e₂)
@[continuity]
theorem continuous.matrix_reindex {X : Type u_1} {l : Type u_3} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} {A : X n R} (hA : continuous A) (e₁ : l m) (e₂ : n p) :
continuous (λ (x : X), e₂) (A x))
@[continuity]
theorem continuous.matrix_diag {X : Type u_1} {n : Type u_5} {R : Type u_8} {A : X n R} (hA : continuous A) :
continuous (λ (x : X), (A x).diag)
theorem continuous_matrix_diag {n : Type u_5} {R : Type u_8}  :
@[continuity]
theorem continuous.matrix_trace {X : Type u_1} {n : Type u_5} {R : Type u_8} [fintype n] {A : X n R} (hA : continuous A) :
continuous (λ (x : X), (A x).trace)
@[continuity]
theorem continuous.matrix_det {X : Type u_1} {n : Type u_5} {R : Type u_8} [fintype n] [decidable_eq n] [comm_ring R] {A : X n R} (hA : continuous A) :
continuous (λ (x : X), (A x).det)
@[continuity]
theorem continuous.matrix_update_column {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [decidable_eq n] (i : n) {A : X n R} {B : X m R} (hA : continuous A) (hB : continuous B) :
continuous (λ (x : X), (A x).update_column i (B x))
@[continuity]
theorem continuous.matrix_update_row {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [decidable_eq m] (i : m) {A : X n R} {B : X n R} (hA : continuous A) (hB : continuous B) :
continuous (λ (x : X), (A x).update_row i (B x))
@[continuity]
theorem continuous.matrix_cramer {X : Type u_1} {n : Type u_5} {R : Type u_8} [fintype n] [decidable_eq n] [comm_ring R] {A : X n R} {B : X n R} (hA : continuous A) (hB : continuous B) :
continuous (λ (x : X), ((A x).cramer) (B x))
@[continuity]
theorem continuous.matrix_adjugate {X : Type u_1} {n : Type u_5} {R : Type u_8} [fintype n] [decidable_eq n] [comm_ring R] {A : X n R} (hA : continuous A) :
continuous (λ (x : X), (A x).adjugate)
theorem continuous_at_matrix_inv {n : Type u_5} {R : Type u_8} [fintype n] [decidable_eq n] [comm_ring R] (A : n R) (h : A.det) :

When ring.inverse is continuous at the determinant (such as in a normed_ring, or a topological_field), so is matrix.has_inv.

@[continuity]
theorem continuous.matrix_from_blocks {X : Type u_1} {l : Type u_3} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} {A : X l R} {B : X m R} {C : X l R} {D : X m R} (hA : continuous A) (hB : continuous B) (hC : continuous C) (hD : continuous D) :
continuous (λ (x : X), matrix.from_blocks (A x) (B x) (C x) (D x))
@[continuity]
theorem continuous.matrix_block_diagonal {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [has_zero R] [decidable_eq p] {A : X p n R} (hA : continuous A) :
continuous (λ (x : X), matrix.block_diagonal (A x))
@[continuity]
theorem continuous.matrix_block_diag {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} {A : X matrix (m × p) (n × p) R} (hA : continuous A) :
continuous (λ (x : X), (A x).block_diag)
@[continuity]
theorem continuous.matrix_block_diagonal' {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l Type u_9} {n' : l Type u_10} [has_zero R] [decidable_eq l] {A : X Π (i : l), matrix (m' i) (n' i) R} (hA : continuous A) :
@[continuity]
theorem continuous.matrix_block_diag' {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l Type u_9} {n' : l Type u_10} {A : X matrix (Σ (i : l), m' i) (Σ (i : l), n' i) R} (hA : continuous A) :
continuous (λ (x : X), (A x).block_diag')

### Lemmas about infinite sums #

theorem has_sum.matrix_transpose {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} {f : X n R} {a : n R} (hf : a) :
has_sum (λ (x : X), (f x).transpose) a.transpose
theorem summable.matrix_transpose {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} {f : X n R} (hf : summable f) :
summable (λ (x : X), (f x).transpose)
@[simp]
theorem summable_matrix_transpose {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} {f : X n R} :
summable (λ (x : X), (f x).transpose)
theorem matrix.transpose_tsum {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [t2_space R] {f : X n R} :
(∑' (x : X), f x).transpose = ∑' (x : X), (f x).transpose
theorem has_sum.matrix_conj_transpose {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} {f : X n R} {a : n R} (hf : a) :
has_sum (λ (x : X), (f x).conj_transpose) a.conj_transpose
theorem summable.matrix_conj_transpose {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} {f : X n R} (hf : summable f) :
summable (λ (x : X), (f x).conj_transpose)
@[simp]
theorem summable_matrix_conj_transpose {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} {f : X n R} :
summable (λ (x : X), (f x).conj_transpose)
theorem matrix.conj_transpose_tsum {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [t2_space R] {f : X n R} :
(∑' (x : X), f x).conj_transpose = ∑' (x : X), (f x).conj_transpose
theorem has_sum.matrix_diagonal {X : Type u_1} {n : Type u_5} {R : Type u_8} [decidable_eq n] {f : X n R} {a : n R} (hf : a) :
has_sum (λ (x : X), matrix.diagonal (f x))
theorem summable.matrix_diagonal {X : Type u_1} {n : Type u_5} {R : Type u_8} [decidable_eq n] {f : X n R} (hf : summable f) :
summable (λ (x : X), matrix.diagonal (f x))
@[simp]
theorem summable_matrix_diagonal {X : Type u_1} {n : Type u_5} {R : Type u_8} [decidable_eq n] {f : X n R} :
summable (λ (x : X), matrix.diagonal (f x))
theorem matrix.diagonal_tsum {X : Type u_1} {n : Type u_5} {R : Type u_8} [decidable_eq n] [t2_space R] {f : X n R} :
matrix.diagonal (∑' (x : X), f x) = ∑' (x : X), matrix.diagonal (f x)
theorem has_sum.matrix_diag {X : Type u_1} {n : Type u_5} {R : Type u_8} {f : X n R} {a : n R} (hf : a) :
has_sum (λ (x : X), (f x).diag) a.diag
theorem summable.matrix_diag {X : Type u_1} {n : Type u_5} {R : Type u_8} {f : X n R} (hf : summable f) :
summable (λ (x : X), (f x).diag)
theorem has_sum.matrix_block_diagonal {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [decidable_eq p] {f : X p n R} {a : p n R} (hf : a) :
has_sum (λ (x : X), matrix.block_diagonal (f x))
theorem summable.matrix_block_diagonal {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [decidable_eq p] {f : X p n R} (hf : summable f) :
summable (λ (x : X), matrix.block_diagonal (f x))
theorem summable_matrix_block_diagonal {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [decidable_eq p] {f : X p n R} :
summable (λ (x : X), matrix.block_diagonal (f x))
theorem matrix.block_diagonal_tsum {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [decidable_eq p] [t2_space R] {f : X p n R} :
matrix.block_diagonal (∑' (x : X), f x) = ∑' (x : X),
theorem has_sum.matrix_block_diag {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} {f : X matrix (m × p) (n × p) R} {a : matrix (m × p) (n × p) R} (hf : a) :
has_sum (λ (x : X), (f x).block_diag) a.block_diag
theorem summable.matrix_block_diag {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} {f : X matrix (m × p) (n × p) R} (hf : summable f) :
summable (λ (x : X), (f x).block_diag)
theorem has_sum.matrix_block_diagonal' {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l Type u_9} {n' : l Type u_10} [decidable_eq l] {f : X Π (i : l), matrix (m' i) (n' i) R} {a : Π (i : l), matrix (m' i) (n' i) R} (hf : a) :
has_sum (λ (x : X), matrix.block_diagonal' (f x))
theorem summable.matrix_block_diagonal' {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l Type u_9} {n' : l Type u_10} [decidable_eq l] {f : X Π (i : l), matrix (m' i) (n' i) R} (hf : summable f) :
summable (λ (x : X), matrix.block_diagonal' (f x))
theorem summable_matrix_block_diagonal' {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l Type u_9} {n' : l Type u_10} [decidable_eq l] {f : X Π (i : l), matrix (m' i) (n' i) R} :
summable (λ (x : X), matrix.block_diagonal' (f x))
theorem matrix.block_diagonal'_tsum {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l Type u_9} {n' : l Type u_10} [decidable_eq l] [t2_space R] {f : X Π (i : l), matrix (m' i) (n' i) R} :
matrix.block_diagonal' (∑' (x : X), f x) = ∑' (x : X),
theorem has_sum.matrix_block_diag' {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l Type u_9} {n' : l Type u_10} {f : X matrix (Σ (i : l), m' i) (Σ (i : l), n' i) R} {a : matrix (Σ (i : l), m' i) (Σ (i : l), n' i) R} (hf : a) :
has_sum (λ (x : X), (f x).block_diag') a.block_diag'
theorem summable.matrix_block_diag' {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l Type u_9} {n' : l Type u_10} {f : X matrix (Σ (i : l), m' i) (Σ (i : l), n' i) R} (hf : summable f) :
summable (λ (x : X), (f x).block_diag')