Documentation

Mathlib.Topology.Instances.Matrix

Topological properties of matrices #

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

Main definitions: #

Main results #

source
๐Ÿ”ธ coverage
instance instTopologicalSpaceMatrix {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace R] :
TopologicalSpace (Matrix m n R)
Equations
    source
    ๐Ÿ“ coverage
    instance instT2SpaceMatrix {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [T2Space R] :
    T2Space (Matrix m n R)
    source
    ๐Ÿ“ coverage
    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.

    source
    ๐Ÿ“ coverage
    theorem IsOpen.matrix {m : Type u_4} {n : Type u_5} {R : Type u_8} [Finite m] [Finite n] [TopologicalSpace R] {S : Set R} (hS : IsOpen S) :
    IsOpen S.matrix
    source
    ๐Ÿ“ coverage
    theorem IsCompact.matrix {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace R] {S : Set R} (hS : IsCompact S) :
    IsCompact S.matrix

    Lemmas about continuity of operations #

    source
    ๐Ÿ“ coverage
    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)
    source
    ๐Ÿ“ coverage
    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)
    source
    ๐Ÿ“ coverage
    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)
    source
    ๐Ÿ“ coverage
    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)
    source
    ๐Ÿ“ coverage
    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)
    source
    ๐Ÿ“ coverage
    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

    source
    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
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    instance instContinuousStarMatrix {m : Type u_4} {R : Type u_8} [TopologicalSpace R] [Star R] [ContinuousStar R] :
    ContinuousStar (Matrix m m R)
    source
    ๐Ÿ“ coverage
    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)
    source
    ๐Ÿ“ coverage
    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)
    source
    ๐Ÿ“ coverage
    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)
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    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.

    source
    ๐Ÿ“ coverage
    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)
    source
    ๐Ÿ“ coverage
    instance instIsTopologicalSemiringMatrix {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [Fintype n] [NonUnitalNonAssocSemiring R] [IsTopologicalSemiring R] :
    IsTopologicalSemiring (Matrix n n R)
    source
    ๐Ÿ“ coverage
    instance Matrix.topologicalRing {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [Fintype n] [NonUnitalNonAssocRing R] [IsTopologicalRing R] :
    IsTopologicalRing (Matrix n n R)
    source
    ๐Ÿ“ coverage
    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)
    source
    ๐Ÿ“ coverage
    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)
    source
    ๐Ÿ“ coverage
    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)
    source
    ๐Ÿ“ coverage
    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โ‚‚
    source
    ๐Ÿ“ coverage
    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)
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    theorem continuous_matrix_diag {n : Type u_5} {R : Type u_8} [TopologicalSpace R] :
    Continuous Matrix.diag
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    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)
    source
    ๐Ÿ“ coverage
    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)
    source
    ๐Ÿ“ coverage
    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)
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    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) :
    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.

    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    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)
    source
    ๐Ÿ“ coverage
    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)
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    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)
    source
    ๐Ÿ“ coverage
    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 #

    source
    ๐Ÿ“ coverage
    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) :
    HasSum (fun (x : X) => (f x).transpose) a.transpose L
    source
    ๐Ÿ“ coverage
    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) :
    Summable (fun (x : X) => (f x).transpose) L
    source
    ๐Ÿ“ coverage
    @[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} :
    Summable (fun (x : X) => (f x).transpose) L โ†” Summable f L
    source
    ๐Ÿ“ coverage
    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} :
    (โˆ‘'[L] (x : X), f x).transpose = โˆ‘'[L] (x : X), (f x).transpose
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    @[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} :
    Summable (fun (x : X) => (f x).conjTranspose) L โ†” Summable f L
    source
    ๐Ÿ“ coverage
    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} :
    (โˆ‘'[L] (x : X), f x).conjTranspose = โˆ‘'[L] (x : X), (f x).conjTranspose
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    @[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} :
    Summable (fun (x : X) => Matrix.diagonal (f x)) L โ†” Summable f L
    source
    ๐Ÿ“ coverage
    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} :
    diagonal (โˆ‘'[L] (x : X), f x) = โˆ‘'[L] (x : X), diagonal (f x)
    source
    ๐Ÿ“ coverage
    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) :
    HasSum (fun (x : X) => (f x).diag) a.diag L
    source
    ๐Ÿ“ coverage
    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) :
    Summable (fun (x : X) => (f x).diag) L
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    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} :
    Summable (fun (x : X) => Matrix.blockDiagonal (f x)) L โ†” Summable f L
    source
    ๐Ÿ“ coverage
    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} :
    blockDiagonal (โˆ‘'[L] (x : X), f x) = โˆ‘'[L] (x : X), blockDiagonal (f x)
    source
    ๐Ÿ“ coverage
    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) :
    HasSum (fun (x : X) => (f x).blockDiag) a.blockDiag L
    source
    ๐Ÿ“ coverage
    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) :
    Summable (fun (x : X) => (f x).blockDiag) L
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    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} :
    Summable (fun (x : X) => Matrix.blockDiagonal' (f x)) L โ†” Summable f L
    source
    ๐Ÿ“ coverage
    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} :
    blockDiagonal' (โˆ‘'[L] (x : X), f x) = โˆ‘'[L] (x : X), blockDiagonal' (f x)
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    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 #

    source
    ๐Ÿ“ coverage
    theorem Matrix.GeneralLinearGroup.continuous_det {n : Type u_5} {R : Type u_8} [Fintype n] [DecidableEq n] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] :
    Continuous โ‡‘det

    The determinant is continuous as a map from the general linear group to the units.

    source
    ๐Ÿ“ coverage
    theorem Matrix.GeneralLinearGroup.continuous_upperRightHom {R : Type u_11} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] :
    Continuous โ‡‘upperRightHom
    source
    ๐Ÿ”ธ coverage
    instance Matrix.SpecialLinearGroup.instTopologicalSpace {n : Type u_5} {R : Type u_8} [Fintype n] [DecidableEq n] [CommRing R] [TopologicalSpace R] :
    TopologicalSpace (SpecialLinearGroup n R)
    Equations
      source
      ๐Ÿ“ coverage
      instance Matrix.SpecialLinearGroup.instDiscreteTopology {n : Type u_5} {R : Type u_8} [Fintype n] [DecidableEq n] [CommRing R] [TopologicalSpace R] [DiscreteTopology R] :
      DiscreteTopology (SpecialLinearGroup n R)

      If R is a commutative ring with the discrete topology, then SL(n, R) has the discrete topology.

      source
      ๐Ÿ“ coverage
      instance Matrix.SpecialLinearGroup.topologicalGroup {n : Type u_5} {R : Type u_8} [Fintype n] [DecidableEq n] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] :
      IsTopologicalGroup (SpecialLinearGroup n R)

      The special linear group over a topological ring is a topological group.

      source
      ๐Ÿ“ coverage
      theorem Matrix.SpecialLinearGroup.continuous_toGL {n : Type u_5} {R : Type u_8} [Fintype n] [DecidableEq n] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] :
      Continuous โ‡‘toGL

      The natural map from SL n A to GL n A is continuous.

      source
      ๐Ÿ“ coverage
      theorem Matrix.SpecialLinearGroup.isInducing_toGL {n : Type u_5} {R : Type u_8} [Fintype n] [DecidableEq n] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] :
      Topology.IsInducing โ‡‘toGL

      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.

      source
      ๐Ÿ“ coverage
      theorem Matrix.SpecialLinearGroup.isEmbedding_toGL {n : Type u_5} {R : Type u_8} [Fintype n] [DecidableEq n] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] :
      Topology.IsEmbedding โ‡‘toGL

      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.

      source
      ๐Ÿ“ coverage
      theorem Matrix.SpecialLinearGroup.range_toGL {n : Type u_5} [Fintype n] [DecidableEq n] {A : Type u_11} [CommRing A] :
      Set.range โ‡‘toGL = โ‡‘GeneralLinearGroup.det โปยน' {1}
      source
      ๐Ÿ“ coverage
      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] :
      Topology.IsClosedEmbedding โ‡‘toGL

      The natural inclusion of SL n A in GL n A is a closed embedding.

      source
      ๐Ÿ“ coverage
      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)
      source
      ๐Ÿ“ coverage
      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)) :
      Topology.IsEmbedding โ‡‘(mapGL B)