instHasInjectiveDimensionLTBiprod

English

In a ShortExact S, if X1 has LT n and X3 has LT n, then X2 has LT n.

Русский

В SE, если X1 и X3 имеют LT n, то X2 имеет LT n.

LaTeX

$$$S.ShortExact \Rightarrow (\text{HasInjectiveDimensionLT}(S.X_1,n) \land \text{HasInjectiveDimensionLT}(S.X_3,n)) \Rightarrow \text{HasInjectiveDimensionLT}(S.X_2,n)$$$

Lean4

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

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