Skip to content

[Merged by Bors] - feat(CategoryTheory): the category of commutative squares#14969

Closed
joelriou wants to merge 6 commits intomasterfrom
category-theory-square
Closed

[Merged by Bors] - feat(CategoryTheory): the category of commutative squares#14969
joelriou wants to merge 6 commits intomasterfrom
category-theory-square

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Jul 21, 2024 •
edited
Loading

In this PR, we define a bundled version of CommSq which allows to consider commutative squares as objects in a category Square 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 3e211eba44

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.CategoryTheory.Square 272

Declarations diff

+ Hom
+ Square
+ arrowArrowEquivalence
+ arrowArrowEquivalence'
+ category
+ commSq
+ comp
+ flip
+ flipEquivalence
+ flipFunctor
+ fromArrowArrowFunctor
+ fromArrowArrowFunctor'
+ hom_ext
+ id
+ isoMk
+ toArrowArrowFunctor
+ toArrowArrowFunctor'

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>

This was referenced Jul 21, 2024
Closed
Closed
Closed
@joelriou joelriou mentioned this pull request Jul 21, 2024
Closed
1 task
erdOne
erdOne approved these changes Jul 21, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@erdOne erdOne left a comment

Choose a reason for hiding this comment

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

I was just thinking about suggesting the same thing when I saw the other PR.
LGTM modulo minor comments.

joelriou and others added 3 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
Copy link
Copy Markdown
Contributor Author

joelriou commented Jul 21, 2024

Thanks for the reviews @erdOne! Indeed, while finding the better way to formalize Mayer-Vietoris squares, it has become more obvious to me that introducing this category Square C was the better approach.

@erdOne
Copy link
Copy Markdown
Member

erdOne commented Jul 21, 2024

Thanks!
maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 21, 2024

🚀 Pull request has been placed on the maintainer queue by erdOne.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jul 21, 2024
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca 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): the category of commutative squares (#14969)
6a18101 
In this PR, we define a bundled version of `CommSq` which allows to consider commutative squares as objects in a category `Square 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): the category of commutative squares [Merged by Bors] - feat(CategoryTheory): the category of commutative squares Jul 21, 2024
@mathlib-bors mathlib-bors bot closed this Jul 21, 2024
@mathlib-bors mathlib-bors bot deleted the category-theory-square branch July 21, 2024 12:55
@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

@erdOne erdOne erdOne approved these changes

Assignees

No one assigned

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. 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 @erdOne @riccardobrasca