projective_iff_subsingleton_ext_one

English

An object X is projective iff Ext^1(X,Y) is subsingleton for all Y.

Русский

Объект X проективен тогда и только тогда, когда Ext^1(X,Y) — это подмножество с одним элементом для всех Y.

LaTeX

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

Lean4

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

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