Skip to content

[Merged by Bors] - feat(CategoryTheory/Monoidal): Day's reflection theorem#15894

Closed
dagurtomas wants to merge 22 commits intomasterfrom
dagur/DayReflection
Closed

[Merged by Bors] - feat(CategoryTheory/Monoidal): Day's reflection theorem#15894
dagurtomas wants to merge 22 commits intomasterfrom
dagur/DayReflection

Conversation

@dagurtomas
Copy link
Copy Markdown
Contributor

@dagurtomas dagurtomas commented Aug 16, 2024

Open in Gitpod

@dagurtomas dagurtomas added the WIP Work in progress label Aug 16, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 16, 2024 •
edited
Loading

PR summary e64d6e3014

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.CategoryTheory.Monoidal.Braided.Reflection 445

Declarations diff

+ closed
+ instance (c : C) (d : D) : IsIso (adj.unit.app ((ihom d).obj (R.obj c))) := by
+ instance (d d' : D) : IsIso (L.map ((adj.unit.app d) ⊗ (adj.unit.app d'))) := by
+ isIso_iff_coyoneda_map_bijective
+ isIso_iff_isIso_coyoneda_map
+ isIso_iff_isIso_yoneda_map
+ isIso_iff_yoneda_map_bijective
+ isIso_tfae
+ isSplitEpi_iff_isIso_counit
+ isSplitMono_iff_isIso_unit
+ map_counit_app
+ map_unit_app
+ monoidalClosed

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.

@dagurtomas dagurtomas changed the title feat(CategoryTheory/Monoidal): pull back a closed symmetric monoidal structure along a reflective inclusion feat(CategoryTheory/Monoidal): Day's reflection theorem Aug 18, 2024
@dagurtomas dagurtomas added t-category-theory Category theory WIP Work in progress and removed WIP Work in progress labels Aug 18, 2024
@dagurtomas dagurtomas removed the WIP Work in progress label Aug 18, 2024
@dagurtomas dagurtomas requested a review from sinhp August 18, 2024 23:20
joelriou
joelriou reviewed Aug 19, 2024
View reviewed changes
jcommelin
jcommelin reviewed Aug 27, 2024
View reviewed changes
@jcommelin jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 27, 2024
@dagurtomas dagurtomas removed the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 28, 2024
jcommelin
jcommelin reviewed Oct 26, 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 Oct 26, 2024

✌️ dagurtomas 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 Oct 26, 2024
@dagurtomas
Copy link
Copy Markdown
Contributor Author

dagurtomas commented Oct 26, 2024

Thanks!

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Oct 26, 2024
@dagurtomas
feat(CategoryTheory/Monoidal): Day's reflection theorem (#15894)
90646da
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 26, 2024

Build failed:

@dagurtomas
Copy link
Copy Markdown
Contributor Author

dagurtomas commented Oct 27, 2024

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Oct 27, 2024
@dagurtomas
feat(CategoryTheory/Monoidal): Day's reflection theorem (#15894)
7e4aaba
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 27, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(CategoryTheory/Monoidal): Day's reflection theorem [Merged by Bors] - feat(CategoryTheory/Monoidal): Day's reflection theorem Oct 27, 2024
@mathlib-bors mathlib-bors bot closed this Oct 27, 2024
@mathlib-bors mathlib-bors bot deleted the dagur/DayReflection branch October 27, 2024 10:42
@joelriou joelriou mentioned this pull request Oct 29, 2024
Closed
1 task
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

@joelriou joelriou joelriou left review comments

@sinhp sinhp Awaiting requested review from sinhp

Assignees

No one assigned

Labels

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

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@dagurtomas @jcommelin @joelriou