Topological properties of matrices

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

Main definitions:

• Matrix.topologicalRing: 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.blockDiagonal_tsum: block diagonal commutes with infinite sums
  • Matrix.blockDiagonal'_tsum: non-uniform block diagonal commutes with infinite sums

instance instTopologicalSpaceMatrix {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace R] : TopologicalSpace (Matrix m n R)

Equations

• instTopologicalSpaceMatrix = Pi.topologicalSpace

instance instT2SpaceMatrix {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [T2Space R] : T2Space (Matrix m n R)

Equations

• ⋯ = ⋯

Lemmas about continuity of operations

instance instContinuousConstSMulMatrix {α : Type u_2} {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [SMul α R] [ContinuousConstSMul α R] : ContinuousConstSMul α (Matrix m n R)

Equations

• ⋯ = ⋯

instance instContinuousSMulMatrix {α : Type u_2} {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [TopologicalSpace α] [SMul α R] [ContinuousSMul α R] : ContinuousSMul α (Matrix m n R)

Equations

• ⋯ = ⋯

instance instContinuousAddMatrix {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [Add R] [ContinuousAdd R] : ContinuousAdd (Matrix m n R)

Equations

• ⋯ = ⋯

instance instContinuousNegMatrix {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [Neg R] [ContinuousNeg R] : ContinuousNeg (Matrix m n R)

Equations

• ⋯ = ⋯

instance instTopologicalAddGroupMatrix {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [AddGroup R] [TopologicalAddGroup R] : TopologicalAddGroup (Matrix m n R)

Equations

• ⋯ = ⋯

theorem continuous_matrix {α : Type u_2} {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [TopologicalSpace α] {f : α → Matrix m n R} (h : ∀ (i : m) (j : n), Continuous fun (a : α) => f a i j) : Continuous f

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} [TopologicalSpace X] [TopologicalSpace R] {A : X → Matrix m n R} (hA : Continuous A) (i : m) (j : n) : Continuous fun (x : X) => A x i j

theorem Continuous.matrix_map {X : Type u_1} {m : Type u_4} {n : Type u_5} {S : Type u_7} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [TopologicalSpace S] {A : X → Matrix m n S} {f : S → R} (hA : Continuous A) (hf : Continuous f) : Continuous fun (x : X) => (A x).map f

theorem Continuous.matrix_transpose {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] {A : X → Matrix m n R} (hA : Continuous A) : Continuous fun (x : X) => (A x).transpose

theorem Continuous.matrix_conjTranspose {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [Star R] [ContinuousStar R] {A : X → Matrix m n R} (hA : Continuous A) : Continuous fun (x : X) => (A x).conjTranspose

instance instContinuousStarMatrix {m : Type u_4} {R : Type u_8} [TopologicalSpace R] [Star R] [ContinuousStar R] : ContinuousStar (Matrix m m R)

Equations

• ⋯ = ⋯

theorem Continuous.matrix_col {X : Type u_1} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] {ι : Type u_11} {A : X → n → R} (hA : Continuous A) : Continuous fun (x : X) => Matrix.col ι (A x)

theorem Continuous.matrix_row {X : Type u_1} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] {ι : Type u_11} {A : X → n → R} (hA : Continuous A) : Continuous fun (x : X) => Matrix.row ι (A x)

theorem Continuous.matrix_diagonal {X : Type u_1} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [Zero R] [DecidableEq n] {A : X → n → R} (hA : Continuous A) : Continuous fun (x : X) => Matrix.diagonal (A x)

theorem Continuous.matrix_dotProduct {X : Type u_1} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [Fintype n] [Mul R] [AddCommMonoid R] [ContinuousAdd R] [ContinuousMul R] {A B : X → n → R} (hA : Continuous A) (hB : Continuous B) : Continuous fun (x : X) => Matrix.dotProduct (A x) (B x)

theorem Continuous.matrix_mul {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [Fintype n] [Mul R] [AddCommMonoid R] [ContinuousAdd R] [ContinuousMul R] {A : X → Matrix m n R} {B : X → Matrix n p R} (hA : Continuous A) (hB : Continuous B) : Continuous fun (x : X) => A x * B x

For square matrices the usual continuous_mul can be used.

instance instContinuousMulMatrixOfContinuousAdd {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [Fintype n] [Mul R] [AddCommMonoid R] [ContinuousAdd R] [ContinuousMul R] : ContinuousMul (Matrix n n R)

Equations

• ⋯ = ⋯

instance instTopologicalSemiringMatrix {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [Fintype n] [NonUnitalNonAssocSemiring R] [TopologicalSemiring R] : TopologicalSemiring (Matrix n n R)

Equations

• ⋯ = ⋯

instance Matrix.topologicalRing {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [Fintype n] [NonUnitalNonAssocRing R] [TopologicalRing R] : TopologicalRing (Matrix n n R)

Equations

• ⋯ = ⋯

theorem Continuous.matrix_vecMulVec {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [Mul R] [ContinuousMul R] {A : X → m → R} {B : X → n → R} (hA : Continuous A) (hB : Continuous B) : Continuous fun (x : X) => Matrix.vecMulVec (A x) (B x)

theorem Continuous.matrix_mulVec {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [NonUnitalNonAssocSemiring R] [ContinuousAdd R] [ContinuousMul R] [Fintype n] {A : X → Matrix m n R} {B : X → n → R} (hA : Continuous A) (hB : Continuous B) : Continuous fun (x : X) => (A x).mulVec (B x)

theorem Continuous.matrix_vecMul {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [NonUnitalNonAssocSemiring R] [ContinuousAdd R] [ContinuousMul R] [Fintype m] {A : X → m → R} {B : X → Matrix m n R} (hA : Continuous A) (hB : Continuous B) : Continuous fun (x : X) => Matrix.vecMul (A x) (B x)

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} [TopologicalSpace X] [TopologicalSpace R] {A : X → Matrix l n R} (hA : Continuous A) (e₁ : m → l) (e₂ : p → n) : Continuous fun (x : X) => (A x).submatrix e₁ e₂

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} [TopologicalSpace X] [TopologicalSpace R] {A : X → Matrix l n R} (hA : Continuous A) (e₁ : l ≃ m) (e₂ : n ≃ p) : Continuous fun (x : X) => (Matrix.reindex e₁ e₂) (A x)

theorem Continuous.matrix_diag {X : Type u_1} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] {A : X → Matrix n n R} (hA : Continuous A) : Continuous fun (x : X) => (A x).diag

theorem continuous_matrix_diag {n : Type u_5} {R : Type u_8} [TopologicalSpace R] : Continuous Matrix.diag

theorem Continuous.matrix_trace {X : Type u_1} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [Fintype n] [AddCommMonoid R] [ContinuousAdd R] {A : X → Matrix n n R} (hA : Continuous A) : Continuous fun (x : X) => (A x).trace

theorem Continuous.matrix_det {X : Type u_1} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [Fintype n] [DecidableEq n] [CommRing R] [TopologicalRing R] {A : X → Matrix n n R} (hA : Continuous A) : Continuous fun (x : X) => (A x).det

theorem Continuous.matrix_updateColumn {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [DecidableEq n] (i : n) {A : X → Matrix m n R} {B : X → m → R} (hA : Continuous A) (hB : Continuous B) : Continuous fun (x : X) => (A x).updateColumn i (B x)

theorem Continuous.matrix_updateRow {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [DecidableEq m] (i : m) {A : X → Matrix m n R} {B : X → n → R} (hA : Continuous A) (hB : Continuous B) : Continuous fun (x : X) => (A x).updateRow i (B x)

theorem Continuous.matrix_cramer {X : Type u_1} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [Fintype n] [DecidableEq n] [CommRing R] [TopologicalRing R] {A : X → Matrix n n R} {B : X → n → R} (hA : Continuous A) (hB : Continuous B) : Continuous fun (x : X) => (A x).cramer (B x)

theorem Continuous.matrix_adjugate {X : Type u_1} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [Fintype n] [DecidableEq n] [CommRing R] [TopologicalRing R] {A : X → Matrix n n R} (hA : Continuous A) : Continuous fun (x : X) => (A x).adjugate

theorem continuousAt_matrix_inv {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [Fintype n] [DecidableEq n] [CommRing R] [TopologicalRing R] (A : Matrix n n R) (h : ContinuousAt Ring.inverse A.det) : ContinuousAt Inv.inv A

When Ring.inverse is continuous at the determinant (such as in a NormedRing, or a topological field), so is Matrix.inv.

theorem Continuous.matrix_fromBlocks {X : Type u_1} {l : Type u_3} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] {A : X → Matrix n l R} {B : X → Matrix n m R} {C : X → Matrix p l R} {D : X → Matrix p m R} (hA : Continuous A) (hB : Continuous B) (hC : Continuous C) (hD : Continuous D) : Continuous fun (x : X) => Matrix.fromBlocks (A x) (B x) (C x) (D x)

theorem Continuous.matrix_blockDiagonal {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [Zero R] [DecidableEq p] {A : X → p → Matrix m n R} (hA : Continuous A) : Continuous fun (x : X) => Matrix.blockDiagonal (A x)

theorem Continuous.matrix_blockDiag {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] {A : X → Matrix (m × p) (n × p) R} (hA : Continuous A) : Continuous fun (x : X) => (A x).blockDiag

theorem Continuous.matrix_blockDiagonal' {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l → Type u_9} {n' : l → Type u_10} [TopologicalSpace X] [TopologicalSpace R] [Zero R] [DecidableEq l] {A : X → (i : l) → Matrix (m' i) (n' i) R} (hA : Continuous A) : Continuous fun (x : X) => Matrix.blockDiagonal' (A x)

theorem Continuous.matrix_blockDiag' {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l → Type u_9} {n' : l → Type u_10} [TopologicalSpace X] [TopologicalSpace R] {A : X → Matrix ((i : l) × m' i) ((i : l) × n' i) R} (hA : Continuous A) : Continuous fun (x : X) => (A x).blockDiag'

Lemmas about infinite sums

theorem HasSum.matrix_transpose {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] {f : X → Matrix m n R} {a : Matrix m n R} (hf : HasSum f a) : HasSum (fun (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} [AddCommMonoid R] [TopologicalSpace R] {f : X → Matrix m n R} (hf : Summable f) : Summable fun (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} [AddCommMonoid R] [TopologicalSpace R] {f : X → Matrix m n R} : (Summable fun (x : X) => (f x).transpose) ↔ Summable f

theorem Matrix.transpose_tsum {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] [T2Space R] {f : X → Matrix m n R} : (∑' (x : X), f x).transpose = ∑' (x : X), (f x).transpose

theorem HasSum.matrix_conjTranspose {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] [StarAddMonoid R] [ContinuousStar R] {f : X → Matrix m n R} {a : Matrix m n R} (hf : HasSum f a) : HasSum (fun (x : X) => (f x).conjTranspose) a.conjTranspose

theorem Summable.matrix_conjTranspose {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] [StarAddMonoid R] [ContinuousStar R] {f : X → Matrix m n R} (hf : Summable f) : Summable fun (x : X) => (f x).conjTranspose

@[simp]

theorem summable_matrix_conjTranspose {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] [StarAddMonoid R] [ContinuousStar R] {f : X → Matrix m n R} : (Summable fun (x : X) => (f x).conjTranspose) ↔ Summable f

theorem Matrix.conjTranspose_tsum {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] [StarAddMonoid R] [ContinuousStar R] [T2Space R] {f : X → Matrix m n R} : (∑' (x : X), f x).conjTranspose = ∑' (x : X), (f x).conjTranspose

theorem HasSum.matrix_diagonal {X : Type u_1} {n : Type u_5} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] [DecidableEq n] {f : X → n → R} {a : n → R} (hf : HasSum f a) : HasSum (fun (x : X) => Matrix.diagonal (f x)) (Matrix.diagonal a)

theorem Summable.matrix_diagonal {X : Type u_1} {n : Type u_5} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] [DecidableEq n] {f : X → n → R} (hf : Summable f) : Summable fun (x : X) => Matrix.diagonal (f x)

@[simp]

theorem summable_matrix_diagonal {X : Type u_1} {n : Type u_5} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] [DecidableEq n] {f : X → n → R} : (Summable fun (x : X) => Matrix.diagonal (f x)) ↔ Summable f

theorem Matrix.diagonal_tsum {X : Type u_1} {n : Type u_5} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] [DecidableEq n] [T2Space R] {f : X → n → R} : Matrix.diagonal (∑' (x : X), f x) = ∑' (x : X), Matrix.diagonal (f x)

theorem HasSum.matrix_diag {X : Type u_1} {n : Type u_5} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] {f : X → Matrix n n R} {a : Matrix n n R} (hf : HasSum f a) : HasSum (fun (x : X) => (f x).diag) a.diag

theorem Summable.matrix_diag {X : Type u_1} {n : Type u_5} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] {f : X → Matrix n n R} (hf : Summable f) : Summable fun (x : X) => (f x).diag

theorem HasSum.matrix_blockDiagonal {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] [DecidableEq p] {f : X → p → Matrix m n R} {a : p → Matrix m n R} (hf : HasSum f a) : HasSum (fun (x : X) => Matrix.blockDiagonal (f x)) (Matrix.blockDiagonal a)

theorem Summable.matrix_blockDiagonal {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] [DecidableEq p] {f : X → p → Matrix m n R} (hf : Summable f) : Summable fun (x : X) => Matrix.blockDiagonal (f x)

theorem summable_matrix_blockDiagonal {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] [DecidableEq p] {f : X → p → Matrix m n R} : (Summable fun (x : X) => Matrix.blockDiagonal (f x)) ↔ Summable f

theorem Matrix.blockDiagonal_tsum {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] [DecidableEq p] [T2Space R] {f : X → p → Matrix m n R} : Matrix.blockDiagonal (∑' (x : X), f x) = ∑' (x : X), Matrix.blockDiagonal (f x)

theorem HasSum.matrix_blockDiag {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] {f : X → Matrix (m × p) (n × p) R} {a : Matrix (m × p) (n × p) R} (hf : HasSum f a) : HasSum (fun (x : X) => (f x).blockDiag) a.blockDiag

theorem Summable.matrix_blockDiag {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] {f : X → Matrix (m × p) (n × p) R} (hf : Summable f) : Summable fun (x : X) => (f x).blockDiag

theorem HasSum.matrix_blockDiagonal' {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l → Type u_9} {n' : l → Type u_10} [AddCommMonoid R] [TopologicalSpace R] [DecidableEq l] {f : X → (i : l) → Matrix (m' i) (n' i) R} {a : (i : l) → Matrix (m' i) (n' i) R} (hf : HasSum f a) : HasSum (fun (x : X) => Matrix.blockDiagonal' (f x)) (Matrix.blockDiagonal' a)

theorem Summable.matrix_blockDiagonal' {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l → Type u_9} {n' : l → Type u_10} [AddCommMonoid R] [TopologicalSpace R] [DecidableEq l] {f : X → (i : l) → Matrix (m' i) (n' i) R} (hf : Summable f) : Summable fun (x : X) => Matrix.blockDiagonal' (f x)

theorem summable_matrix_blockDiagonal' {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l → Type u_9} {n' : l → Type u_10} [AddCommMonoid R] [TopologicalSpace R] [DecidableEq l] {f : X → (i : l) → Matrix (m' i) (n' i) R} : (Summable fun (x : X) => Matrix.blockDiagonal' (f x)) ↔ Summable f

theorem Matrix.blockDiagonal'_tsum {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l → Type u_9} {n' : l → Type u_10} [AddCommMonoid R] [TopologicalSpace R] [DecidableEq l] [T2Space R] {f : X → (i : l) → Matrix (m' i) (n' i) R} : Matrix.blockDiagonal' (∑' (x : X), f x) = ∑' (x : X), Matrix.blockDiagonal' (f x)

theorem HasSum.matrix_blockDiag' {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l → Type u_9} {n' : l → Type u_10} [AddCommMonoid R] [TopologicalSpace R] {f : X → Matrix ((i : l) × m' i) ((i : l) × n' i) R} {a : Matrix ((i : l) × m' i) ((i : l) × n' i) R} (hf : HasSum f a) : HasSum (fun (x : X) => (f x).blockDiag') a.blockDiag'

theorem Summable.matrix_blockDiag' {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l → Type u_9} {n' : l → Type u_10} [AddCommMonoid R] [TopologicalSpace R] {f : X → Matrix ((i : l) × m' i) ((i : l) × n' i) R} (hf : Summable f) : Summable fun (x : X) => (f x).blockDiag'