injective_iff_hasInjectiveDimensionLT_one

English

For any X in an abelian category, Injective X is equivalent to HasInjectiveDimensionLT X 1.

Русский

Для любого X в абелевой категории инъективность эквивалентна HasInjectiveDimensionLT X 1.

LaTeX

$$$\text{Injective}(X) \iff \text{HasInjectiveDimensionLT}(X,1)$$$

Lean4

theorem injective_iff_hasInjectiveDimensionLT_one (X : C) : Injective X ↔ HasInjectiveDimensionLT X 1 :=
  by
  letI := HasExt.standard C
  exact
    ⟨fun _ ↦ inferInstance, fun _ ↦
      injective_iff_subsingleton_ext_one.2 (HasInjectiveDimensionLT.subsingleton X 1 1 (by rfl))⟩

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