Commit 2024-02-29 02:01 13e13156

View on Github →

feat(CategoryTheory/Monoidal): redefine tensorLeft by using whiskering (#10898) Extracted from #6307

Estimated changes

Modified Mathlib/CategoryTheory/Closed/FunctorCategory.lean

Modified Mathlib/CategoryTheory/Closed/Monoidal.lean

modified theorem CategoryTheory.MonoidalClosed.curry_natural_left

modified theorem CategoryTheory.MonoidalClosed.uncurry_eq

modified theorem CategoryTheory.ihom.ev_coev

Modified Mathlib/CategoryTheory/Monoidal/Bimod.lean

modified theorem Bimod.TensorBimod.actRight_one'

deleted theorem Bimod.TensorBimod.id_tensor_π_actLeft

modified theorem Bimod.TensorBimod.one_act_left'

added theorem Bimod.TensorBimod.whiskerLeft_π_actLeft

added theorem Bimod.comp_whiskerLeft_bimod

added theorem Bimod.comp_whiskerRight_bimod

deleted theorem Bimod.comp_whisker_left_bimod

deleted theorem Bimod.comp_whisker_right_bimod

added theorem Bimod.id_whiskerLeft_bimod

added theorem Bimod.id_whiskerRight_bimod

deleted theorem Bimod.id_whisker_left_bimod

deleted theorem Bimod.tensor_comp

deleted theorem Bimod.tensor_id

added theorem Bimod.whiskerLeft_comp_bimod

added theorem Bimod.whiskerLeft_id_bimod

added theorem Bimod.whiskerRight_comp_bimod

added theorem Bimod.whiskerRight_id_bimod

deleted theorem Bimod.whisker_left_comp_bimod

deleted theorem Bimod.whisker_right_comp_bimod

deleted theorem Bimod.whisker_right_id_bimod

Modified Mathlib/CategoryTheory/Monoidal/Category.lean

Modified Mathlib/CategoryTheory/Monoidal/Functor.lean

Modified Mathlib/CategoryTheory/Monoidal/Linear.lean

Modified Mathlib/CategoryTheory/Monoidal/Preadditive.lean

added theorem CategoryTheory.sum_whiskerRight

added theorem CategoryTheory.whiskerLeft_sum

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