Skip to content

[Merged by Bors] - feat(CategoryTheory): commutative squares that are pushout or pullback squares#14971

Closed
joelriou wants to merge 12 commits intomasterfrom
category-theory-square-limits
Closed

[Merged by Bors] - feat(CategoryTheory): commutative squares that are pushout or pullback squares#14971
joelriou wants to merge 12 commits intomasterfrom
category-theory-square-limits

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Jul 21, 2024 •
edited by kim-em
Loading

In this PR, we translate the IsPushout/IsPullback API for the objects of the category Square C of commutative squares in a category C.

Open in Gitpod

@joelriou joelriou added the t-category-theory Category theory label Jul 21, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 21, 2024 •
edited
Loading

PR summary 7c161b93ea

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square 534

Declarations diff

+ IsPullback
+ IsPullback.iff_of_iso
+ IsPullback.isLimit
+ IsPullback.mk
+ IsPullback.of_iso
+ IsPushout
+ IsPushout.iff_of_iso
+ IsPushout.isColimit
+ IsPushout.mk
+ IsPushout.of_iso
+ evaluation₁
+ evaluation₂
+ evaluation₃
+ evaluation₄
+ isPullback_iff
+ isPushout_iff

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>

@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 21, 2024
joelriou and others added 4 commits July 21, 2024 16:23
@joelriou @erdOne
Update Mathlib/CategoryTheory/Square.lean
e08550d 
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
@joelriou @erdOne
Update Mathlib/CategoryTheory/Square.lean
b88854c 
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
@joelriou
fixed asciiart
3e211eb
@joelriou
Merge remote-tracking branch 'origin/category-theory-square' into cat…
17bb707 
…egory-theory-square-limits
@joelriou joelriou mentioned this pull request Jul 21, 2024
Closed
2 tasks
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 21, 2024
@ghost
Copy link
Copy Markdown

ghost commented Jul 21, 2024

This PR/issue depends on:

@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 21, 2024
kim-em
kim-em reviewed Jul 21, 2024
View reviewed changes
kim-em
kim-em reviewed Jul 21, 2024
View reviewed changes
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Jul 21, 2024

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 21, 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.

@github-actions github-actions bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jul 21, 2024
@joelriou joelriou added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Jul 21, 2024
@joelriou joelriou mentioned this pull request Jul 21, 2024
Closed
3 tasks
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jul 21, 2024
@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Jul 21, 2024

Thanks!

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Jul 21, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 21, 2024
@joelriou
feat(CategoryTheory): commutative squares that are pushout or pullbac…
aaa0f40 
…k squares (#14971)

In this PR, we translate the `IsPushout/IsPullback` API for the objects of the category `Square C` of commutative squares in a category `C`.



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

mathlib-bors bot commented Jul 21, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(CategoryTheory): commutative squares that are pushout or pullback squares [Merged by Bors] - feat(CategoryTheory): commutative squares that are pushout or pullback squares Jul 21, 2024
@mathlib-bors mathlib-bors bot closed this Jul 21, 2024
@mathlib-bors mathlib-bors bot deleted the category-theory-square-limits branch July 21, 2024 16:20
@adomani adomani mentioned this pull request Aug 1, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em kim-em 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.

2 participants

@joelriou @kim-em