hasProjectiveDimensionLT_iff — Mathlib

English

HasProjectiveDimensionLT X n holds iff Ext^i(X,Y) vanishes for all i ≥ n and all Y.

Русский

HasProjectiveDimensionLT X n эквивалентно исчезновению Ext^i(X,Y) для всех i ≥ n и всех Y.

LaTeX

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

Lean4

theorem hasProjectiveDimensionLT_iff [HasExt.{w} C] :
    HasProjectiveDimensionLT X n ↔ ∀ (i : ℕ) (_ : n ≤ i) ⦃Y : C⦄, ∀ (e : Ext X Y i), e = 0 :=
  ⟨fun _ _ hi _ e ↦ e.eq_zero_of_hasProjectiveDimensionLT n hi, HasProjectiveDimensionLT.mk⟩

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