Commit 2025-11-18 16:33 0b399191

View on Github →

feat(CategoryTheory): the universal property of localized monoidal categories (#25799) This PR provides a monoidal structure on any functor out of a localized monoidal category whose precomposition with the localization functor is monoidal

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Localization/Bifunctor.lean

Created Mathlib/CategoryTheory/Localization/Monoidal/Functor.lean

added theorem CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app'

added theorem CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app

added theorem CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_ε

added theorem CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_μ

Modified Mathlib/CategoryTheory/Monoidal/Functor.lean

added theorem CategoryTheory.Functor.Monoidal.map_associator'

added theorem CategoryTheory.Functor.Monoidal.map_associator_inv'

Modified Mathlib/CategoryTheory/Monoidal/Multifunctor.lean

added def CategoryTheory.MonoidalCategory.Functor.curriedTensorPreIsoPost

added def CategoryTheory.MonoidalCategory.curriedTensorPreFunctor