[Merged by Bors] - refactor(CategoryTheory/Monoidal/Braided): use monoidalComp in the proofs#10078
[Merged by Bors] - refactor(CategoryTheory/Monoidal/Braided): use monoidalComp in the proofs#10078yuma-mizuno wants to merge 9 commits intomasterfrom
Conversation
|
This PR/issue depends on: |
| #align category_theory.braiding_left_unitor_aux₂ CategoryTheory.braiding_leftUnitor_aux₂ | ||
|
|
||
| @[simp] | ||
| theorem braiding_leftUnitor (X : C) : (β_ X (𝟙_ C)).hom ≫ (λ_ X).hom = (ρ_ X).hom := by |
There was a problem hiding this comment.
We could add the reassoc attribute here.
| theorem braiding_rightUnitor (X : C) : (β_ (𝟙_ C) X).hom ≫ (ρ_ X).hom = (λ_ X).hom := by | ||
| rw [← tensor_left_iff, id_tensor_comp, braiding_rightUnitor_aux₂] | ||
| rw [← whiskerLeft_iff, MonoidalCategory.whiskerLeft_comp, braiding_rightUnitor_aux₂] | ||
| #align category_theory.braiding_right_unitor CategoryTheory.braiding_rightUnitor | ||
|
|
||
| @[simp] | ||
| theorem braiding_tensorUnit_left (X : C) : (β_ (𝟙_ C) X).hom = (λ_ X).hom ≫ (ρ_ X).inv := by | ||
| simp [← braiding_rightUnitor] | ||
|
|
||
| theorem leftUnitor_inv_braiding (X : C) : (λ_ X).inv ≫ (β_ (𝟙_ C) X).hom = (ρ_ X).inv := by | ||
| apply (cancel_mono (ρ_ X).hom).1 | ||
| simp only [assoc, braiding_rightUnitor, Iso.inv_hom_id] | ||
| simp | ||
| #align category_theory.left_unitor_inv_braiding CategoryTheory.leftUnitor_inv_braiding | ||
|
|
||
| @[simp] | ||
| theorem rightUnitor_inv_braiding (X : C) : (ρ_ X).inv ≫ (β_ X (𝟙_ C)).hom = (λ_ X).inv := by |
There was a problem hiding this comment.
These lemmas braiding_rightUnitor, braiding_tensorUnit_left, leftUnitor_inv_braiding and rightUnitor_inv_braiding should have the reassoc attr, as well as braiding_tensorUnit_right below.
| by dsimp [tensor_μ]; simp | ||
| #align category_theory.tensor_μ_def₂ CategoryTheory.tensor_μ_def₂ | ||
|
|
||
| theorem tensor_μ_natural {X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : U₁ ⟶ V₁) |
There was a problem hiding this comment.
reassoc could be useful here also.
| tensor_μ C (Z₁, Z₂) (X₁, X₂) ≫ (Z₁ ◁ f₁ ⊗ Z₂ ◁ f₂) := by | ||
| convert tensor_μ_natural C (𝟙 Z₁) (𝟙 Z₂) f₁ f₂ using 1 <;> simp | ||
|
|
||
| theorem tensor_left_unitality (X₁ X₂ : C) : |
There was a problem hiding this comment.
reassoc should also be added to lemmas tensor_left_unitality, tensor_right_unitality, tensor_associativity, leftUnitor_monoidal, rightUnitor_monoidal, associator_monoidal.
There was a problem hiding this comment.
Adding reassoc to tensor_associativity and associator_monoidal seems to give errors unless we increase the maxHeartbeats. Do you think it's OK to do this, or should we postpone adding reassoc until some optimization is done?
There was a problem hiding this comment.
Adding the line attribute [reassoc] tensor_associativity associator_monoidal after the declarations seem to work without increasing maxHeartbeats.
| f ≫ (λ_ Y).inv = (λ_ X).inv ≫ (_ ◁ f) := by simp | ||
| f ≫ (λ_ Y).inv = (λ_ X).inv ≫ _ ◁ f := by simp | ||
|
|
||
| theorem id_whiskerLeft_symm {X X' : C} (f : X ⟶ X') : |
There was a problem hiding this comment.
reassoc can be added to id_whiskerLeft_symm and whiskerRight_id_symm
joelriou
left a comment
There was a problem hiding this comment.
Thanks for this great work! Apart from the reassoc attribute which shoud be added to some lemmas, this looks good to me.
|
Thanks! bors merge |
|
Pull request successfully merged into master. Build succeeded: |
Uh oh!
There was an error while loading. Please reload this page.