feat(CategoryTheory/Triangulated): localizing subcategories

[joelriou]

We show that the functor from the Verdier quotient A/(A ⊓ B) to C/B is fully faithful when A is a B-right- or left-localizing triangulated subcategory in the sense of Verdier.

---

• depends on: [Merged by Bors] - feat(CategoryTheory/Triangulated): definition of localising subcategories #38987
• depends on: [Merged by Bors] - feat(CategoryTheory): localizer morphisms which induces fully faithful functors on localized categories #38804
• depends on: [Merged by Bors] - feat(CategoryTheory): the opposite of a full subcategory #38803
• depends on: [Merged by Bors] - feat(CategoryTheory/Localization): lemmas regarding calculus of fractions and full/faithful functors #38802
• depends on: [Merged by Bors] - feat(CategoryTheory): the opposite of a triangulated subcategory #38650

[github-actions]

PR summary e336692c24

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ IsVerdierLeftLocalizing.fullyFaithful
+ IsVerdierRightLocalizing.fullyFaithful
+ instance : ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Faithful := by
+ instance : ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Full := by
+ instance [A.IsVerdierLeftLocalizing B] :
+ instance [A.IsVerdierLeftLocalizing B] [Preadditive D₁] [Preadditive D₂]
+ instance [A.IsVerdierRightLocalizing B] :
+ instance [Preadditive D₁] [Preadditive D₂] [L₁.Additive] [L₂.Additive] :
+ inverseImage_opEquivalence_inverse_trW_inverseImage_ι_op
+ trW_inverseImage_ι_iff
+ triangulatedLocalizerMorphism
++ instance [A.IsTriangulated] :

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.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - feat(CategoryTheory/Triangulated): definition of localising subcategories #38987
• [Merged by Bors] - feat(CategoryTheory): localizer morphisms which induces fully faithful functors on localized categories #38804
• [Merged by Bors] - feat(CategoryTheory): the opposite of a full subcategory #38803
• [Merged by Bors] - feat(CategoryTheory/Localization): lemmas regarding calculus of fractions and full/faithful functors #38802
• [Merged by Bors] - feat(CategoryTheory): the opposite of a triangulated subcategory #38650
  By Dependent Issues (🤖). Happy coding!