Commit 2023-06-26 18:00 49b574e1

View on Github →

feat: port CategoryTheory.Monoidal.Bimod (#5490)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monoidal/Bimod.lean

added theorem Bimod.AssociatorBimod.hom_inv_id

added theorem Bimod.AssociatorBimod.hom_left_act_hom'

added theorem Bimod.AssociatorBimod.hom_right_act_hom'

added theorem Bimod.AssociatorBimod.inv_hom_id

added structure Bimod.Hom

added theorem Bimod.LeftUnitorBimod.hom_inv_id

added theorem Bimod.LeftUnitorBimod.hom_left_act_hom'

added theorem Bimod.LeftUnitorBimod.hom_right_act_hom'

added theorem Bimod.LeftUnitorBimod.inv_hom_id

added theorem Bimod.RightUnitorBimod.hom_inv_id

added theorem Bimod.RightUnitorBimod.hom_left_act_hom'

added theorem Bimod.RightUnitorBimod.hom_right_act_hom'

added theorem Bimod.RightUnitorBimod.inv_hom_id

added theorem Bimod.TensorBimod.actRight_one'

added theorem Bimod.TensorBimod.id_tensor_π_actLeft

added theorem Bimod.TensorBimod.left_assoc'

added theorem Bimod.TensorBimod.middle_assoc'

added theorem Bimod.TensorBimod.one_act_left'

added theorem Bimod.TensorBimod.right_assoc'

added theorem Bimod.TensorBimod.π_tensor_id_actRight

added def Bimod.comp

added theorem Bimod.comp_hom'

added theorem Bimod.comp_whisker_left_bimod

added theorem Bimod.comp_whisker_right_bimod

added def Bimod.forget

added theorem Bimod.hom_ext

added def Bimod.id'

added theorem Bimod.id_hom'

added theorem Bimod.id_whisker_left_bimod

added def Bimod.isoOfIso

added theorem Bimod.pentagon_bimod

added def Bimod.regular

added theorem Bimod.tensor_comp

added theorem Bimod.tensor_id

added theorem Bimod.triangle_bimod

added theorem Bimod.whisker_assoc_bimod

added theorem Bimod.whisker_exchange_bimod

added theorem Bimod.whisker_left_comp_bimod

added theorem Bimod.whisker_right_comp_bimod

added theorem Bimod.whisker_right_id_bimod

added structure Bimod

added theorem id_tensor_π_preserves_coequalizer_inv_colimMap_desc

added theorem id_tensor_π_preserves_coequalizer_inv_desc

added theorem π_tensor_id_preserves_coequalizer_inv_colimMap_desc

added theorem π_tensor_id_preserves_coequalizer_inv_desc