matrixDecompositionAddEquiv — Mathlib

English

The matrix decomposition is additive, giving an additive equivalence between Hom and block-matrix space.

Русский

Разложение по матрице совместимо по сложению, образуя аддитивное эквивалентство между Hom и пространством блочно-матриц.

LaTeX

$$$$ o.matrixDecompositionAddEquiv : \\text{Hom}(\\oplus s, \\oplus s) \\simeq_+ \\forall i, \\mathrm{End}(s(i)). $$$$

Lean4

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

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