Commit 2024-03-01 18:37 8a40b522

View on Github →

feat(CategoryTheory/Monoidal): replace 𝟙 X ⊗ f with X ◁ f (#10912) We set id_tensorHom and tensorHom_id as simp lemmas. Partially extracted from #6307.

Estimated changes

Modified Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean

Modified Mathlib/CategoryTheory/Bicategory/SingleObj.lean

Modified Mathlib/CategoryTheory/Closed/Monoidal.lean

Modified Mathlib/CategoryTheory/Enriched/Basic.lean

Modified Mathlib/CategoryTheory/Monoidal/Bimod.lean

Modified Mathlib/CategoryTheory/Monoidal/Braided.lean

Modified Mathlib/CategoryTheory/Monoidal/Category.lean

deleted theorem CategoryTheory.MonoidalCategory.leftUnitor_conjugation

deleted theorem CategoryTheory.MonoidalCategory.leftUnitor_inv_naturality'

modified theorem CategoryTheory.MonoidalCategory.leftUnitor_inv_naturality

deleted theorem CategoryTheory.MonoidalCategory.leftUnitor_naturality'

deleted theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor'

added theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor

deleted theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor_inv'

added theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor_inv

deleted theorem CategoryTheory.MonoidalCategory.pentagon'

deleted theorem CategoryTheory.MonoidalCategory.pentagon_inv'

modified theorem CategoryTheory.MonoidalCategory.pentagon_inv

deleted theorem CategoryTheory.MonoidalCategory.rightUnitor_conjugation

deleted theorem CategoryTheory.MonoidalCategory.rightUnitor_inv_naturality'

deleted theorem CategoryTheory.MonoidalCategory.rightUnitor_naturality'

deleted theorem CategoryTheory.MonoidalCategory.rightUnitor_tensor'

deleted theorem CategoryTheory.MonoidalCategory.rightUnitor_tensor_inv'

deleted theorem CategoryTheory.MonoidalCategory.triangle'

deleted theorem CategoryTheory.MonoidalCategory.triangle_assoc_comp_left_inv'

deleted theorem CategoryTheory.MonoidalCategory.triangle_assoc_comp_right'

deleted theorem CategoryTheory.MonoidalCategory.triangle_assoc_comp_right_inv'

added theorem CategoryTheory.MonoidalCategory.triangle_assoc_comp_right_inv

Modified Mathlib/CategoryTheory/Monoidal/Center.lean

Modified Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean

added theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor'

deleted theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor

added theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor_inv'

deleted theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor_inv

deleted theorem CategoryTheory.MonoidalCategory.triangle_assoc_comp_right_inv

Modified Mathlib/CategoryTheory/Monoidal/CommMon_.lean

Modified Mathlib/CategoryTheory/Monoidal/End.lean

Modified Mathlib/CategoryTheory/Monoidal/Free/Basic.lean

Modified Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean

Modified Mathlib/CategoryTheory/Monoidal/Functor.lean

deleted theorem CategoryTheory.LaxMonoidalFunctor.associativity'

deleted theorem CategoryTheory.LaxMonoidalFunctor.associativity_inv'

deleted theorem CategoryTheory.LaxMonoidalFunctor.left_unitality'

deleted theorem CategoryTheory.LaxMonoidalFunctor.left_unitality_inv'

deleted theorem CategoryTheory.LaxMonoidalFunctor.right_unitality'

deleted theorem CategoryTheory.LaxMonoidalFunctor.right_unitality_inv'

deleted theorem CategoryTheory.LaxMonoidalFunctor.μ_natural_left'

deleted theorem CategoryTheory.LaxMonoidalFunctor.μ_natural_right'

deleted theorem CategoryTheory.MonoidalFunctor.map_whiskerLeft'

deleted theorem CategoryTheory.MonoidalFunctor.map_whiskerRight'

Modified Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean

Modified Mathlib/CategoryTheory/Monoidal/Functorial.lean

Modified Mathlib/CategoryTheory/Monoidal/Limits.lean

Modified Mathlib/CategoryTheory/Monoidal/Linear.lean

Modified Mathlib/CategoryTheory/Monoidal/Mon_.lean

Modified Mathlib/CategoryTheory/Monoidal/Opposite.lean

Modified Mathlib/CategoryTheory/Monoidal/Preadditive.lean

Modified Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean

Modified Mathlib/CategoryTheory/Monoidal/Rigid/OfEquivalence.lean

Modified Mathlib/CategoryTheory/Monoidal/Transport.lean

Modified Mathlib/CategoryTheory/Monoidal/Types/Coyoneda.lean

Modified Mathlib/RepresentationTheory/Action/Monoidal.lean