projectiveDimension_lt_iff — Mathlib

English

For any object X, the statement 'projectiveDimension X < n' is equivalent to HasProjectiveDimensionLT X n.

Русский

Для любого объекта X утверждение 'pd(X) < n' эквивалентно HasProjectiveDimensionLT X n.

LaTeX

$$$\forall X:\mathcal C, \forall n:\mathbb N,\operatorname{projectiveDimension}(X) < n \iff HasProjectiveDimensionLT(X, n)$$$

Lean4

theorem projectiveDimension_lt_iff {X : C} {n : ℕ} : projectiveDimension X < n ↔ HasProjectiveDimensionLT X n :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ sInf_lt_iff.2 ?_⟩
  · have : projectiveDimension X ∈ _ := csInf_mem ⟨⊤, by simp⟩
    simp only [Set.mem_setOf_eq] at this
    exact this _ h
  · obtain _ | n := n
    · exact ⟨⊥, fun _ _ ↦ hasProjectiveDimensionLT_of_ge _ 0 _ (by simp), by decide⟩
    ·
      exact
        ⟨n, fun i hi ↦ hasProjectiveDimensionLT_of_ge _ (n + 1) _ (by simpa using hi), by simp [WithBot.lt_add_one_iff]⟩

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