English
Let f, g : J → C be families with biproducts, and p : J → C a family of arrows p j : f j → g j that are all mono. Then the induced map Sigma.map p between biproducts is mono.
Русский
Пусть f, g : J → C — семейства с биопродуктами, и p : J → Hom(f j, g j) — семейство стрелок мономорфизмов. Тогда отображение Sigma.map p между биопродуктами мономорфно.
LaTeX
$$$\\forall J\\, C\\, (\\text{HasBiproduct } f)(\\text{HasBiproduct } g)(p : \\forall j, f\\,j ⟶ g\\,j)\\; (H: \\forall j, Mono(p\\,j)):\\; Mono(\\Sigma.map p).$$$
Lean4
instance map_mono {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ j, f j ⟶ g j) [∀ j, Mono (p j)] :
Mono (Sigma.map p) :=
by
rw [show Sigma.map p = (biproduct.isoCoproduct _).inv ≫ biproduct.map p ≫ (biproduct.isoCoproduct _).hom by aesop]
infer_instance
