mk — Mathlib · SciLib

English

Given a property forcing Ext groups to vanish, one obtains HasInjectiveDimensionLT X n.

Русский

При заданном условии, гарантирующем нулевые Ext-группы, строится HasInjectiveDimensionLT X n.

LaTeX

$$$\text{HasInjectiveDimensionLT}(X,n)$$$

Lean4

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

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