Mₙ(R)-module structure on Mⁿ

Main Results

• Matrix.Module.matrixModule: This instance shows ι → M is a module over Matrix ι ι R, and the action of it is a generalization of Matrix.mulVec, this is only available in the Matrix.Module namespace.
• LinearMap.mapMatrixModule: This defines a linear map from ι → M to ι → N over Matrix ι ι R induced by a linear map from M to N and together with Matrix.matrixModule it gives a functor from the category of R-modules to the category of Matrix ι ι R-modules.

Tags

matrix, module

@[instance_reducible]

def Matrix.Module.matrixModule {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Ring R] [Fintype ι] [DecidableEq ι] [AddCommGroup M] [Module R M] : Module (Matrix ι ι R) (ι → M)

Mⁿ is a Mₙ(R) module, note that this creates a diamond when M is Matrix ι ι R or when M is R.

Equations

• One or more equations did not get rendered due to their size.

theorem Matrix.Module.smul_def {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Ring R] [Fintype ι] [DecidableEq ι] [AddCommGroup M] [Module R M] (N : Matrix ι ι R) (v : ι → M) : N • v = fun (i : ι) => ∑ j : ι, N i j • v j

theorem Matrix.Module.smul_def' {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Ring R] [Fintype ι] [DecidableEq ι] [AddCommGroup M] [Module R M] (N : Matrix ι ι R) (v : ι → M) : N • v = ∑ j : ι, fun (i : ι) => N i j • v j

@[simp]

theorem Matrix.Module.smul_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Ring R] [Fintype ι] [DecidableEq ι] [AddCommGroup M] [Module R M] (N : Matrix ι ι R) (v : ι → M) (i : ι) : (N • v) i = ∑ j : ι, N i j • v j

@[simp]

theorem Matrix.Module.single_smul {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Ring R] [Fintype ι] [DecidableEq ι] [AddCommGroup M] [Module R M] (i j : ι) (r : R) (v : ι → M) : single i j r • v = Pi.single i (r • v j)

@[simp]

theorem Matrix.Module.diagonal_const_smul {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Ring R] [Fintype ι] [DecidableEq ι] [AddCommGroup M] [Module R M] (r : R) (v : ι → M) : (diagonal fun (x : ι) => r) • v = r • v

theorem Matrix.Module.scalar_smul {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Ring R] [Fintype ι] [DecidableEq ι] [AddCommGroup M] [Module R M] (r : R) (v : ι → M) : (scalar ι) r • v = r • v

theorem Matrix.Module.instIsScalarTowerForall {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Ring R] [Fintype ι] [DecidableEq ι] [AddCommGroup M] [Module R M] (S : Type u_6) [Ring S] [SMul R S] [Module S M] [IsScalarTower R S M] : IsScalarTower R (Matrix ι ι S) (ι → M)

def LinearMap.mapMatrixModule (ι : Type u_1) {R : Type u_2} {M : Type u_3} {N : Type u_4} [Ring R] [Fintype ι] [DecidableEq ι] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) : (ι → M) →ₗ[Matrix ι ι R] ι → N

The induced linear map from Mⁿ to Nⁿ by a linear map f : M → N, this is the matrix linear version of LinearMap.compLeft.

Equations

• LinearMap.mapMatrixModule ι f = { toFun := ⇑(f.compLeft ι), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LinearMap.mapMatrixModule_apply (ι : Type u_1) {R : Type u_2} {M : Type u_3} {N : Type u_4} [Ring R] [Fintype ι] [DecidableEq ι] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (a : ι → M) (a✝ : ι) : (mapMatrixModule ι f) a a✝ = (f.compLeft ι) a a✝

@[simp]

theorem LinearMap.mapMatrixModule_id {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Ring R] [Fintype ι] [DecidableEq ι] [AddCommGroup M] [Module R M] : mapMatrixModule ι id = id

theorem LinearMap.mapMatrixModule_id_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Ring R] [Fintype ι] [DecidableEq ι] [AddCommGroup M] [Module R M] (v : ι → M) : (mapMatrixModule ι id) v = v

theorem LinearMap.mapMatrixModule_comp {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [Ring R] [Fintype ι] [DecidableEq ι] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup P] [Module R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) : mapMatrixModule ι (g ∘ₗ f) = mapMatrixModule ι g ∘ₗ mapMatrixModule ι f

@[simp]

theorem LinearMap.mapMatrixModule_comp_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [Ring R] [Fintype ι] [DecidableEq ι] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup P] [Module R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (v : ι → M) : (mapMatrixModule ι (g ∘ₗ f)) v = (mapMatrixModule ι g) ((mapMatrixModule ι f) v)