Commit 2024-06-01 00:00 20b1e82e

View on Github →

feat(CategoryTheory/Monoidal/Bimon): definition of bimonoid object in a braided category (#12970)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monoidal/Bimon_.lean

added theorem Bimon_.comp_hom'

added def Bimon_.equivMon_Comon_

added theorem Bimon_.ext

added def Bimon_.forget

added theorem Bimon_.id_hom'

added def Bimon_.ofMon_Comon_

added def Bimon_.ofMon_Comon_obj

added def Bimon_.toComon_

added theorem Bimon_.toComon_forget

added def Bimon_.toMon_Comon_

added def Bimon_.toMon_Comon_obj

added theorem Bimon_.toMon_forget

added def Bimon_

Modified Mathlib/CategoryTheory/Monoidal/Comon_.lean

added def Comon_.forgetMonoidal

added theorem Comon_.forgetMonoidal_toFunctor

added theorem Comon_.forgetMonoidal_ε

added theorem Comon_.forgetMonoidal_μ

modified def Comon_.mkIso

Modified Mathlib/CategoryTheory/Monoidal/Functor.lean

Modified Mathlib/CategoryTheory/Monoidal/Mon_.lean

deleted def Mon_.isoOfIso

added def Mon_.mkIso

added theorem Mon_.tensorObj_mul

added theorem Mon_.tensorObj_one

added theorem Mon_.tensorUnit_mul

added theorem Mon_.tensorUnit_one

Modified Mathlib/CategoryTheory/Opposites.lean

added theorem Quiver.Hom.unop_op'