Skip to content

[Merged by Bors] - feat(CategoryTheory): cardinals that are suitable for the small object argument#21865

Closed
joelriou wants to merge 21 commits intomasterfrom
small-object-iscardinal
Closed

[Merged by Bors] - feat(CategoryTheory): cardinals that are suitable for the small object argument#21865
joelriou wants to merge 21 commits intomasterfrom
small-object-iscardinal

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Feb 14, 2025 •
edited
Loading

In this PR, we package the technical assumptions that are needed for the small object argument in a typeclass IsCardinalForSmallObjectArgument I κ where I is a class of morphisms and κ is a suitable regular cardinal. In a follow-up PR, it shall be proved that HasFunctorialFactorization I.rlp.llp I.rlp holds.

Open in Gitpod

@joelriou joelriou added WIP Work in progress t-category-theory Category theory labels Feb 14, 2025
@joelriou joelriou mentioned this pull request Feb 14, 2025
Closed
21 tasks
@github-actions github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Feb 14, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Feb 14, 2025 •
edited
Loading

PR summary bd62451491

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument (new file) 865

Declarations diff

+ IsCardinalForSmallObjectArgument
+ attachCellsOfSuccStructProp
+ attachCellsιFunctorObjOfSmall
+ functorObj_isPushout
+ hasColimitsOfShape_discrete
+ hasCoproducts
+ hasIterationOfShape
+ hasPushouts
+ instance (o : Ordinal) : SuccOrder o.toType
+ instance : Small.{t} (FunctorObjIndex f πX) := by
+ instance : Small.{t} (attachCellsιFunctorObj f πX).ι := by
+ isSmall
+ iteration
+ iterationFunctor
+ locallySmall
+ preservesColimit
+ prop.arrowIso
+ propArrow
+ succStruct
+ succStruct_prop_le_propArrow
+ transfiniteCompositionOfShapeSuccStructPropιIteration
+ transfiniteCompositionOfShapeSuccStructPropιIteration_F
+ transfiniteCompositionOfShapeιIterationAppRight
+ ιFunctorObj_extension'
+ ιIteration

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.

Increase in tech debt: (relative, absolute) = (1.00, 0.02)
Current number Change Type
43 1 large files

Current commit bd62451491
Reference commit 3bc2081fd5

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 mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 14, 2025
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 15, 2025
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Feb 15, 2025

This PR/issue depends on:

@joelriou joelriou removed the WIP Work in progress label Feb 15, 2025
TwoFX
TwoFX approved these changes Feb 15, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@TwoFX TwoFX left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!
bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 15, 2025

✌️ joelriou can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Feb 15, 2025
@github-actions github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Feb 15, 2025
@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Feb 15, 2025

Thanks!

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Feb 15, 2025
mathlib-bors bot pushed a commit that referenced this pull request Feb 15, 2025
@joelriou
feat(CategoryTheory): cardinals that are suitable for the small objec…
38f496f 
…t argument (#21865)

In this PR, we package the technical assumptions that are needed for the small object argument in a typeclass `IsCardinalForSmallObjectArgument I κ` where `I` is a class of morphisms and `κ` is a suitable regular cardinal. In a follow-up PR, it shall be proved that `HasFunctorialFactorization I.rlp.llp I.rlp` holds.



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
@joelriou joelriou mentioned this pull request Feb 15, 2025
Closed
1 task
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 15, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(CategoryTheory): cardinals that are suitable for the small object argument [Merged by Bors] - feat(CategoryTheory): cardinals that are suitable for the small object argument Feb 15, 2025
@mathlib-bors mathlib-bors bot closed this Feb 15, 2025
@mathlib-bors mathlib-bors bot deleted the small-object-iscardinal branch February 15, 2025 13:36
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@TwoFX TwoFX TwoFX approved these changes

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors. t-category-theory Category theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@joelriou @mathlib4-dependent-issues-bot @TwoFX