matrixDecomposition — Mathlib

English

Block-diagonal matrix decomposition expresses Hom between biproducts as a product of endomorphism matrices indexed by the objects s(i).

Русский

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

LaTeX

$$$$\\text{Hom}(\\bigoplus_i s(f(i)), \\bigoplus_j s(g(j))) \\cong \\prod_{i} \\mathrm{End}(s(i))^{(g^{-1}\\{i\\}) \\times (f^{-1}\\{i\})}.$$$$

Lean4

/-- Morphisms between two direct sums over a hom orthogonal family `s : ι → C`
are equivalent to block diagonal matrices,
with blocks indexed by `ι`,
and matrix entries in `i`-th block living in the endomorphisms of `s i`. -/
@[simps]
noncomputable def matrixDecomposition (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))
    where
  toFun z i j
    k :=
    eqToHom
        (by
          rcases k with ⟨k, ⟨⟩⟩
          simp) ≫
      biproduct.components z k j ≫
        eqToHom
          (by
            rcases j with ⟨j, ⟨⟩⟩
            simp)
  invFun
    z :=
    biproduct.matrix fun j k =>
      if h : f j = g k then z (f j) ⟨k, by simp [h]⟩ ⟨j, by simp⟩ ≫ eqToHom (by simp [h]) else 0
  left_inv
    z := by
    ext j k
    simp only [biproduct.matrix_π, biproduct.ι_desc]
    split_ifs with h
    · simp
      rfl
    · symm
      apply o.eq_zero h
  right_inv
    z := by
    ext i ⟨j, w⟩ ⟨k, ⟨⟩⟩
    simp only [eqToHom_refl, biproduct.matrix_components, Category.id_comp]
    split_ifs with h
    · simp
    · exfalso
      exact h w.symm

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