matrixDecompositionLinearEquiv — Mathlib

English

The matrix decomposition yields an additive and linear equivalence between Hom spaces and block matrices over End(s(i)).

Русский

Разложение по матрице даёт аддитивное и линейное эквивалентство между косвенными пространствами и блочно-матрицами над End(s(i)).

LaTeX

$$$$ o.matrixDecompositionAddEquiv : (\\bigoplus s) \\to (\\bigoplus s) \\simeq_+ \\forall i, \\mathrm{End}(s(i)). $$$$

Lean4

/-- `HomOrthogonal.MatrixDecomposition` as an `R`-linear equivalence. -/
@[simps]
noncomputable def matrixDecompositionLinearEquiv (o : HomOrthogonal s) {α β : Type} [Finite α] [Finite β] {f : α → ι}
    {g : β → ι} :
    ((⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)) ≃ₗ[R] ∀ i : ι, Matrix (g ⁻¹' { i }) (f ⁻¹' { i }) (End (s i)) :=
  { o.matrixDecompositionAddEquiv with
    map_smul' := fun w z => by
      ext
      dsimp [biproduct.components]
      simp }

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