isoCoproduct_hom — Mathlib

English

The forward map of the coproduct isoCoproduct is the described by the universal arrow to the Sigma-ι structure.

Русский

Прямой маппинг копродукта задаётся через Sigma.ι.

LaTeX

$$$\forall J\, C [HasBiproduct f] : (biproduct.isoCoproduct f).hom = biproduct.desc (Sigma.ι f)$$$

Lean4

@[simp]
theorem isoCoproduct_hom {f : J → C} [HasBiproduct f] : (biproduct.isoCoproduct f).hom = biproduct.desc (Sigma.ι f) :=
  biproduct.hom_ext' _ _ fun j => by simp [← Iso.eq_comp_inv]

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