Commit 2023-06-12 09:24 1ab969a0

View on Github →

feat: port CategoryTheory.Monoidal.Center (#4941)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monoidal/Center.lean

added structure CategoryTheory.Center.Hom

added def CategoryTheory.Center.associator

added theorem CategoryTheory.Center.associator_hom_f

added theorem CategoryTheory.Center.associator_inv_f

added def CategoryTheory.Center.braiding

added theorem CategoryTheory.Center.comp_f

added theorem CategoryTheory.Center.ext

added def CategoryTheory.Center.forget

added theorem CategoryTheory.Center.id_f

added def CategoryTheory.Center.isoMk

added def CategoryTheory.Center.leftUnitor

added theorem CategoryTheory.Center.leftUnitor_hom_f

added theorem CategoryTheory.Center.leftUnitor_inv_f

added def CategoryTheory.Center.ofBraided

added def CategoryTheory.Center.ofBraidedObj

added def CategoryTheory.Center.rightUnitor

added theorem CategoryTheory.Center.rightUnitor_hom_f

added theorem CategoryTheory.Center.rightUnitor_inv_f

added def CategoryTheory.Center.tensorHom

added def CategoryTheory.Center.tensorObj

added def CategoryTheory.Center.tensorUnit

added theorem CategoryTheory.Center.tensorUnit_β

added theorem CategoryTheory.Center.tensor_f

added theorem CategoryTheory.Center.tensor_fst

added theorem CategoryTheory.Center.tensor_β

added def CategoryTheory.Center

added structure CategoryTheory.HalfBraiding