Commit 2024-05-23 18:22 7f5ae31c

View on Github →

feat: comonoid objects in a braided category form a monoidal category (#10098)

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Comon_.lean

added def Comon_.Comon_EquivMon_OpOp

added def Comon_.Comon_ToMon_OpOp

added def Comon_.Comon_ToMon_OpOp_obj'

deleted def Comon_.Comon_equiv_Mon_op_op

deleted def Comon_.Comon_to_Mon_op_op

deleted def Comon_.Comon_to_Mon_op_op_obj

added def Comon_.Mon_OpOpToComon_

added def Comon_.Mon_OpOpToComon_obj'

deleted def Comon_.Mon_op_op_to_Comon

deleted def Comon_.Mon_op_op_to_Comon_obj

added theorem Comon_.tensorObj_X

added theorem Comon_.tensorObj_comul'

added theorem Comon_.tensorObj_comul

added theorem Comon_.tensorObj_counit

Modified Mathlib/CategoryTheory/Opposites.lean

added theorem Quiver.Hom.unop_mk