matrixDecomposition_id — Mathlib

English

The matrix corresponding to the identity morphism on a biproduct is the identity matrix in each block.

Русский

Матрица, соответствующая тождественному морфизму на би-произведении, является тождественной в каждом блоке.

LaTeX

$$$$ o.matrixDecomposition(\\mathrm{id}_{\\bigoplus s(f)}) = \\mathbf{1}.$$$$

Lean4

@[simp]
theorem matrixDecomposition_id (o : HomOrthogonal s) {α : Type} [Finite α] {f : α → ι} (i : ι) :
    o.matrixDecomposition (𝟙 (⨁ fun a => s (f a))) i = 1 :=
  by
  ext ⟨b, ⟨⟩⟩ ⟨a, j_property⟩
  simp only [Set.mem_preimage, Set.mem_singleton_iff] at j_property
  simp only [Category.comp_id, Category.id_comp, End.one_def, eqToHom_refl, Matrix.one_apply,
    HomOrthogonal.matrixDecomposition_apply, biproduct.components]
  split_ifs with h
  · cases h
    simp
  · simp only [Subtype.mk.injEq] at h
    convert comp_zero
    simpa using biproduct.ι_π_ne _ (Ne.symm h)

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