English
For a linear map φ: A → B, the entrywise map on matrices M ↦ M.mapₗ φ is a map of CStarMatrix, intertwining with StarAlgEquiv and reindex operations.
Русский
Для линейного отображения φ: A → B отображение по элементам на матрицах M ↦ M.mapₗ φ образует отображение CStarMatrix и согласуется с операциями звуковых эквивалентностей и переиндексации.
LaTeX
$$$\mathrm{reindex}_{\mathsf{a}}(R,B,e) \circ \mathrm{map}_{\ell} \;\phi = \mathrm{map}_{\ell} \circ \mathrm{StarAlgEquiv}.instFunLike_1(\mathrm{reindex}_{\mathsf{a}}(R,A,e))$$$
Lean4
/-- Applying a non-unital ⋆-algebra homomorphism to every entry of a matrix is itself a
⋆-algebra homomorphism on matrices. -/
@[simps]
def mapₙₐ [Fintype n] [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B]
[Module R B] [Star B] (f : A →⋆ₙₐ[R] B) : CStarMatrix n n A →⋆ₙₐ[R] CStarMatrix n n B
where
toFun := fun M => M.mapₗ (f : A →ₗ[R] B)
map_smul' := by simp
map_zero' := by simp [map_zero]
map_add' := by simp [map_add]
map_mul' M
N :=
by
ext
-- Un-squeezing this `simp` seems to add about half a second elaboration time.
simp only [mapₗ_apply, map, LinearMap.coe_coe, ofMatrix_apply, mul_apply, map_sum, map_mul, ofMatrix_apply]
map_star' M := by ext; simp [map, star_apply, map_star]
