English
If each component p_j is epi, then biproduct.map p is also epi.
Русский
Если каждый компонент p_j является эпиморфизмом, то biproduct.map p тоже эпиморфизм.
LaTeX
$$$\forall J\, {f g : J \to C} [HasBiproduct f] [HasBiproduct g] (p : \forall j, f j \to g j) [\forall j, Epi (p j)] : Epi (biproduct.map p)$$$
Lean4
instance map_epi {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ j, f j ⟶ g j) [∀ j, Epi (p j)] :
Epi (biproduct.map p) := by
classical
have : biproduct.map p = (biproduct.isoCoproduct _).hom ≫ Sigma.map p ≫ (biproduct.isoCoproduct _).inv :=
by
ext
simp only [map_π, isoCoproduct_hom, isoCoproduct_inv, Category.assoc, ι_desc_assoc, ι_colimMap_assoc,
Discrete.functor_obj_eq_as, Discrete.natTrans_app, colimit.ι_desc_assoc, Cofan.mk_pt, Cofan.mk_ι_app, ι_π,
ι_π_assoc]
split
all_goals simp_all
rw [this]
infer_instance
