lift_desc — Mathlib

English

A repeated interaction between biproduct.matrix and biproduct.map yields a simple equality with a reshaped matrix: composition equals a matrix of componentwise compositions.

Русский

Повторение взаимодействия matrix и map: map m ≫ matrix n = matrix (m j k ≫ n k).

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem lift_desc {T U : C} {f : T ⟶ X} {g : T ⟶ Y} {h : X ⟶ U} {i : Y ⟶ U} :
    biprod.lift f g ≫ biprod.desc h i = f ≫ h + g ≫ i := by simp [biprod.lift_eq, biprod.desc_eq]

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