Continuous matrix actions and block maps over a topological module

A matrix A : Matrix κ ι R acts on vectors x : ι → M with entries in an R-module M by k ↦ ∑ i, A k i • x i. When M is a topological additive monoid on which each scalar acts continuously, this is the continuous additive map Matrix.smulVecHom A M : (ι → M) →ₜ+ (κ → M), and it is functorial in the matrix (Matrix.smulVecHom_one, Matrix.smulVecHom_mul). For M = R it is Matrix.mulVec (Matrix.smulVecHom_self_apply).

The motivating case is R = ℤ and M = AddCircle p, where an integer matrix induces a map of tori (ι → AddCircle p) → (κ → AddCircle p).

The upper-right block projection and the matching insertion are continuous linear maps over any semiring and topological module, with arbitrary row and column index types. Their application lemmas are Matrix.toBlocks₁₂CLM_apply and Matrix.fromBlocks₁₂CLM_apply.

Main definitions

• Matrix.smulVecHom: the continuous additive action of a matrix on module-valued vectors.
• Matrix.toBlocks₁₂CLM: projection onto the upper-right block as a continuous linear map.
• Matrix.fromBlocks₁₂CLM: insertion into the upper-right block as a continuous linear map.

def Matrix.smulVecHom {ι : Type u_1} {κ : Type u_2} {R : Type u_4} [Fintype ι] [Semiring R] (A : Matrix κ ι R) (M : Type u_5) [AddCommMonoid M] [Module R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousConstSMul R M] : (ι → M) →ₜ+ κ → M

The continuous additive map (ι → M) →ₜ+ (κ → M) induced by a matrix A with entries in R, sending x to k ↦ ∑ i, A k i • x i.

@[simp]

theorem Matrix.smulVecHom_apply {ι : Type u_1} {κ : Type u_2} {R : Type u_4} [Fintype ι] [Semiring R] (A : Matrix κ ι R) (M : Type u_5) [AddCommMonoid M] [Module R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousConstSMul R M] (x : ι → M) (k : κ) : (A.smulVecHom M) x k = ∑ i : ι, A k i • x i

@[simp]

theorem Matrix.smulVecHom_self_apply {ι : Type u_1} {κ : Type u_2} {R : Type u_4} [Fintype ι] [Semiring R] (A : Matrix κ ι R) [TopologicalSpace R] [ContinuousAdd R] [ContinuousConstSMul R R] (x : ι → R) : (A.smulVecHom R) x = A.mulVec x

For M = R, the induced map is Matrix.mulVec.

@[simp]

theorem Matrix.smulVecHom_one {ι : Type u_1} {R : Type u_4} [Fintype ι] [Semiring R] (M : Type u_5) [AddCommMonoid M] [Module R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousConstSMul R M] [DecidableEq ι] : smulVecHom 1 M = ContinuousAddMonoidHom.id (ι → M)

The identity matrix induces the identity map.

theorem Matrix.smulVecHom_mul {ι : Type u_1} {κ : Type u_2} {μ : Type u_3} {R : Type u_4} [Fintype ι] [Semiring R] (A : Matrix κ ι R) (M : Type u_5) [AddCommMonoid M] [Module R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousConstSMul R M] [Fintype κ] (B : Matrix μ κ R) : (B * A).smulVecHom M = (B.smulVecHom M).comp (A.smulVecHom M)

The map induced by a product of matrices is the composite of the maps they induce.

def Matrix.toBlocks₁₂CLM (𝕜 : Type u_6) {R : Type u_7} {m : Type u_8} {n : Type u_9} {l : Type u_10} {o : Type u_11} [Semiring 𝕜] [AddCommMonoid R] [Module 𝕜 R] [TopologicalSpace R] : Matrix (m ⊕ n) (l ⊕ o) R →L[𝕜] Matrix m o R

Projection onto the upper-right block as a continuous linear map.

@[simp]

theorem Matrix.toBlocks₁₂CLM_apply (𝕜 : Type u_6) {R : Type u_7} {m : Type u_8} {n : Type u_9} {l : Type u_10} {o : Type u_11} [Semiring 𝕜] [AddCommMonoid R] [Module 𝕜 R] [TopologicalSpace R] (A : Matrix (m ⊕ n) (l ⊕ o) R) : (toBlocks₁₂CLM 𝕜) A = A.toBlocks₁₂

The block projection acts by taking the upper-right block.

def Matrix.fromBlocks₁₂CLM (𝕜 : Type u_6) {R : Type u_7} {m : Type u_8} {n : Type u_9} {l : Type u_10} {o : Type u_11} [Semiring 𝕜] [AddCommMonoid R] [Module 𝕜 R] [TopologicalSpace R] : Matrix m o R →L[𝕜] Matrix (m ⊕ n) (l ⊕ o) R

Insertion into the upper-right block, with all other blocks zero, as a continuous linear map.

@[simp]

theorem Matrix.fromBlocks₁₂CLM_apply (𝕜 : Type u_6) {R : Type u_7} {m : Type u_8} {n : Type u_9} {l : Type u_10} {o : Type u_11} [Semiring 𝕜] [AddCommMonoid R] [Module 𝕜 R] [TopologicalSpace R] (A : Matrix m o R) : (fromBlocks₁₂CLM 𝕜) A = fromBlocks 0 A 0 0

The block insertion puts its argument in the upper-right block and zero elsewhere.