Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

refactor(CategoryTheory/Monoidal): add whiskering operators #6307

Open
wants to merge 79 commits into
base: master
Choose a base branch
from
Open

refactor(CategoryTheory/Monoidal): add whiskering operators #6307

wants to merge 79 commits into from

Conversation

yuma-mizuno
Copy link
Collaborator

@yuma-mizuno yuma-mizuno commented Aug 2, 2023 •
edited

We introduce whiskering operators. This allows us to introduce a simp-normal form for morphisms in monoidal categories. Rewriting into simp-normal forms is especially useful when combined with the coherence tactic.

Open in Gitpod

@yuma-mizuno yuma-mizuno added the WIP Work in progress label Aug 2, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Aug 2, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Aug 3, 2023
@yuma-mizuno yuma-mizuno added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Aug 5, 2023
@yuma-mizuno yuma-mizuno changed the title refactor(CategoryTheory/Monoidal): whiskerings as fundamental refactor(CategoryTheory/Monoidal): add whiskering operators Aug 5, 2023
@semorrison semorrison added the t-category-theory Category theory label Aug 6, 2023
semorrison
semorrison reviewed Aug 6, 2023
View reviewed changes
Mathlib/CategoryTheory/Monoidal/Braided.lean Outdated
Comment on lines 548 to 554
calc
_ = 𝟙 _ ⊗≫
X₁ ◁ ((β_ X₂ Y₁).hom ▷ (Y₂ ⊗ Z₁) ≫ (Y₁ ⊗ X₂) ◁ (β_ Y₂ Z₁).hom) ▷ Z₂ ⊗≫
X₁ ◁ Y₁ ◁ (β_ X₂ Z₁).hom ▷ Y₂ ▷ Z₂ ⊗≫ 𝟙 _ := ?eq1
_ = _ := ?eq2
case eq1 => coherence
case eq2 => rw [← whisker_exchange]; coherence
Copy link
Contributor

Choose a reason for hiding this comment

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

My preference is not to use this ?eqn style, but to write the proofs inline in the calc block, at least when the proofs are as short as these ones.

I'm happy to use this technique for multiline proofs needed in a calc block, however.

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Mar 4, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Mar 7, 2024
@yuma-mizuno yuma-mizuno mentioned this pull request Mar 7, 2024
Closed
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Mar 7, 2024
mathlib-bors bot pushed a commit that referenced this pull request Mar 7, 2024
@yuma-mizuno
chore(CategoryTheory/Monoidal): replace 𝟙 X ⊗ f with X ◁ f (#11223)
ee3a8f2 
Extracted from #6307
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Mar 7, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Mar 7, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Mar 7, 2024
kbuzzard pushed a commit that referenced this pull request Mar 12, 2024
@yuma-mizuno @kbuzzard
feat(CategoryTheory/Monoidal): redefine tensorLeft by using whisker…
23f29f2 
…ing (#10898)

Extracted from #6307
kbuzzard pushed a commit that referenced this pull request Mar 12, 2024
@yuma-mizuno @kbuzzard
feat(CategoryTheory/Monoidal): replace 𝟙 X ⊗ f with X ◁ f (#10912)
f9b8d0f 
We set `id_tensorHom` and `tensorHom_id` as simp lemmas. Partially extracted from #6307.
kbuzzard pushed a commit that referenced this pull request Mar 12, 2024
@yuma-mizuno @kbuzzard
chore(CategoryTheory/Monoidal): replace 𝟙 X ⊗ f with X ◁ f (#11223)
6577655 
Extracted from #6307
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Mar 14, 2024
dagurtomas pushed a commit that referenced this pull request Mar 22, 2024
@yuma-mizuno @dagurtomas
feat(CategoryTheory/Monoidal): redefine tensorLeft by using whisker…
dd8dc22 
…ing (#10898)

Extracted from #6307
dagurtomas pushed a commit that referenced this pull request Mar 22, 2024
@yuma-mizuno @dagurtomas
feat(CategoryTheory/Monoidal): replace 𝟙 X ⊗ f with X ◁ f (#10912)
15acb55 
We set `id_tensorHom` and `tensorHom_id` as simp lemmas. Partially extracted from #6307.
dagurtomas pushed a commit that referenced this pull request Mar 22, 2024
@yuma-mizuno @dagurtomas
chore(CategoryTheory/Monoidal): replace 𝟙 X ⊗ f with X ◁ f (#11223)
a511ae4 
Extracted from #6307
utensil pushed a commit that referenced this pull request Mar 26, 2024
@yuma-mizuno @utensil
feat(CategoryTheory/Monoidal): redefine tensorLeft by using whisker…
0e30438 
…ing (#10898)

Extracted from #6307
utensil pushed a commit that referenced this pull request Mar 26, 2024
@yuma-mizuno @utensil
feat(CategoryTheory/Monoidal): replace 𝟙 X ⊗ f with X ◁ f (#10912)
5621cbd 
We set `id_tensorHom` and `tensorHom_id` as simp lemmas. Partially extracted from #6307.
utensil pushed a commit that referenced this pull request Mar 26, 2024
@yuma-mizuno @utensil
chore(CategoryTheory/Monoidal): replace 𝟙 X ⊗ f with X ◁ f (#11223)
907714c 
Extracted from #6307
@fpvandoorn fpvandoorn added the awaiting-author A reviewer has asked the author a question or requested changes label Apr 5, 2024
Louddy pushed a commit that referenced this pull request Apr 15, 2024
@yuma-mizuno @Louddy
feat(CategoryTheory/Monoidal): redefine tensorLeft by using whisker…
47f6cea 
…ing (#10898)

Extracted from #6307
Louddy pushed a commit that referenced this pull request Apr 15, 2024
@yuma-mizuno @Louddy
feat(CategoryTheory/Monoidal): replace 𝟙 X ⊗ f with X ◁ f (#10912)
06bdd3b 
We set `id_tensorHom` and `tensorHom_id` as simp lemmas. Partially extracted from #6307.
Louddy pushed a commit that referenced this pull request Apr 15, 2024
@yuma-mizuno @Louddy
chore(CategoryTheory/Monoidal): replace 𝟙 X ⊗ f with X ◁ f (#11223)
0c64b69 
Extracted from #6307
callesonne pushed a commit that referenced this pull request Apr 22, 2024
@yuma-mizuno @callesonne
chore(CategoryTheory/Monoidal): replace 𝟙 X ⊗ f with X ◁ f (#11223)
57ecf7e 
Extracted from #6307
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@semorrison semorrison semorrison left review comments

@jcommelin jcommelin jcommelin left review comments

@github-actions github-actions[bot] github-actions left review comments

@Shamrock-Frost Shamrock-Frost Awaiting requested review from Shamrock-Frost

Assignees
No one assigned
Labels
awaiting-author A reviewer has asked the author a question or requested changes merge-conflict The PR has a merge conflict with master, and needs manual merging. t-category-theory Category theory
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
7 participants
@yuma-mizuno @eric-wieser @grunweg @leanprover-community-mathlib4-bot @semorrison @jcommelin @fpvandoorn