feat(CategoryTheory/Localization): transport resolutions along 2-commutative squares

[joelriou]

We transport LocalizerMorphism.HasLeft/RightResolutions assumptions along 2-commutative squares.

---

[github-actions]

PR summary 424dce2f30

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
9 files Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureCofibrant Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureFibrant Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived Mathlib.CategoryTheory.Localization.Resolution	1
Mathlib.CategoryTheory.Comma.CatCommSq (new file)	311

---

Declarations diff

+ catCommSq
+ essSurj_mapArrow
+ hasLeftResolutions_arrow_iff_of_equivalences
+ hasLeftResolutions_arrow_of_essSurj_of_full
+ hasLeftResolutions_iff_iso_of_essSurj_of_full
+ hasLeftResolutions_of_iso_of_essSurj
+ hasLeftResolutions_of_iso_of_essSurj_of_full
+ hasRightResolutions_arrow_iff_of_equivalences
+ hasRightResolutions_arrow_of_essSurj_of_full
+ hasRightResolutions_iff_iso_of_essSurj_of_full
+ hasRightResolutions_of_iso_of_essSurj
+ hasRightResolutions_of_iso_of_essSurj_of_full
+ instance (W : MorphismProperty C) [W.RespectsIso] : W.arrow.RespectsIso
+ instance [Φ.IsInduced] : Φ.arrow.IsInduced

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.