projective_iff_hasProjectiveDimensionLT_one

English

An object X is projective iff HasProjectiveDimensionLT X 1.

Русский

Объект X проективен тогда и только тогда, когда HasProjectiveDimensionLT X 1.

LaTeX

$$$ \text{Projective}(X) \iff \operatorname{HasProjectiveDimensionLT}(X,1). $$$

Lean4

theorem projective_iff_hasProjectiveDimensionLT_one (X : C) : Projective X ↔ HasProjectiveDimensionLT X 1 :=
  by
  letI := HasExt.standard C
  exact
    ⟨fun _ ↦ inferInstance, fun _ ↦
      projective_iff_subsingleton_ext_one.2 (HasProjectiveDimensionLT.subsingleton X 1 1 (by rfl))⟩

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