mapₗ_reindexₐ — Mathlib

English

Given a linear map φ: A →ₗ[R] B, reindexₐ commutes with mapₗ, i.e., reindexₐ(φ) ∘ mapₗ = mapₗ ∘ reindexₐ(φ).

Русский

Для линейного отображения φ: A →ₗ[R] B, переиндексация сохраняет линейное отображение: reindexₐ ∘ mapₗ = mapₗ ∘ reindexₐ.

LaTeX

$$$\mathrm{reindex}_{\mathsf{a}}(R,B,e)\,M \circ \mathrm{map}_{\ell}\;\phi = \mathrm{map}_{\ell}\;\phi \circ \mathrm{reindex}_{\mathsf{a}}(R,A,e).$$$

Lean4

theorem mapₗ_reindexₐ [Fintype m] [Fintype n] [Semiring R] [AddCommMonoid A] [Mul A] [Module R A] [Star A]
    [AddCommMonoid B] [Mul B] [Module R B] [Star B] {e : m ≃ n} {M : CStarMatrix m m A} (φ : A →ₗ[R] B) :
    reindexₐ R B e (M.mapₗ φ) = ((reindexₐ R A e M).mapₗ φ) := by ext; simp [reindexₐ, reindexₗ]

Похожие утверждения