[Merged by Bors] - feat(CategoryTheory/Triangulated): definition of localising subcategories

[joelriou]

Let C be a pretriangulated category. If A and B are triangulated subcategories of C, we define predicates (typeclasses IsVerdierRightLocalizing and IsVerdierLeftLocalizing) saying that A is right B-localizing (or left B-localizing). When B is closed under isomorphisms, we shall show that this implies that the functor from the Verdier quotient A/(A ⊓ B) to C/B is fully faithful (#38651).

---

[github-actions]

PR summary ab9605ce36

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory (new file)	1235

---

Declarations diff

+ FullyFaithful.unop
+ IsVerdierLeftLocalizing
+ IsVerdierLeftLocalizing.fac'
+ IsVerdierRightLocalizing
+ IsVerdierRightLocalizing.fac'
+ distinguished_cocone_triangle
+ distinguished_cocone_triangle₁
+ distinguished_cocone_triangle₂
+ instance (A B : ObjectProperty C) [A.IsVerdierLeftLocalizing B] :
+ instance (A B : ObjectProperty C) [A.IsVerdierRightLocalizing B] :
+ instance (A B : ObjectProperty Cᵒᵖ) [A.IsVerdierLeftLocalizing B] :
+ instance (A B : ObjectProperty Cᵒᵖ) [A.IsVerdierRightLocalizing B] :
+ instance [P.ContainsZero] [Q.ContainsZero] [Q.IsClosedUnderIsomorphisms] :
+ instance {Q : ObjectProperty C} [P.IsTriangulated] [Q.IsTriangulated]
+ isVerdierLeftLocalizing_iff
+ isVerdierLeftLocalizing_op_iff
+ isVerdierRightLocalizing_iff
+ isVerdierRightLocalizing_op_iff
+ trW_monotone

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[dagurtomas]

The code looks fine to me, but could you give a more precise reference to the corresponding definitions in Verdier, and whether this is called something else there? And indicate future goals with this code

[joelriou]

The code looks fine to me, but could you give a more precise reference to the corresponding definitions in Verdier, and whether this is called something else there? And indicate future goals with this code

I have added a TODO and a reference to Proposition 2.3.5 (chapitre II) in Verdier's Astérique.
This notion does not seem to appear in Neeman's book, nor in the stacks project (it may have appeared at https://stacks.math.columbia.edu/tag/05RW but it is not mentionned).

[dagurtomas]

Thanks!

maintainer delegate

[github-actions]

🚀 Pull request has been placed on the maintainer queue by dagurtomas.

[riccardobrasca]

Thanks!

bors d+

[mathlib-bors]

✌️ joelriou can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[joelriou]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-CI job
• ci (staging) / Build
• ci (staging) / Lint style
• ci (staging) / Post-Build Step