add_eq_lift_desc_id — Mathlib

English

In a binary biproduct Y ⊞ Y, f + g = lift(f,g) ∘ desc(id_Y, id_Y).

Русский

В бинарном биопродукте Y ⊞ Y, для морфизмов f,g: X ⟶ Y имеем f+g = lift(f,g) ∘ desc(id_Y, id_Y).

LaTeX

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

Lean4

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

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