English
Let J be a index set, C a category with zero morphisms, and f, g: J → C objects admitting biproducts. If p j : f j → g j is a morphism for every j and each p j is a mono, then the induced map between biproducts, biproduct.map p, is mono.
Русский
Пусть J — множество индексов, C — категория с нулевыми морфизмами, f, g : J → C такие, что существуют би-одинообразия. Если для каждого j существует морфизм p j : f j → g j и все p j мономорфизмы, тогда индуцированное отображение между биопродуктами biproduct.map p является мономорфизмом.
LaTeX
$$$\\forall J\\, C\\, (\\text{HasBiproduct } f) (\\text{HasBiproduct } g)\n (p : \\forall j \\in J, f\\,j \\to g\\,j)\\; (H: \\forall j, Mono(p\\,j)):\\; Mono(\\text{biproduct.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 (biproduct.map p) :=
by
rw [show biproduct.map p = (biproduct.isoProduct _).hom ≫ Pi.map p ≫ (biproduct.isoProduct _).inv by aesop]
infer_instance
