English
If f: A →ₛₗ[σ] B is a semilinear map, then applying f entrywise to m×n matrices yields a semilinear map on matrices; i.e., there is a map mapₗ(f): CStarMatrix m n A →ₛₗ[σ] CStarMatrix m n B preserving addition and scalar multiplication coordinatewise.
Русский
Если f : A →ₛₗ[σ] B — полулинейкое отображение, то применение f к каждому элементу матрицы размерности m×n задаёт полулинейкое отображение между CStarMatrix m n A и CStarMatrix m n B, сохраняющее сложение и умножение на скаляры по координатам.
LaTeX
$$$\text{map}_{\ell}(f): CStarMatrix_{m n}(A) \to_{\sigma} CStarMatrix_{m n}(B),\quad M \mapsto M.map f,\quad (M+N).map f = M.map f + N.map f,\quad (r\cdot M).map f = r\cdot (M.map f).$$$
Lean4
/-- The semilinear map constructed by applying a semilinear map to all the entries of the matrix. -/
@[simps]
def mapₗ [Semiring R] [Semiring S] {σ : R →+* S} [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module S B]
(f : A →ₛₗ[σ] B) : CStarMatrix m n A →ₛₗ[σ] CStarMatrix m n B
where
toFun := fun M => M.map f
map_add' M N := by ext; simp
map_smul' r M := by ext; simp
