[Merged by Bors] - feat: more basic API for pretriangulated categories

[joelriou]

This PR slightly extends the basic API of pretriangulated categories.

---

[jcommelin]

There are 3 coyoneda_exact lemmas, but only 2 yoneda_exact lemmas. Is that on purpose?

[joelriou]

There are 3 coyoneda_exact lemmas, but only 2 yoneda_exact lemmas. Is that on purpose?

Yes, it is on purpose. Indeed, the yoneda_exact₁ variant would be quite unpractical because of the complicated formulation of the condition on the morphism:

lemma yoneda_exact₁ (T : Triangle C) (hT : T ∈ distTriang C) {X : C} (f : T.obj₁ ⟶ X)
    (hf : T.mor₃⟦(-1 : ℤ)⟧' ≫ (shiftEquiv C (1 : ℤ)).unitIso.inv.app T.obj₁ ≫ f = 0) :
    ∃ (g : T.obj₂ ⟶ X), f = T.mor₁ ≫ g :=
  yoneda_exact₂ T.invRotate (inv_rot_of_dist_triangle _ hT) f (by
    simpa using hf)

If we ever need this in the applications, it would be more obvious to me to directly use yoneda_exact₂ T.invRotate rather than yoneda_exact₁. Do you think I should include it anyway?

[jcommelin]

Sorry for the late response. I think your reasoning for leaving out the yoneda_exact_1 variant is fine.

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style