add_eq_lift_id_desc — Mathlib

English

If X ⊞ X exists as a binary biproduct, then addition of morphisms is given by lifting the identities and descending; i.e., f + g = lift(id_X, id_X) ∘ desc(f,g).

Русский

Если существуют бинарные биопродукты X ⊞ X, то сложение морфизмов определяется как lift(id_X, id_X) ∘ desc(f,g).

LaTeX

$$$f,g: X \to Y:\; f+g = \mathrm{biprod.lift}(\mathrm{id}_X,\mathrm{id}_X) \circ \mathrm{biprod.desc}(f,g)$$$

Lean4

/-- The existence of binary biproducts implies that there is at most one preadditive structure. -/
theorem add_eq_lift_id_desc [HasBinaryBiproduct X X] : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g := by simp

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