feat(AlgebraicTopology/ModelCategory): a trick by Joyal#20224
feat(AlgebraicTopology/ModelCategory): a trick by Joyal#20224
Conversation
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
|
This PR/issue depends on: |
PR summary eecc0d927cImport changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.AlgebraicTopology.ModelCategory.Basic | 586 | 646 | +60 (+10.24%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.AlgebraicTopology.ModelCategory.Basic |
60 |
Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick (new file) |
640 |
Mathlib.CategoryTheory.MorphismProperty.WeakFactorizationSystem (new file) |
643 |
Mathlib.AlgebraicTopology.ModelCategory.Instances (new file) |
645 |
Declarations diff
+ IsWeakFactorizationSystem
+ cofibrations_isStableUnderCoproductsOfShape
+ cofibrations_rlp
+ fibrations_isStableUnderProductsOfShape
+ fibrations_llp
+ hasLiftingProperty_of_wfs
+ 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] :
+ joyal_trick
+ llp_eq_of_wfs
+ mk'.cm3a_aux
+ rlp_eq_of_wfs
+ 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 [(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
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).
…m.lean Co-authored-by: Calle Sönne <calle.sonne@gmail.com>
|
This pull request has conflicts, please merge |
|
This PR has been migrated to a fork-based workflow: #26169 |
In order to construct a model category, we may sometimes have basically proven all the axioms with the exception of the left lifting property of cofibrations with respect to trivial fibrations. A trick by Joyal allows to obtain this lifting property under suitable assumptions, namely that cofibrations are stable under composition and cobase change.