map_eq_map' — Mathlib

English

For two biproduct diagrams f and g, a componentwise map p induces equality of the corresponding biproduct maps.

Русский

Для двух диаграмм би-произведения, отображение по компонентам порождает равенство отображений би-произведения.

LaTeX

$$$\forall J\, {f g : J \to C} [HasBiproduct f] [HasBiproduct g] (p : \forall j, f j \to g j) :\n biproduct.map p = biproduct.map' p$$$

Lean4

theorem map_eq_map' {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ b, f b ⟶ g b) :
    biproduct.map p = biproduct.map' p := by
  classical
  ext
  dsimp
  simp only [Discrete.natTrans_app, Limits.IsColimit.ι_map_assoc, Limits.IsLimit.map_π, ← Bicone.toCone_π_app_mk,
    ← Bicone.toCocone_ι_app_mk]
  dsimp
  rw [biproduct.ι_π_assoc, biproduct.ι_π]
  split_ifs with h
  · subst h; simp
  · simp

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