feat(AlgebraicTopology): cylinder objects in model categories

[joelriou]

---

• depends on: feat(CategoryTheory): the retract argument #20666
• depends on: feat(CategoryTheory): weak factorization systems #20680
• depends on: feat(AlgebraicTopology): application of the retract argument to model categories #20210

[github-actions]

PR summary 945ccc0a95

Import changes exceeding 2%

%	File
+7.93%	Mathlib.AlgebraicTopology.ModelCategory.Basic

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.AlgebraicTopology.ModelCategory.Basic	555	599	+44 (+7.93%)

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.MorphismProperty.LiftingProperty	1
Mathlib.AlgebraicTopology.ModelCategory.Basic	44
Mathlib.CategoryTheory.MorphismProperty.RetractArgument (new file)	595
Mathlib.CategoryTheory.MorphismProperty.WeakFactorizationSystem (new file)	596
Mathlib.AlgebraicTopology.ModelCategory.Instances (new file)	598
Mathlib.AlgebraicTopology.ModelCategory.IsFibrant (new file)	599
Mathlib.AlgebraicTopology.ModelCategory.Cylinder (new file)	601

---

Declarations diff

+ Cylinder
+ IsCofibrant
+ IsFibrant
+ IsGood
+ IsPushout.of_coprod_inl_with_id
+ IsVeryGood
+ IsWeakFactorizationSystem
+ RetractArrow.ofLeftLiftingProperty
+ RetractArrow.ofRightLiftingProperty
+ cofibrations_isStableUnderCoproductsOfShape
+ cofibrations_rlp
+ exists_very_good_cylinder
+ fibrations_isStableUnderProductsOfShape
+ fibrations_llp
+ gc_llp_rlp
+ hasLiftingProperty_of_wfs
+ i
+ inl_i
+ inr_i
+ instance (P₁ P₂ : MorphismProperty C)
+ instance : (cofibrations C).IsMultiplicative := by
+ instance : (cofibrations C).IsStableUnderCobaseChange := by
+ instance : (fibrations C).IsMultiplicative := by
+ instance : (fibrations C).IsStableUnderBaseChange := by
+ instance : (ofFactorizationData h).IsVeryGood
+ instance : (trivialCofibrations C).IsMultiplicative := by
+ instance : (trivialCofibrations C).IsStableUnderCobaseChange := by
+ instance : (trivialFibrations C).IsMultiplicative := by
+ instance : (trivialFibrations C).IsStableUnderBaseChange := by
+ instance : MorphismProperty.IsWeakFactorizationSystem (cofibrations C) (trivialFibrations C)
+ instance : MorphismProperty.IsWeakFactorizationSystem (trivialCofibrations C) (fibrations C)
+ instance : WeakEquivalence P.i₀
+ instance : WeakEquivalence P.i₁
+ instance : WeakEquivalence h.i := by
+ instance : WeakEquivalence h.p := by
+ instance [(cofibrations C).IsStableUnderCobaseChange] [hf : Cofibration f] :
+ instance [(cofibrations C).IsStableUnderCobaseChange] [hg : Cofibration g] :
+ instance [(cofibrations C).IsStableUnderComposition]
+ instance [(fibrations C).IsStableUnderComposition]
+ instance [(weakEquivalences C).ContainsIdentities] (X : C) :
+ instance [(weakEquivalences C).IsStableUnderComposition]
+ instance [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C]
+ instance [CategoryWithWeakEquivalences C] [CategoryWithFibrations C]
+ instance [HasInitial C] [HasBinaryCoproduct X Y] [hX : IsCofibrant X] :
+ instance [HasInitial C] [HasBinaryCoproduct X Y] [hY : IsCofibrant Y] :
+ instance [HasTerminal C] [IsFibrant A] [(fibrations C).IsStableUnderComposition] :
+ instance [IsCofibrant A] (P P' : Cylinder A) [P.IsGood] [P'.IsGood] :
+ instance [IsCofibrant A] [P.IsGood] : Cofibration P.i₀ := by
+ instance [IsCofibrant A] [P.IsGood] : Cofibration P.i₁ := by
+ instance [IsCofibrant A] [P.IsGood] : IsCofibrant P.I
+ instance [IsWeakFactorizationSystem (cofibrations C) (trivialFibrations C)] :
+ instance [IsWeakFactorizationSystem (cofibrations C) (trivialFibrations C)] [IsIso f] :
+ instance [IsWeakFactorizationSystem (trivialCofibrations C) (fibrations C)] :
+ instance [IsWeakFactorizationSystem (trivialCofibrations C) (fibrations C)] [IsIso f] :
+ instance [P.IsGood] : P.symm.IsGood
+ instance [P.IsVeryGood] : P.symm.IsVeryGood
+ isCofibrant_iff
+ isCofibrant_iff_of_isInitial
+ isCofibrant_of_cofibration
+ isFibrant_iff
+ isFibrant_iff_of_isTerminal
+ isFibrant_of_fibration
+ isPushout_of_isColimit_binaryCofan
+ le_llp_iff_le_rlp
+ llp_eq_of_le_llp_of_hasFactorization_of_isStableUnderRetracts
+ llp_eq_of_wfs
+ llp_of_isIso
+ mem_trivialCofibrations_iff
+ mem_trivialFibrations_iff
+ mk'.cm3a_aux
+ ofFactorizationData
+ ofFactorizationData_i
+ rlp_eq_of_le_rlp_of_hasFactorization_of_isStableUnderRetracts
+ rlp_eq_of_wfs
+ rlp_of_isIso
+ symm
+ symm_i
+ trans
+ trivialCofibrations_isStableUnderCoproductsOfShape
+ trivialCofibrations_rlp
+ trivialFibrations_isStableUnderProductsOfShape
+ trivialFibrations_llp
+ weakEquivalence_of_postcomp
+ weakEquivalence_of_postcomp_of_fac
+ weakEquivalence_of_precomp
+ weakEquivalence_of_precomp_of_fac
++ instance : Cofibration h.i := by
++ instance : Fibration h.p := by
++ instance [(fibrations C).IsStableUnderBaseChange]
++ instance [(trivialCofibrations C).IsStableUnderCobaseChange]
++ instance [(trivialFibrations C).IsStableUnderBaseChange]
++ instance [IsWeakFactorizationSystem (cofibrations C) (trivialFibrations C)]
++ mk'
+++++ instance [IsWeakFactorizationSystem (trivialCofibrations C) (fibrations C)]

You can run this locally as follows

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

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/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).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat(CategoryTheory): the retract argument #20666
• feat(CategoryTheory): weak factorization systems #20680
• feat(AlgebraicTopology): application of the retract argument to model categories #20210
  By Dependent Issues (🤖). Happy coding!