[Merged by Bors] - feat(CategoryTheory): pullbacks/pushouts/limits/colimits of a class of morphisms by joelriou · Pull Request #20157 · leanprover-community/mathlib4

joelriou · 2024-12-21T14:35:16Z

Given P : MorphismProperty C and J a category, we introduce morphisms properties P.pullbacks, P.pushouts, P.limitsOfShape J and P.colimitsOfShape J which are obtained from P by taking these type of (co)limits. We obtain results like P.isStableUnderBaseChange_iff_pullbacks_le : P.IsStableUnderBaseChange ↔ P.pullbacks ≤ P.

…of morphisms

github-actions · 2024-12-21T14:36:06Z

PR summary fc37372887

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ IsStableUnderColimitsOfShape.colimMap
+ IsStableUnderColimitsOfShape.colimitsOfShape_le
+ IsStableUnderLimitsOfShape.limMap
+ IsStableUnderLimitsOfShape.limitsOfShape_le
+ colimitsOfShape
+ colimitsOfShape_colimMap
+ colimitsOfShape_le_coproducts
+ coproducts
+ coproducts_iff
+ iSup_iff
+ instance (priority := 900) IsStableUnderBaseChange.respectsIso
+ instance : (W.colimitsOfShape J).RespectsIso
+ instance : (W.limitsOfShape J).RespectsIso
+ instance : P.pullbacks.IsStableUnderBaseChange
+ instance : P.pullbacks.RespectsIso
+ instance : P.pushouts.IsStableUnderCobaseChange
+ instance : P.pushouts.RespectsIso
+ isStableUnderBaseChange_iff_pullbacks_le
+ isStableUnderCobaseChange_iff_pushouts_le
+ isStableUnderColimitsOfShape_iff_colimitsOfShape_le
+ isStableUnderLimitsOfShape_iff_limitsOfShape_le
+ le_pullbacks
+ le_pushouts
+ limitsOfShape
+ limitsOfShape_limMap
+ pullbacks
+ pullbacks_mk
+ pushouts
+ pushouts_mk
+ sSup_iff
- IsStableUnderColimitsOfShape.colim_map
- IsStableUnderLimitsOfShape.lim_map
- instance (priority := 900) IsStableUnderBaseChange.respectsIso {P : MorphismProperty 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 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).

Mathlib/CategoryTheory/MorphismProperty/Limits.lean

…operty-coproducts

TwoFX

Thanks!
bors r+

…f morphisms (#20157) Given `P : MorphismProperty C` and `J` a category, we introduce morphisms properties `P.pullbacks`, `P.pushouts`, `P.limitsOfShape J` and `P.colimitsOfShape J` which are obtained from `P` by taking these type of (co)limits. We obtain results like `P.isStableUnderBaseChange_iff_pullbacks_le : P.IsStableUnderBaseChange ↔ P.pullbacks ≤ P`. Co-authored-by: Jack McKoen <104791831+mckoen@users.noreply.github.com> Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr> Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

mathlib-bors · 2025-01-22T12:32:14Z

Build failed (retrying...):

Build

…f morphisms (#20157) Given `P : MorphismProperty C` and `J` a category, we introduce morphisms properties `P.pullbacks`, `P.pushouts`, `P.limitsOfShape J` and `P.colimitsOfShape J` which are obtained from `P` by taking these type of (co)limits. We obtain results like `P.isStableUnderBaseChange_iff_pullbacks_le : P.IsStableUnderBaseChange ↔ P.pullbacks ≤ P`. Co-authored-by: Jack McKoen <104791831+mckoen@users.noreply.github.com> Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr> Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

mathlib-bors · 2025-01-22T12:43:31Z

Build failed:

Build

TwoFX

bors r-

TwoFX · 2025-01-22T13:15:36Z

bors d+

mathlib-bors · 2025-01-22T13:15:39Z

✌️ 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.

joelriou · 2025-01-22T14:26:23Z

Thanks!

bors merge

…f morphisms (#20157) Given `P : MorphismProperty C` and `J` a category, we introduce morphisms properties `P.pullbacks`, `P.pushouts`, `P.limitsOfShape J` and `P.colimitsOfShape J` which are obtained from `P` by taking these type of (co)limits. We obtain results like `P.isStableUnderBaseChange_iff_pullbacks_le : P.IsStableUnderBaseChange ↔ P.pullbacks ≤ P`. Co-authored-by: mckoen <mckoen@ualberta.ca> Co-authored-by: Jack McKoen <mckoen@ualberta.ca> Co-authored-by: Jack McKoen <104791831+mckoen@users.noreply.github.com> Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

mathlib-bors · 2025-01-22T14:34:19Z

Pull request successfully merged into master.

Build succeeded:

mckoen and others added 16 commits November 16, 2024 13:32

initial

0609afa

tentative

482cc46

lint

858ec65

add to Mathlib.lean

0a21409

some feedback from joël, still wip

6090684

update

16793f7

golf

38be602

Merge branch 'master' into mckoen/lifting

18ba00e

fix imports

e496339

some of Joël's code review

c5451b1

Update Basic.lean

b521049

Update Basic.lean

86282af

add stable under products and coproducts

b21ab3a

update

0567596

add ascii

b06771c

feat(CategoryTheory): coproducts/pushouts/limits/colimits of a class …

4be350a

…of morphisms

joelriou added the t-category-theory Category theory label Dec 21, 2024

joelriou mentioned this pull request Dec 21, 2024

feat(CategoryTheory): the small object argument #20146

Closed

4 tasks

joelriou changed the title ~~feat(CategoryTheory): coproducts/pushouts/limits/colimits of a class of morphisms~~ feat(CategoryTheory): pullbacks/pushouts/limits/colimits of a class of morphisms Dec 21, 2024

joelriou and others added 2 commits December 21, 2024 15:41

fixing the build

b80d31b

update

28e54b5

joelriou commented Dec 21, 2024

View reviewed changes

Mathlib/CategoryTheory/MorphismProperty/Limits.lean Outdated Show resolved Hide resolved

joelriou and others added 5 commits December 21, 2024 22:19

Update Mathlib/CategoryTheory/MorphismProperty/Limits.lean

d9915e1

feedback

9b461dc

implement feedback

1e77b75

remove mk

da48574

oops, remove superfluous defns

2ee843a

joelriou mentioned this pull request Dec 21, 2024

[Merged by Bors] - feat(CategoryTheory): Grothendieck abelian categories have enough injectives #20079

Closed

20 tasks

joelriou added the WIP Work in progress label Dec 21, 2024

Merge remote-tracking branch 'origin/mckoen/lifting' into morphism-pr…

5a66ab9

…operty-coproducts

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Dec 22, 2024

Merge remote-tracking branch 'origin' into morphism-property-coproducts

a41fadf

github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Dec 22, 2024

joelriou added 4 commits December 22, 2024 17:00

Merge remote-tracking branch 'origin' into morphism-property-coproducts

5d62242

Merge remote-tracking branch 'origin' into morphism-property-coproducts

3b0911a

restored a lemma

8ea9b9c

better syntax

f7b7747

joelriou removed the WIP Work in progress label Dec 24, 2024

joelriou mentioned this pull request Dec 25, 2024

[Merged by Bors] - feat(CategoryTheory): the small object argument #20245

Closed

21 tasks

TwoFX approved these changes Jan 22, 2025

View reviewed changes

ghost added the ready-to-merge This PR has been sent to bors. label Jan 22, 2025

TwoFX reviewed Jan 22, 2025

View reviewed changes

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jan 22, 2025

joelriou added 2 commits January 22, 2025 14:59

Merge remote-tracking branch 'origin' into morphism-property-coproducts

8bc5dd8

fix

fc37372

mathlib-bors bot changed the title ~~feat(CategoryTheory): pullbacks/pushouts/limits/colimits of a class of morphisms~~ [Merged by Bors] - feat(CategoryTheory): pullbacks/pushouts/limits/colimits of a class of morphisms Jan 22, 2025

mathlib-bors bot closed this Jan 22, 2025

mathlib-bors bot deleted the morphism-property-coproducts branch January 22, 2025 14:34

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(CategoryTheory): pullbacks/pushouts/limits/colimits of a class of morphisms#20157

[Merged by Bors] - feat(CategoryTheory): pullbacks/pushouts/limits/colimits of a class of morphisms#20157
joelriou wants to merge 31 commits intomasterfrom
morphism-property-coproducts

joelriou commented Dec 21, 2024 •

edited

Loading

Uh oh!

github-actions bot commented Dec 21, 2024 •

edited

Loading

Declarations diff

Uh oh!

Uh oh!

TwoFX left a comment

Uh oh!

mathlib-bors bot commented Jan 22, 2025

Uh oh!

mathlib-bors bot commented Jan 22, 2025

Uh oh!

TwoFX left a comment

Uh oh!

TwoFX commented Jan 22, 2025

Uh oh!

mathlib-bors bot commented Jan 22, 2025

Uh oh!

joelriou commented Jan 22, 2025

Uh oh!

mathlib-bors bot commented Jan 22, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

joelriou commented Dec 21, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Dec 21, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary fc37372887

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

TwoFX left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Jan 22, 2025

Uh oh!

mathlib-bors bot commented Jan 22, 2025

Uh oh!

TwoFX left a comment

Choose a reason for hiding this comment

Uh oh!

TwoFX commented Jan 22, 2025

Uh oh!

mathlib-bors bot commented Jan 22, 2025

Uh oh!

joelriou commented Jan 22, 2025

Uh oh!

mathlib-bors bot commented Jan 22, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

joelriou commented Dec 21, 2024 •

edited

Loading

github-actions bot commented Dec 21, 2024 •

edited

Loading