eq_zero_of_hasProjectiveDimensionLT

English

If HasProjectiveDimensionLT X n holds, then any Ext^i(X,Y) with i ≥ n vanishes.

Русский

Если HasProjectiveDimensionLT X n, то Ext^i(X,Y)=0 при i ≥ n.

LaTeX

$$$ [\text{HasProjectiveDimensionLT } X n] \Rightarrow \forall i \ge n, \forall Y, \operatorname{Ext}^i(X,Y)=0. $$$

Lean4

theorem eq_zero_of_hasProjectiveDimensionLT [HasExt.{w} C] {X Y : C} {i : ℕ} (e : Ext X Y i) (n : ℕ)
    [HasProjectiveDimensionLT X n] (hi : n ≤ i) : e = 0 :=
  (HasProjectiveDimensionLT.subsingleton X n i hi Y).elim _ _

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