Commit 2026-09-30 10:44 851d2845

View on Github →

feat(CategoryTheory): express monoidal pentagons using quadrifunctors (#43008) Expresses the monoidal pentagon and triangle as equalities of natural transformations between quadrifunctors and bifunctors, and adds a corresponding MonoidalCategory.ofBifunctor constructor. This resolves the quadrifunctor API TODO in Mathlib/CategoryTheory/Monoidal/Multifunctor.lean.

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Multifunctor.lean

deleted def CategoryTheory.Functor.LaxMonoidal.CoreMonoidal.ofBifunctor

deleted def CategoryTheory.Functor.LaxMonoidal.Monoidal.ofBifunctor

deleted def CategoryTheory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.bottomMapᵣ

deleted def CategoryTheory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.bottomMapₗ

deleted def CategoryTheory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.firstMap

deleted def CategoryTheory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.firstMap₁

deleted def CategoryTheory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.firstMap₂

deleted def CategoryTheory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.firstMap₃

deleted def CategoryTheory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.leftMapᵣ

deleted def CategoryTheory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.leftMapₗ

deleted def CategoryTheory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.secondMap

deleted def CategoryTheory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.secondMap₁

deleted def CategoryTheory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.secondMap₂

deleted def CategoryTheory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.secondMap₃

deleted def CategoryTheory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.topMapᵣ

deleted def CategoryTheory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.topMapₗ

deleted def CategoryTheory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor

deleted def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.bottomMapᵣ

deleted def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.bottomMapₗ

deleted def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap

deleted def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₁

deleted def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₂

deleted def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₃

deleted def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.leftMapᵣ

deleted def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.leftMapₗ

deleted def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap

deleted def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₁

deleted def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₂

deleted def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₃

deleted def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.topMapᵣ

deleted def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.topMapₗ

deleted def CategoryTheory.Functor.LaxMonoidal.ofBifunctor

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.CoreMonoidal.ofBifunctor

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.Monoidal.ofBifunctor

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.bottomMapᵣ

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.bottomMapₗ

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.firstMap

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.firstMap₁

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.firstMap₂

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.firstMap₃

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.leftMapᵣ

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.leftMapₗ

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.secondMap

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.secondMap₁

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.secondMap₂

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.secondMap₃

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.topMapᵣ

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.topMapₗ

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.ofBifunctor.bottomMapᵣ

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.ofBifunctor.bottomMapₗ

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.ofBifunctor.firstMap

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.ofBifunctor.firstMap₁

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.ofBifunctor.firstMap₂

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.ofBifunctor.firstMap₃

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.ofBifunctor.leftMapᵣ

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.ofBifunctor.leftMapₗ

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.ofBifunctor.secondMap

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.ofBifunctor.secondMap₁

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.ofBifunctor.secondMap₂

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.ofBifunctor.secondMap₃

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.ofBifunctor.topMapᵣ

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.ofBifunctor.topMapₗ

added def CategoryTheory.MonoidalCategory.Functor.LaxMonoidal.ofBifunctor

deleted def CategoryTheory.MonoidalCategory.Functor.curriedTensorPreIsoPost

added def CategoryTheory.MonoidalCategory.MonoidalCategory.Functor.curriedTensorPreIsoPost

added def CategoryTheory.MonoidalCategory.MonoidalCategory.curriedTensorPreFunctor

deleted def CategoryTheory.MonoidalCategory.curriedTensorPreFunctor

added def CategoryTheory.MonoidalCategory.ofBifunctor.Pentagon.firstMap

added def CategoryTheory.MonoidalCategory.ofBifunctor.Pentagon.secondMap

added def CategoryTheory.MonoidalCategory.ofBifunctor.Triangle.associatorMap

added def CategoryTheory.MonoidalCategory.ofBifunctor.Triangle.firstMap

added def CategoryTheory.MonoidalCategory.ofBifunctor.Triangle.leftUnitorMap

added def CategoryTheory.MonoidalCategory.ofBifunctor.Triangle.secondMap

added def CategoryTheory.MonoidalCategory.ofBifunctor