prop_biprod — Mathlib

English

If X1 and X2 have property P in a preadditive category with zero object and a biproduct X1 ⊞ X2 exists, then the biproduct has P as well.

Русский

Если X1 и X2 обладают свойством P в предадитивной категории с нулевым образом и имеется би-произведение X1 ⊞ X2, то би-произведение обладает свойством P.

LaTeX

$$$\forall X_1,X_2, P(X_1) \to P(X_2) \to [\text{Preadditive}(C)] [\text{HasZeroObject}(C)] [\text{HasBinaryBiproduct}(X_1,X_2)] \Rightarrow P(X_1 \oplus X_2).$$$

Lean4

theorem prop_biprod {X₁ X₂ : C} (h₁ : P X₁) (h₂ : P X₂) [Preadditive C] [HasZeroObject C] [P.IsClosedUnderExtensions]
    [HasBinaryBiproduct X₁ X₂] : P (X₁ ⊞ X₂) :=
  P.prop_X₂_of_shortExact (ShortComplex.Splitting.ofHasBinaryBiproduct X₁ X₂).shortExact h₁ h₂

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