injective_iff_subsingleton_ext_one

English

For an abelian category with HasExt available, an object X is injective if and only if for every Y the group Ext^1(Y,X) is a subsingleton.

Русский

В абелевой категории, если для каждого Y группа Ext^1(Y,X) сведена к ед. элементу, то X injective; и наоборот.

LaTeX

$$$\text{Injective}(X) \iff \forall Y,\operatorname{Subsingleton}(\operatorname{Ext}^1(Y,X))$$$

Lean4

theorem injective_iff_subsingleton_ext_one [HasExt.{w} C] {X : C} : Injective X ↔ ∀ ⦃Y : C⦄, Subsingleton (Ext Y X 1) :=
  by
  refine ⟨fun h ↦ HasInjectiveDimensionLT.subsingleton X 1 1 (by rfl), fun h ↦ ⟨fun f g _ ↦ ?_⟩⟩
  obtain ⟨φ, hφ⟩ :=
    Ext.contravariant_sequence_exact₁ { exact := ShortComplex.exact_cokernel g } _ (Ext.mk₀ f) (zero_add 1)
      (by subsingleton)
  obtain ⟨φ, rfl⟩ := Ext.homEquiv₀.symm.surjective φ
  exact ⟨φ, Ext.homEquiv₀.symm.injective (by simpa using hφ)⟩

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