total — Mathlib

English

Specialized form of map_eq under finite biproducts: the biproduct map equals the finite sum of composites with injections and projections for each index.

Русский

Уточненная форма map_eq при конечных бинарных би-произведениях: biproduct.map равен конечной сумме композициями с инъекциями и проекциями по каждому индексу.

LaTeX

$$$\operatorname{biproduct.map} h = \sum_{j \in J} \; \operatorname{comp} (\operatorname{biproduct.π} f j) (h j) (\operatorname{biproduct.ι} g j)$$$

Lean4

/-- In any preadditive category, any binary biproduct satisfies
`biprod.fst ≫ biprod.inl + biprod.snd ≫ biprod.inr = 𝟙 (X ⊞ Y)`.
-/
@[simp]
theorem total : biprod.fst ≫ biprod.inl + biprod.snd ≫ biprod.inr = 𝟙 (X ⊞ Y) := by ext <;> simp

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