map_matrix — Mathlib

English

The interplay between biproduct.map and biproduct.matrix yields a product-like composition identity: map m ≫ matrix n equals matrix of the composites m_jk ≫ n_k.

Русский

Согласование между map и matrix: map m ≫ matrix n = matrix (m_jk ≫ n_k).

LaTeX

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

Lean4

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

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