mk — Mathlib · SciLib

English

If for every i ≥ n and every Y, Ext^i(X,Y) = 0, then HasProjectiveDimensionLT X n holds.

Русский

Если для каждого i ≥ n и каждого Y Ext^i(X,Y) = 0, то HasProjectiveDimensionLT X n выполняется.

LaTeX

$$$ \left( \forall i \ (n \le i) \ \forall Y, \operatorname{Ext}^i(X,Y)=0 \right) \Rightarrow \operatorname{HasProjectiveDimensionLT}(X,n). $$$

Lean4

theorem mk (hX : ∀ (i : ℕ) (_ : n ≤ i) ⦃Y : C⦄, ∀ (e : Ext X Y i), e = 0) : HasProjectiveDimensionLT X n where
  subsingleton' i hi
    Y := by
    have : Subsingleton (Ext X Y i) := ⟨fun e₁ e₂ ↦ by simp only [hX i hi]⟩
    letI := HasExt.standard C
    exact Ext.chgUniv.{max u v, w}.symm.subsingleton

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