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 #
- Sets of matrices:
IsOpen.matrix: the set of finite matrices with entries in an open set is itself an open set.IsCompact.matrix: the set of matrices with entries in a compact set is itself a compact set.
- 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 sumsMatrix.diagonal_tsum: diagonal commutes with infinite sumsMatrix.blockDiagonal_tsum: block diagonal commutes with infinite sumsMatrix.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)
instance
instT2SpaceMatrix
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[TopologicalSpace R]
[T2Space R]
:
instance
instDiscreteTopologyMatrixOfFinite
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[TopologicalSpace R]
[Finite m]
[Finite n]
[DiscreteTopology R]
:
DiscreteTopology (Matrix m n R)
The topology on finite matrices over a discrete space is discrete.
theorem
IsCompact.matrix
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[TopologicalSpace R]
{S : Set R}
(hS : IsCompact S)
:
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)
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)
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)
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)
instance
instIsTopologicalAddGroupMatrix
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[TopologicalSpace R]
[AddGroup R]
[IsTopologicalAddGroup R]
:
IsTopologicalAddGroup (Matrix m n R)
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)
:
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)
theorem
Continuous.matrix_replicateCol
{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.replicateCol ι (A x)
@[deprecated Continuous.matrix_replicateCol (since := "2025-03-15")]
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.replicateCol ι (A x)
Alias of Continuous.matrix_replicateCol.
theorem
Continuous.matrix_replicateRow
{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.replicateRow ι (A x)
@[deprecated Continuous.matrix_replicateRow (since := "2025-03-15")]
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.replicateRow ι (A x)
Alias of Continuous.matrix_replicateRow.
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.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) => A x ⬝ᵥ B x
@[deprecated Continuous.dotProduct (since := "2025-05-09")]
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) => A x ⬝ᵥ B x
Alias of Continuous.dotProduct.
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)
instance
instIsTopologicalSemiringMatrix
{n : Type u_5}
{R : Type u_8}
[TopologicalSpace R]
[Fintype n]
[NonUnitalNonAssocSemiring R]
[IsTopologicalSemiring R]
:
IsTopologicalSemiring (Matrix n n R)
instance
Matrix.topologicalRing
{n : Type u_5}
{R : Type u_8}
[TopologicalSpace R]
[Fintype n]
[NonUnitalNonAssocRing R]
[IsTopologicalRing R]
:
IsTopologicalRing (Matrix n n R)
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_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]
[IsTopologicalRing R]
{A : X → Matrix n n R}
(hA : Continuous A)
:
Continuous fun (x : X) => (A x).det
theorem
Continuous.matrix_updateCol
{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).updateCol 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]
[IsTopologicalRing 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]
[IsTopologicalRing 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]
[IsTopologicalRing R]
(A : Matrix n n R)
(h : ContinuousAt Ring.inverse A.det)
:
When Ring.inverse is continuous at the determinant (such as in a NormedRing, or a
topological field), so is Matrix.inv.
theorem
Topology.IsInducing.matrix_map
{m : Type u_11}
{n : Type u_12}
{R : Type u_13}
{S : Type u_14}
[TopologicalSpace R]
[TopologicalSpace S]
{f : R → S}
(hf : IsInducing f)
:
IsInducing fun (x : Matrix m n R) => x.map f
theorem
Topology.IsEmbedding.matrix_map
{m : Type u_11}
{n : Type u_12}
{R : Type u_13}
{S : Type u_14}
[TopologicalSpace R]
[TopologicalSpace S]
{f : R → S}
(hf : IsEmbedding f)
:
IsEmbedding fun (x : Matrix m n R) => x.map f
theorem
Topology.IsClosedEmbedding.matrix_map
{m : Type u_11}
{n : Type u_12}
{R : Type u_13}
{S : Type u_14}
[TopologicalSpace R]
[TopologicalSpace S]
{f : R → S}
(hf : IsClosedEmbedding f)
:
IsClosedEmbedding fun (x : Matrix m n R) => x.map f
theorem
Topology.IsOpenEmbedding.matrix_map
{m : Type u_11}
{n : Type u_12}
{R : Type u_13}
{S : Type u_14}
[TopologicalSpace R]
[TopologicalSpace S]
{f : R → S}
[Finite m]
[Finite n]
(hf : IsOpenEmbedding f)
:
IsOpenEmbedding fun (x : Matrix m n R) => x.map f
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]
{L : SummationFilter X}
{f : X → Matrix m n R}
{a : Matrix m n R}
(hf : HasSum f a L)
:
theorem
Summable.matrix_transpose
{X : Type u_1}
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[AddCommMonoid R]
[TopologicalSpace R]
{L : SummationFilter X}
{f : X → Matrix m n R}
(hf : Summable f L)
:
@[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]
{L : SummationFilter X}
{f : X → Matrix m n R}
:
theorem
Matrix.transpose_tsum
{X : Type u_1}
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[AddCommMonoid R]
[TopologicalSpace R]
{L : SummationFilter X}
[T2Space R]
{f : X → Matrix m n R}
:
theorem
HasSum.matrix_conjTranspose
{X : Type u_1}
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[AddCommMonoid R]
[TopologicalSpace R]
{L : SummationFilter X}
[StarAddMonoid R]
[ContinuousStar R]
{f : X → Matrix m n R}
{a : Matrix m n R}
(hf : HasSum f a L)
:
HasSum (fun (x : X) => (f x).conjTranspose) a.conjTranspose L
theorem
Summable.matrix_conjTranspose
{X : Type u_1}
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[AddCommMonoid R]
[TopologicalSpace R]
{L : SummationFilter X}
[StarAddMonoid R]
[ContinuousStar R]
{f : X → Matrix m n R}
(hf : Summable f L)
:
Summable (fun (x : X) => (f x).conjTranspose) L
@[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]
{L : SummationFilter X}
[StarAddMonoid R]
[ContinuousStar R]
{f : X → Matrix m n R}
:
theorem
Matrix.conjTranspose_tsum
{X : Type u_1}
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[AddCommMonoid R]
[TopologicalSpace R]
{L : SummationFilter X}
[StarAddMonoid R]
[ContinuousStar R]
[T2Space R]
{f : X → Matrix m n R}
:
theorem
HasSum.matrix_diagonal
{X : Type u_1}
{n : Type u_5}
{R : Type u_8}
[AddCommMonoid R]
[TopologicalSpace R]
{L : SummationFilter X}
[DecidableEq n]
{f : X → n → R}
{a : n → R}
(hf : HasSum f a L)
:
HasSum (fun (x : X) => Matrix.diagonal (f x)) (Matrix.diagonal a) L
theorem
Summable.matrix_diagonal
{X : Type u_1}
{n : Type u_5}
{R : Type u_8}
[AddCommMonoid R]
[TopologicalSpace R]
{L : SummationFilter X}
[DecidableEq n]
{f : X → n → R}
(hf : Summable f L)
:
Summable (fun (x : X) => Matrix.diagonal (f x)) L
@[simp]
theorem
summable_matrix_diagonal
{X : Type u_1}
{n : Type u_5}
{R : Type u_8}
[AddCommMonoid R]
[TopologicalSpace R]
{L : SummationFilter X}
[DecidableEq n]
{f : X → n → R}
:
theorem
Matrix.diagonal_tsum
{X : Type u_1}
{n : Type u_5}
{R : Type u_8}
[AddCommMonoid R]
[TopologicalSpace R]
{L : SummationFilter X}
[DecidableEq n]
[T2Space R]
{f : X → n → R}
:
theorem
HasSum.matrix_diag
{X : Type u_1}
{n : Type u_5}
{R : Type u_8}
[AddCommMonoid R]
[TopologicalSpace R]
{L : SummationFilter X}
{f : X → Matrix n n R}
{a : Matrix n n R}
(hf : HasSum f a L)
:
theorem
Summable.matrix_diag
{X : Type u_1}
{n : Type u_5}
{R : Type u_8}
[AddCommMonoid R]
[TopologicalSpace R]
{L : SummationFilter X}
{f : X → Matrix n n R}
(hf : Summable f L)
:
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]
{L : SummationFilter X}
[DecidableEq p]
{f : X → p → Matrix m n R}
{a : p → Matrix m n R}
(hf : HasSum f a L)
:
HasSum (fun (x : X) => Matrix.blockDiagonal (f x)) (Matrix.blockDiagonal a) L
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]
{L : SummationFilter X}
[DecidableEq p]
{f : X → p → Matrix m n R}
(hf : Summable f L)
:
Summable (fun (x : X) => Matrix.blockDiagonal (f x)) L
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]
{L : SummationFilter X}
[DecidableEq p]
{f : X → p → Matrix m n R}
:
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]
{L : SummationFilter X}
[DecidableEq p]
[T2Space R]
{f : X → p → Matrix m n R}
:
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]
{L : SummationFilter X}
{f : X → Matrix (m × p) (n × p) R}
{a : Matrix (m × p) (n × p) R}
(hf : HasSum f a L)
:
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]
{L : SummationFilter X}
{f : X → Matrix (m × p) (n × p) R}
(hf : Summable f L)
:
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]
{L : SummationFilter X}
[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 L)
:
HasSum (fun (x : X) => Matrix.blockDiagonal' (f x)) (Matrix.blockDiagonal' a) L
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]
{L : SummationFilter X}
[DecidableEq l]
{f : X → (i : l) → Matrix (m' i) (n' i) R}
(hf : Summable f L)
:
Summable (fun (x : X) => Matrix.blockDiagonal' (f x)) L
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]
{L : SummationFilter X}
[DecidableEq l]
{f : X → (i : l) → Matrix (m' i) (n' i) R}
:
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]
{L : SummationFilter X}
[DecidableEq l]
[T2Space R]
{f : X → (i : l) → Matrix (m' i) (n' i) R}
:
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]
{L : SummationFilter X}
{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 L)
:
HasSum (fun (x : X) => (f x).blockDiag') a.blockDiag' L
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]
{L : SummationFilter X}
{f : X → Matrix ((i : l) × m' i) ((i : l) × n' i) R}
(hf : Summable f L)
:
Summable (fun (x : X) => (f x).blockDiag') L
Lemmas about matrix groups #
theorem
Matrix.GeneralLinearGroup.continuous_det
{n : Type u_5}
{R : Type u_8}
[Fintype n]
[DecidableEq n]
[CommRing R]
[TopologicalSpace R]
[IsTopologicalRing R]
:
The determinant is continuous as a map from the general linear group to the units.
instance
Matrix.SpecialLinearGroup.instTopologicalSpace
{n : Type u_5}
{R : Type u_8}
[Fintype n]
[DecidableEq n]
[CommRing R]
[TopologicalSpace R]
:
instance
Matrix.SpecialLinearGroup.instDiscreteTopology
{n : Type u_5}
{R : Type u_8}
[Fintype n]
[DecidableEq n]
[CommRing R]
[TopologicalSpace R]
[DiscreteTopology R]
:
If R is a commutative ring with the discrete topology, then SL(n, R) has the discrete
topology.
instance
Matrix.SpecialLinearGroup.topologicalGroup
{n : Type u_5}
{R : Type u_8}
[Fintype n]
[DecidableEq n]
[CommRing R]
[TopologicalSpace R]
[IsTopologicalRing R]
:
The special linear group over a topological ring is a topological group.
theorem
Matrix.SpecialLinearGroup.continuous_toGL
{n : Type u_5}
{R : Type u_8}
[Fintype n]
[DecidableEq n]
[CommRing R]
[TopologicalSpace R]
[IsTopologicalRing R]
:
The natural map from SL n A to GL n A is continuous.
theorem
Matrix.SpecialLinearGroup.isInducing_toGL
{n : Type u_5}
{R : Type u_8}
[Fintype n]
[DecidableEq n]
[CommRing R]
[TopologicalSpace R]
[IsTopologicalRing R]
:
The natural map from SL n A to GL n A is inducing, i.e. the topology on
SL n A is the pullback of the topology from GL n A.
theorem
Matrix.SpecialLinearGroup.isEmbedding_toGL
{n : Type u_5}
{R : Type u_8}
[Fintype n]
[DecidableEq n]
[CommRing R]
[TopologicalSpace R]
[IsTopologicalRing R]
:
The natural map from SL n A in GL n A is an embedding, i.e. it is an injection and
the topology on SL n A coincides with the subspace topology from GL n A.
theorem
Matrix.SpecialLinearGroup.range_toGL
{n : Type u_5}
[Fintype n]
[DecidableEq n]
{A : Type u_11}
[CommRing A]
:
theorem
Matrix.SpecialLinearGroup.isClosedEmbedding_toGL
{n : Type u_5}
{R : Type u_8}
[Fintype n]
[DecidableEq n]
[CommRing R]
[TopologicalSpace R]
[IsTopologicalRing R]
[T0Space R]
:
The natural inclusion of SL n A in GL n A is a closed embedding.
theorem
Matrix.SpecialLinearGroup.isInducing_mapGL
{n : Type u_11}
[Fintype n]
[DecidableEq n]
{A : Type u_12}
{B : Type u_13}
[CommRing A]
[CommRing B]
[Algebra A B]
[TopologicalSpace A]
[TopologicalSpace B]
[IsTopologicalRing B]
(h : Topology.IsInducing ⇑(algebraMap A B))
:
Topology.IsInducing ⇑(mapGL B)
theorem
Matrix.SpecialLinearGroup.isEmbedding_mapGL
{n : Type u_11}
[Fintype n]
[DecidableEq n]
{A : Type u_12}
{B : Type u_13}
[CommRing A]
[CommRing B]
[Algebra A B]
[TopologicalSpace A]
[TopologicalSpace B]
[IsTopologicalRing B]
(h : Topology.IsEmbedding ⇑(algebraMap A B))
: