matrix_map — Mathlib

English

The matrix map interacts with composition in a way that composing with a map n on the right distributes over matrix composition; i.e., biproduct.matrix m ≫ biproduct.map n equals biproduct.matrix of the composite m j k ≫ n k.

Русский

Матрица би-производной совместима с композициями: matrix m ≫ map n = matrix (m j k ≫ n k).

LaTeX

$$$\operatorname{biproduct.matrix} m \;\gg\; \operatorname{biproduct.map} n = \operatorname{biproduct.matrix} (\lambda j k, m_{j k} \gg n_k)$$$

Lean4

@[reassoc]
theorem matrix_map {f : J → C} {g : K → C} {h : K → C} (m : ∀ j k, f j ⟶ g k) (n : ∀ k, g k ⟶ h k) :
    biproduct.matrix m ≫ biproduct.map n = biproduct.matrix fun j k => m j k ≫ n k :=
  by
  ext
  simp

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