matrix_desc — Mathlib

English

The matrix of morphisms from J to K, when composed with a descent along x, equals the descent of the sums over j of m_{j k} followed by x_k; i.e., matrix_desc expresses a compatibility between matrices and descent maps.

Русский

Матрица отображений между множества индексов совместима с descent: описывая m, затем применяя desc, мы получаем descent от сумм по k и x_k.

LaTeX

$$$\operatorname{biproduct.matrix} m \;\gg\; \operatorname{biproduct.desc} x = \operatorname{biproduct.desc} (\lambda j, \sum_k m_{j k} \,\gg\; x_k)$$$

Lean4

@[reassoc]
theorem matrix_desc [Fintype K] {f : J → C} {g : K → C} (m : ∀ j k, f j ⟶ g k) {P} (x : ∀ k, g k ⟶ P) :
    biproduct.matrix m ≫ biproduct.desc x = biproduct.desc fun j => ∑ k, m j k ≫ x k :=
  by
  ext
  simp [lift_desc]

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