feat(AlgebraicTopology): proper model categories

[joelriou]

Some fixes are also done in the pullbacks API: this allows to avoid adding set_option backward.isDefEq.respectTransparency false in the new file (and the downstream PR #41735).

---

[github-actions]

PR summary 41ba022005

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.AlgebraicTopology.ModelCategory.Proper (new file)	673

---

Declarations diff (regex)

+ IsLeftProper
+ IsRightProper
+ instance (i : X ⟶ Y) (w : X ⟶ X') [Cofibration i] [WeakEquivalence w] [HasPushout i w] :
+ instance (i : X ⟶ Y) (w : X ⟶ X') [Cofibration i] [WeakEquivalence w] [HasPushout w i] :
+ instance [CategoryWithCofibrations C] [CategoryWithWeakEquivalences C] [IsLeftProper C] :
+ instance [CategoryWithFibrations C] [CategoryWithWeakEquivalences C] [IsRightProper C] :
+ isLeftProper_op_iff
+ isRightProper_op_iff
++ instance (p : E ⟶ B) (w : B' ⟶ B) [Fibration p] [WeakEquivalence w]
++ instance [(cofibrations C).IsStableUnderCobaseChange]
++ instance [(fibrations C).IsStableUnderBaseChange]
++ weakEquivalence
++ weakEquivalence'

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.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 41ba022).

• +28 new declarations
• −0 removed declarations

+HomotopicalAlgebra.IsLeftProper
+HomotopicalAlgebra.IsLeftProper.casesOn
+HomotopicalAlgebra.IsLeftProper.instWeakEquivalenceInlOfCofibration
+HomotopicalAlgebra.IsLeftProper.instWeakEquivalenceInrOfCofibration
+HomotopicalAlgebra.IsLeftProper.instWeakEquivalenceMapCompId
+HomotopicalAlgebra.IsLeftProper.instWeakEquivalenceMapCompId_1
+HomotopicalAlgebra.IsLeftProper.isStableUnderCobaseChangeAlong
+HomotopicalAlgebra.IsLeftProper.mk
+HomotopicalAlgebra.IsLeftProper.rec
+HomotopicalAlgebra.IsLeftProper.recOn
+HomotopicalAlgebra.IsLeftProper.weakEquivalence
+HomotopicalAlgebra.IsLeftProper.weakEquivalence'
+HomotopicalAlgebra.IsRightProper
+HomotopicalAlgebra.IsRightProper.casesOn
+HomotopicalAlgebra.IsRightProper.instWeakEquivalenceFstOfFibration
+HomotopicalAlgebra.IsRightProper.instWeakEquivalenceMapCompId
+HomotopicalAlgebra.IsRightProper.instWeakEquivalenceMapCompId_1
+HomotopicalAlgebra.IsRightProper.instWeakEquivalenceSndOfFibration
+HomotopicalAlgebra.IsRightProper.isStableUnderBaseChangeAlong
+HomotopicalAlgebra.IsRightProper.mk
+HomotopicalAlgebra.IsRightProper.rec
+HomotopicalAlgebra.IsRightProper.recOn
+HomotopicalAlgebra.IsRightProper.weakEquivalence
+HomotopicalAlgebra.IsRightProper.weakEquivalence'
+HomotopicalAlgebra.instIsLeftProperOppositeOfIsRightProper
+HomotopicalAlgebra.instIsRightProperOppositeOfIsLeftProper
+HomotopicalAlgebra.isLeftProper_op_iff
+HomotopicalAlgebra.isRightProper_op_iff

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 41ba022005
Reference commit 14c4b77b0c

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).