isoCoproduct_inv — Mathlib

English

The inverse of the coproduct isoCoproduct is described by the Sigma.desc of injections.

Русский

Обратный изоморфизм копродукта задан описанием Sigma.desc инъекций.

LaTeX

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

Lean4

@[simp]
theorem isoCoproduct_inv {f : J → C} [HasBiproduct f] : (biproduct.isoCoproduct f).inv = Sigma.desc (biproduct.ι f) :=
  colimit.hom_ext fun j => by simp [biproduct.isoCoproduct]

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