Theorems · Theorem · category theory

isZero_Ext_succ_of_projective

∀ {R : Type u_1} [inst : Ring R] {C : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.Linear R C] [inst_4 : CategoryTheory.EnoughProjectives C]
  (X Y : C) [CategoryTheory.Projective X] (n : ℕ),
  CategoryTheory.Limits.IsZero (((Ext R C (n + 1)).obj (Opposite.op X)).obj Y)

If X : C is projective and n : ℕ, then Ext^(n + 1) X Y ≅ 0 for any Y.

Defined in

Mathlib.CategoryTheory.Abelian.Ext

Cited by

1 results in Mathlib

Foundations

Depth 115 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingCategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.LinearCategoryTheory.EnoughProjectivesCategoryTheory.Projective