English
If X is projective, then Ext^{n+1}(X,Y) = 0 for all n and any Y.
Русский
Если X проектов, то Ext^{n+1}(X,Y) = 0 для всех n и любых Y.
LaTeX
$$$\\text{IsZero}(\\mathrm{Ext}^{n+1}_R(X,Y))$ for all n when X is projective$$
Lean4
/-- If `X : C` is projective and `n : ℕ`, then `Ext^(n + 1) X Y ≅ 0` for any `Y`. -/
theorem isZero_Ext_succ_of_projective (X Y : C) [Projective X] (n : ℕ) :
IsZero (((Ext R C (n + 1)).obj (Opposite.op X)).obj Y) :=
by
refine IsZero.of_iso ?_ ((ProjectiveResolution.self X).isoExt (n + 1) Y)
rw [← HomologicalComplex.exactAt_iff_isZero_homology, HomologicalComplex.exactAt_iff]
refine ShortComplex.exact_of_isZero_X₂ _ ?_
dsimp
rw [IsZero.iff_id_eq_zero]
ext (x : _ ⟶ _)
obtain rfl : x = 0 :=
(HomologicalComplex.isZero_single_obj_X (ComplexShape.down ℕ) 0 X (n + 1) (by simp)).eq_of_src _ _
rfl
