hom_ext' — Mathlib

English

Dual extensionality: two arrows from the biproduct to Z are equal if they agree after precomposing with injections.

Русский

Дуальная экстенсиональность: два гомоморфизма из би-произведения в Z равны, если они совпадают после префиксации инъекциями.

LaTeX

$$$\forall J\, f \; [HasBiproduct f] \; {Z : C} (g h : ⨁ f \to Z) (w : \forall j, biproduct.ι f j ≫ g = biproduct.ι f j ≫ h) \Rightarrow g = h$$$

Lean4

@[ext]
theorem hom_ext' {f : J → C} [HasBiproduct f] {Z : C} (g h : ⨁ f ⟶ Z)
    (w : ∀ j, biproduct.ι f j ≫ g = biproduct.ι f j ≫ h) : g = h :=
  (biproduct.isColimit f).hom_ext fun j => w j.as

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