decomp_hom_to — Mathlib

English

Every morphism to a biproduct factors as a sum of components going through the two summands.

Русский

Каждый морфизм в би-производное факторизуется через сумму компонент, проходящих через две составляющие.

LaTeX

$$$\exists f_1 f_2,\; f = f_1 \;\gg\; inl \; + \; f_2 \;\gg\; inr$$$

Lean4

theorem decomp_hom_to (f : Z ⟶ X ⊞ Y) : ∃ f₁ f₂, f = f₁ ≫ biprod.inl + f₂ ≫ biprod.inr :=
  ⟨f ≫ biprod.fst, f ≫ biprod.snd, by aesop⟩

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