instBiprod — Mathlib

English

The biproduct (direct sum) of two injective objects is injective, provided the category has zero morphisms and binary biproducts.

Русский

Бипродукт двух инъективных объектов инъективен, если в категории существуют нулевые морфизмы и двоичные би-продукты.

LaTeX

$$$$\text{Injective}(P) \land \text{Injective}(Q) \Rightarrow \text{Injective}(P \oplus Q).$$$$

Lean4

instance {P Q : C} [HasZeroMorphisms C] [HasBinaryBiproduct P Q] [Injective P] [Injective Q] : Injective (P ⊞ Q) where
  factors g f
    mono := by
    refine ⟨biprod.lift (factorThru (g ≫ biprod.fst) f) (factorThru (g ≫ biprod.snd) f), ?_⟩
    ext
    · simp only [Category.assoc, biprod.lift_fst, comp_factorThru]
    · simp only [Category.assoc, biprod.lift_snd, comp_factorThru]

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