We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 2d78c61 commit ea9c914Copy full SHA for ea9c914
Mathlib/CategoryTheory/Triangulated/Yoneda.lean
@@ -39,13 +39,15 @@ section
39
variable [HasZeroObject C] [∀ (n : ℤ), (shiftFunctor C n).Additive]
40
[Pretriangulated C]
41
42
+@[stacks 0149]
43
instance (A : Cᵒᵖ) : (preadditiveCoyoneda.obj A).IsHomological where
44
exact T hT := by
45
rw [ShortComplex.ab_exact_iff]
46
intro (x₂ : A.unop ⟶ T.obj₂) (hx₂ : x₂ ≫ T.mor₂ = 0)
47
obtain ⟨x₁, hx₁⟩ := T.coyoneda_exact₂ hT x₂ hx₂
48
exact ⟨x₁, hx₁.symm⟩
49
50
51
instance (B : C) : (preadditiveYoneda.obj B).IsHomological where
52
53
0 commit comments