matrix_π — Mathlib

English

For finite J and K, and functions f : J → C, g : K → C, the matrix m determines a map to the biproduct and its projections satisfy a matrix-π compatibility condition.

Русский

Для конечных множеств J, K и функций f, g соответствующая матрица m задаёт отображение к биопродукту, а проекции удовлетворяют условию совместимости матрица-пi.

LaTeX

$$$\\text{biproduct.matrix } m \\; \\text{ и } \\text{biproduct.π } g k \; \Rightarrow \\text{равенство по описанию desc}$$$

Lean4

@[reassoc (attr := simp)]
theorem matrix_π (m : ∀ j k, f j ⟶ g k) (k : K) :
    biproduct.matrix m ≫ biproduct.π g k = biproduct.desc fun j => m j k :=
  by
  ext
  simp [biproduct.matrix]

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