instHasProjectiveDimensionLTBiprod

English

If objects X and Y have HasProjectiveDimensionLT n, then their biproduct X ⊞ Y has HasProjectiveDimensionLT n.

Русский

Если X и Y имеют HasProjectiveDimensionLT n, то их би-продукт X ⊞ Y имеет HasProjectiveDimensionLT n.

LaTeX

$$$\forall X,Y,\forall n:\mathbb{N}, HasProjectiveDimensionLT(X,n) \rightarrow HasProjectiveDimensionLT(Y,n) \rightarrow HasProjectiveDimensionLT(X \oplus Y,n)$$$

Lean4

instance (X Y : C) (n : ℕ) [HasProjectiveDimensionLT X n] [HasProjectiveDimensionLT Y n] :
    HasProjectiveDimensionLT (X ⊞ Y) n :=
  (ShortComplex.Splitting.ofHasBinaryBiproduct X Y).shortExact.hasProjectiveDimensionLT_X₂ n (by assumption)
    (by assumption)

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