[Merged by Bors] - feat(CategoryTheory/SmallObject): the functorial factorization#21911
[Merged by Bors] - feat(CategoryTheory/SmallObject): the functorial factorization#21911
Conversation
…sitionOfShape.lean
…ansfinite-compositions-misc
…sitionOfShape.lean
…nto small-object-iscardinal
PR summary 3b266fe1ac
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument | 866 | 871 | +5 (+0.58%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument |
5 |
Declarations diff
+ functorialFactorizationData
+ hasFunctorialFactorization
+ hasRightLiftingProperty_πObj
+ instance (f : Arrow C) : IsIso ((ιIteration I κ).app f).right
+ instance {j₁ j₂ : κ.ord.toType} (φ : j₁ ⟶ j₂) (f : Arrow C) :
+ iterationFunctorMapSuccAppArrowIso
+ iterationFunctorMapSuccAppArrowIso_hom_left
+ iterationFunctorMapSuccAppArrowIso_hom_right_right_comp
+ iterationFunctorObjObjRightIso
+ iterationFunctorObjObjRightIso_ιIteration_app_right
+ iterationObjRightIso
+ llp_rlp_ιObj
+ obj
+ objMap
+ objMap_comp
+ objMap_id
+ prop_iterationFunctor_map_succ
+ relativeCellComplexιObj
+ relativeCellComplexιObjFObjSuccIso
+ retracts_transfiniteComposition_pushouts_coproducts_le_llp_rlp
+ retracts_transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp
+ rlp_πObj
+ transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp
+ transfiniteCompositionsOfShape_ιObj
+ transfiniteCompositions_pushouts_coproducts_le_llp_rlp
+ ιFunctorObj_eq
+ ιObj
+ ιObj_naturality
+ ιObj_πObj
+ πFunctorObj_eq
+ πObj
+ πObj_naturality
+ πObj_ιIteration_app_right
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).
|
This PR/issue depends on: |
The main results in the small object argument are obtained in this PR. If `I : MorphismProperty C` has a cardinal that is suitable for the small object argument, then any morphism in `C` can be factored functorialy as a morphism in `I.rlp.llp` followed by a morphism in `I.rlp`. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
The main results in the small object argument are obtained in this PR. If
I : MorphismProperty Chas a cardinal that is suitable for the small object argument, then any morphism inCcan be factored functorialy as a morphism inI.rlp.llpfollowed by a morphism inI.rlp.