Skip to content

[Merged by Bors] - feat(CategoryTheory/SmallObject/Iteration): existence of objects (bot and succ cases)#19047

Closed
joelriou wants to merge 23 commits intomasterfrom
small-object-7
Closed

[Merged by Bors] - feat(CategoryTheory/SmallObject/Iteration): existence of objects (bot and succ cases)#19047
joelriou wants to merge 23 commits intomasterfrom
small-object-7

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Nov 14, 2024 •
edited
Loading

joelriou and others added 19 commits October 23, 2024 15:50
@joelriou
feat(CategoryTheory/SmallObject): very basic API for the iteration of…
b5c4880 
… functors
@joelriou
feat(CategoryTheory/SmallObject): construction of a morphism between …
73f3517 
…iterations of functors in two cases
@joelriou @github-actions
Update Mathlib.lean
9a2e020 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@joelriou
fix Mathlib.lean
f497043
@joelriou
feat(CategoryTheory/SmallObject/Iteration): the unique morphism (limi…
46bf440 
…t case)
@joelriou
Merge remote-tracking branch 'origin' into small-object-4
ba501fa
@joelriou
fixes, using interval notation
295d8df
@joelriou
Merge remote-tracking branch 'origin/small-object-4' into small-object-5
8d33372
@joelriou
fix
26405bd
@joelriou
Merge remote-tracking branch 'origin/small-object-5' into small-object-6
c60220e
@joelriou @alreadydone
Update Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
ecdbc60 
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
@joelriou
Merge remote-tracking branch 'origin' into small-object-5
0ed84bf
@joelriou
Merge remote-tracking branch 'origin/small-object-5' into small-object-6
9a446f2
@joelriou
fix
64c0674
@joelriou
fix
6d4fc10
@joelriou
Merge remote-tracking branch 'origin/small-object-5' into small-object-6
bb49cdf
@joelriou
Merge remote-tracking branch 'origin' into small-object-6
3d76917
@joelriou
s/refine/exact/
f8a7628
@joelriou
wip
3398597
@joelriou joelriou added WIP Work in progress t-category-theory Category theory labels Nov 14, 2024
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Nov 14, 2024
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Nov 14, 2024

This PR/issue depends on:

@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 19, 2024 •
edited
Loading

PR summary 5f04722491

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc (new file) 425
Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty (new file) 426

Declarations diff

+ extendToSucc
+ extendToSuccObjIso
+ extendToSuccObjIso_hom_naturality
+ extendToSuccObjSuccIso
+ extendToSuccRestrictionLEIso
+ extendToSucc_map_le_succ
+ extentToSucc_map
+ map
+ map_comp
+ map_eq
+ map_id
+ map_self_succ
+ mkOfBot
+ mkOfSucc
+ obj
+ objIso
+ objSuccIso

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) = (2.00, 0.00)
Current number Change Type
1551 2 erw

Current commit 5f04722491
Reference commit 22229e91bb

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

@joelriou joelriou removed the WIP Work in progress label Nov 19, 2024
@joelriou joelriou mentioned this pull request Nov 19, 2024
Closed
2 tasks
jcommelin
jcommelin reviewed Nov 28, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 28, 2024

✌️ 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 Nov 28, 2024
@joelriou @jcommelin
Update Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean
5f04722 
Co-authored-by: Johan Commelin <johan@commelin.net>
@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Nov 30, 2024

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Nov 30, 2024
mathlib-bors bot pushed a commit that referenced this pull request Nov 30, 2024
@joelriou
feat(CategoryTheory/SmallObject/Iteration): existence of objects (bot…
c73ab4c 
… and succ cases) (#19047)

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 30, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(CategoryTheory/SmallObject/Iteration): existence of objects (bot and succ cases) [Merged by Bors] - feat(CategoryTheory/SmallObject/Iteration): existence of objects (bot and succ cases) Nov 30, 2024
@mathlib-bors mathlib-bors bot closed this Nov 30, 2024
@mathlib-bors mathlib-bors bot deleted the small-object-7 branch November 30, 2024 09:15
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

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 @jcommelin