English
The construction toOneByOne is an explicit star-algebra equivalence between A and the 1×1 matrices over A, respecting multiplication, addition, and the star operation.
Русский
Конструкция toOneByOne является явной эквивалентностью звуковой алгебры между A и матрицей 1×1 над A, сохраняющей умножение, сложение и операцию звезды.
LaTeX
$$toOneByOne is a star-algebra equivalence between A and C^*Matrix_{1×1}(A).$$
Lean4
/-- Interpret a `CStarMatrix m n A` as a continuous linear map acting on `C⋆ᵐᵒᵈ (n → A)`. -/
noncomputable def toCLM : CStarMatrix m n A →ₗ[ℂ] C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)
where
toFun
M :=
{ toFun := (WithCStarModule.equivL ℂ).symm ∘ M.vecMul ∘ WithCStarModule.equivL ℂ
map_add' := M.add_vecMul
map_smul' := M.smul_vecMul
cont := Continuous.comp (by fun_prop) (by fun_prop) }
map_add' M₁
M₂ := by
ext
simp only [ContinuousLinearMap.coe_mk', LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply,
WithCStarModule.equivL_apply, WithCStarModule.equivL_symm_apply, WithCStarModule.equiv_symm_pi_apply,
ContinuousLinearMap.add_apply, WithCStarModule.add_apply]
rw [Matrix.vecMul_add, Pi.add_apply]
map_smul' c
M := by
ext x i
simp only [ContinuousLinearMap.coe_mk', LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply,
WithCStarModule.equivL_apply, WithCStarModule.equivL_symm_apply, WithCStarModule.equiv_symm_pi_apply,
ContinuousLinearMap.smul_apply, WithCStarModule.smul_apply, RingHom.id_apply]
rw [Matrix.vecMul_smul, Pi.smul_apply]
