English
A linear map that maps internal submodules to internal submodules yields a block diagonal matrix with blocks given by the restricted maps, provided the action preserves the grading.
Русский
Линейное отображение, сохраняющее разбиение, даёт блочно-диагональную матрицу, составные блоки — ограничения отображения на каждую компоненту.
LaTeX
$$diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne …$$
Lean4
/-- If a linear map `f : M₁ → M₂` respects direct sum decompositions of `M₁` and `M₂`, then it has a
block diagonal matrix with respect to bases compatible with the direct sum decompositions. -/
theorem toMatrix_directSum_collectedBasis_eq_blockDiagonal' {R M₁ M₂ : Type*} [CommSemiring R] [AddCommMonoid M₁]
[Module R M₁] {N₁ : ι → Submodule R M₁} (h₁ : IsInternal N₁) [AddCommMonoid M₂] [Module R M₂]
{N₂ : ι → Submodule R M₂} (h₂ : IsInternal N₂) {κ₁ κ₂ : ι → Type*} [∀ i, Fintype (κ₁ i)] [∀ i, Finite (κ₂ i)]
[∀ i, DecidableEq (κ₁ i)] [Fintype ι] (b₁ : (i : ι) → Basis (κ₁ i) R (N₁ i)) (b₂ : (i : ι) → Basis (κ₂ i) R (N₂ i))
{f : M₁ →ₗ[R] M₂} (hf : ∀ i, MapsTo f (N₁ i) (N₂ i)) :
toMatrix (h₁.collectedBasis b₁) (h₂.collectedBasis b₂) f =
Matrix.blockDiagonal' fun i ↦ toMatrix (b₁ i) (b₂ i) (f.restrict (hf i)) :=
by
ext ⟨i, _⟩ ⟨j, _⟩
simp only [toMatrix_apply, Matrix.blockDiagonal'_apply]
rcases eq_or_ne i j with rfl | hij
· simp [h₂.collectedBasis_repr_of_mem _ (hf _ (Subtype.mem _)), restrict_apply]
· simp [hij, h₂.collectedBasis_repr_of_mem_ne _ hij.symm (hf _ (Subtype.mem _))]
