feat(AlgebraicTopology): application of the retract argument to model categories#20210
Conversation
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
PR summary 4516ade296Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.AlgebraicTopology.ModelCategory.Basic | 603 | 665 | +62 (+10.28%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.AlgebraicTopology.ModelCategory.Basic |
62 |
Mathlib.AlgebraicTopology.ModelCategory.Instances (new file) |
664 |
Declarations diff
+ cofibrations_rlp
+ fibrations_llp
+ instance : (cofibrations C).IsMultiplicative := by
+ instance : (cofibrations C).IsStableUnderCobaseChange := by
+ instance : (fibrations C).IsMultiplicative := by
+ instance : (fibrations C).IsStableUnderBaseChange := by
+ 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 [(cofibrations C).IsStableUnderCobaseChange] [hf : Cofibration f] :
+ instance [(cofibrations C).IsStableUnderCobaseChange] [hg : Cofibration g] :
+ instance [(cofibrations C).IsStableUnderComposition]
+ instance [(fibrations C).IsStableUnderComposition]
+ instance [(weakEquivalences C).IsStableUnderComposition]
+ instance [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C]
+ instance [CategoryWithWeakEquivalences C] [CategoryWithFibrations C]
+ 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] :
+ isStableUnderCoproductsOfShape_cofibrations
+ isStableUnderCoproductsOfShape_trivialCofibrations
+ isStableUnderProductsOfShape_fibrations
+ isStableUnderProductsOfShape_trivialFibrations
+ mk'
+ trivialCofibrations_rlp
+ trivialFibrations_llp
+ weakEquivalence_of_postcomp
+ weakEquivalence_of_postcomp_of_fac
+ weakEquivalence_of_precomp
+ weakEquivalence_of_precomp_of_fac
++ instance [(fibrations C).IsStableUnderBaseChange]
++ instance [(trivialCofibrations C).IsStableUnderCobaseChange]
++ instance [(trivialFibrations C).IsStableUnderBaseChange]
++ instance [IsWeakFactorizationSystem (cofibrations C) (trivialFibrations C)]
+++++ 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
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
In a category, if `i ≫ p = f`, and `f` has the left lifting property with respect to `p`, then `f` is a retract of `i`. This statement and its dual are formalised, as well as consequences for classes of morphisms which satisfy `HasFactorization W₁ W₂`. This is applied to classes of morphisms in model categories in #20210. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
…m.lean Co-authored-by: Calle Sönne <calle.sonne@gmail.com>
|
This PR has been migrated to a fork-based workflow: #26166 |
Basic consequences of the retract argument are obtained for model categories: cofibrations are exactly the morphisms that have the left lifting property with respect to trivial fibrations, etc. We deduce various properties of cofibrations, fibrations and weak equivalences in model categories (e.g. they are stable by composition).