Commit 2023-06-02 10:22 b265a524

View on Github →

feat: port CategoryTheory.Monoidal.Braided (#4560)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monoidal/Braided.lean

added def CategoryTheory.BraidedFunctor.comp

added theorem CategoryTheory.BraidedFunctor.comp_toNatTrans

added def CategoryTheory.BraidedFunctor.id

added def CategoryTheory.BraidedFunctor.mkIso

added def CategoryTheory.BraidedFunctor.toLaxBraidedFunctor

added structure CategoryTheory.BraidedFunctor

added def CategoryTheory.Discrete.braidedFunctor

added def CategoryTheory.LaxBraidedFunctor.comp

added theorem CategoryTheory.LaxBraidedFunctor.comp_toNatTrans

added def CategoryTheory.LaxBraidedFunctor.id

added def CategoryTheory.LaxBraidedFunctor.mkIso

added structure CategoryTheory.LaxBraidedFunctor

added theorem CategoryTheory.associator_monoidal

added theorem CategoryTheory.associator_monoidal_aux

added def CategoryTheory.braidedCategoryOfFaithful

added theorem CategoryTheory.braiding_leftUnitor

added theorem CategoryTheory.braiding_leftUnitor_aux₁

added theorem CategoryTheory.braiding_leftUnitor_aux₂

added theorem CategoryTheory.braiding_rightUnitor

added theorem CategoryTheory.braiding_rightUnitor_aux₁

added theorem CategoryTheory.braiding_rightUnitor_aux₂

added theorem CategoryTheory.leftUnitor_inv_braiding

added theorem CategoryTheory.leftUnitor_monoidal

added theorem CategoryTheory.rightUnitor_inv_braiding

added theorem CategoryTheory.rightUnitor_monoidal

added def CategoryTheory.symmetricCategoryOfFaithful

added def CategoryTheory.tensorMonoidal

added theorem CategoryTheory.tensor_associativity

added theorem CategoryTheory.tensor_associativity_aux

added theorem CategoryTheory.tensor_left_unitality

added theorem CategoryTheory.tensor_right_unitality

added def CategoryTheory.tensor_μ

added theorem CategoryTheory.tensor_μ_def₁

added theorem CategoryTheory.tensor_μ_def₂

added theorem CategoryTheory.tensor_μ_natural

Modified Mathlib/Tactic/CategoryTheory/Coherence.lean